OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.11.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2010, 2011, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00025 
00026 
00027 /* *************************
00028    * Deciding irredundancy *
00029    *************************
00030 */
00031 
00032 /* Predicate to decide whether formal clause-set FF implies clause C,
00033    using solver S: */
00034 /* RENAME: impliesp_fcs */
00035 impliesp_f(FF,C,S) := not S(apply_pa_f(comp_sl(C),FF))$
00036 impliesp_fcs(FF,C,S) := impliesp_f(FF,C,S)$
00037 /* The variation for clause-sets F. */
00038 /* RENAME: impliesp_cs */
00039 impliesp(F,C,S) := not S(cs2fcs(apply_pa_cs(comp_sl(C),F)))$
00040 impliesp_cs(F,C,S) := impliesp(F,C,S)$
00041 
00042 /* Returns true iff input FF (formal clause-set) is minimally unsatisfiable.
00043    The second input, the "solver", shall just return true or false. */
00044 min_unsat_bydef(FF, solver) := not solver(FF) and
00045  block([all_sat : true],
00046   for C in FF[2] unless not all_sat do
00047    all_sat : solver([FF[1], disjoin(C, FF[2])]),
00048   return(all_sat))$
00049 min_unsat_bydef_fcs(FF) := min_unsat_bydef(FF, current_satsolver)$
00050 min_unsat_bydef_cs(F) := min_unsat_bydef_fcs(cs2fcs(F))$
00051 /* More generally, returns true iff input FF (formal clause-set) is
00052    irredundant. */
00053 irredundant_bydef(FF, solver) :=
00054  block([V : FF[1], F : FF[2], redundancy : false],
00055   for C in F unless redundancy do
00056    redundancy : impliesp_f([V,disjoin(C,F)],C,solver),
00057   return(not redundancy))$
00058 irredundant_bydef_fcs(FF) := irredundant_bydef(FF, current_satsolver)$
00059 irredundant_bydef_cs(F) := irredundant_bydef_fcs(cs2fcs(F))$
00060 
00061 
00062 /* *****************************
00063    * Classification of clauses *
00064    *****************************
00065 */
00066 
00067 /* Returns the set of all irredundant clauses (for unsatisfiable
00068    clause-sets also called necessary clauses) for input FF: */
00069 all_irrcl_bydef(FF,S) := block([V : FF[1], F : FF[2], I : {}],
00070   for C in F do
00071     if not impliesp_f([V,disjoin(C,F)],C,S) then I : adjoin(C,I),
00072   return(I))$
00073 all_irrcl_bydef_fcs(FF) := all_irrcl_bydef(FF,current_satsolver)$
00074 all_irrcl_bydef_cs(F) := all_irrcl_bydef_fcs(cs2fcs(F))$
00075 
00076 
00077 /* **************************************
00078    * Saturated minimal unsatisfiability *
00079    **************************************
00080 */
00081 
00082 /* Returns true iff input formal clause-set FF is saturated minimally
00083    unsatisfiable:
00084 */
00085 saturated_min_unsat_bydef(FF, solver) := min_unsat_bydef(FF,solver) and
00086  every_s(lambda([x],irredundant_bydef(apply_pa_fcs({x},FF),solver)),
00087          literals_v(FF[1]))$
00088 saturated_min_unsat_bydef_fcs(FF) :=
00089   saturated_min_unsat_bydef(FF, current_satsolver)$
00090 
00091 /* Return the set of partial assignments of size at most 1 which after
00092    application to formal clause-set FF do not result in a minimally
00093    unsatisfiable clause-set. So
00094     saturated_min_unsat_bydef(FF) = true iff non_saturating_pas_bydef(FF) = {}
00095    for a minimally unsatisfiable FF.
00096 */
00097 non_saturating_pas_bydef(FF,solver) := block(
00098  [assignments : union({{}}, map(set,literals_v(FF[1]))),
00099   result : {}],
00100   for phi in assignments do
00101     if not min_unsat_bydef(apply_pa_fcs(phi,FF),solver) then
00102       result : adjoin(phi,result),
00103   return(result))$
00104 non_saturating_pas_bydef_fcs(FF) :=
00105   non_saturating_pas_bydef(FF, current_satsolver)$
00106 
00107 
00108 /* *************************************
00109    * Marginal minimal unsatisfiability *
00110    *************************************
00111 */
00112 
00113 /* Returns true iff input FF is marginal minimally unsatisfiable: */
00114 marginal_min_unsat_bydef(FF, solver) := min_unsat_bydef(FF,solver) and
00115  if (
00116   for C in FF[2] do
00117    if (
00118      for x in C do
00119        if irredundant_bydef([FF[1], adjoin(disjoin(x,C),disjoin(C,FF[2]))], solver)
00120        then return(false)
00121    ) # done then return(false)
00122  ) =  done then true else false$
00123 marginal_min_unsat_bydef_fcs(FF) :=
00124   marginal_min_unsat_bydef(FF, current_satsolver)$
00125 
00126 
00127