OKlibrary  0.2.1.6
PrimeImplicatesImplicants.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.3.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 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/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Transversals/Bounded/MaintainingBound.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00029 
00030 
00031 /* *****************
00032    * Prime clauses *
00033    *****************
00034 */
00035 
00036 /* Generic function, using the "best" method (at Maxima-level) to compute
00037    the set of all prime-clauses of clause-set F:
00038 */
00039 prime_clauses_cs(F) := min_extdp_prod_cs(F)$
00040 
00041 /* Considering F as CNF, prime_clauses_cs(F) is the set of all "prime
00042    implicates" of the corresponding boolean function, while considering F as
00043    a DNF this is the set of all "prime implicants".
00044 
00045    That is, a prime implicate of F as CNF is a CNF-clause C which follows
00046    from F, while this is not true for any strict subset of C. And a prime
00047    implicant of F as a DNF is a DNF-clause C which implies F, while this is
00048    not true for any strict subset of C.
00049 
00050    Note that in this library a "clause" C is a combinatorial object, and
00051    whether C is a "CNF-clause" or a "DNF-clause" is just a matter of an
00052    (additional) interpretation.
00053 
00054    In other words, using the CNF interpretation, the prime clauses of F
00055    are the comp_sl(phi) for partial assignments phi such that phi * F
00056    is unsatisfiable, while this is not true for any strict subset of phi.
00057    And using the DNF interpretation, the prime clauses of F
00058    are the phi for partial assignments phi such that phi * F
00059    is tautological, while this is not true for any strict subset of phi.
00060 
00061    Note that in this library partial assignments are just represented
00062    as DNF-clauses, taking for clause-sets the "default interpretation"
00063    as CNF-clause-sets.
00064 
00065    Alternative computations:
00066    For general F we have
00067      prime_clauses_cs(F) = min_resolution_closure_cs(F)[1]
00068                          = min_2resolution_closure_cs(expand_cs(F))
00069                          = min_elements(dual_cs(G))
00070      (the first method is often called the "consensus algorithm", the third
00071      the "double negation procedure of Nelson").
00072    For full F we have
00073      prime_clauses_cs(F) = min_2resolution_closure_cs(F)
00074    (the prime-computation of the Quine/McCluskey procedure).
00075 
00076 */
00077 
00078 /* Tison's method
00079 
00080    This is just like applying DP-resolution, but keeping all clauses, except
00081    when they are subsumed. So we treat it as "extended DP".
00082 */
00083 extdp_operator_cs(F,v) := block(
00084  [Fv : subset(F, lambda([C], not disjointp(C, {v,-v})))],
00085   union(F, resolvents_cs_l(Fv,v)))$
00086 min_extdp_operator_cs(F,v) := min_elements(extdp_operator_cs(F,v))$
00087 
00088 /* Using V (from left to right): */
00089 min_extdp_cs(F,V) := (for v in V do F : min_extdp_operator_cs(F,v), F)$
00090 
00091 /* Heuristics: */
00092 min_extdp_prod_cs(F) := min_extdp_cs(F,sortvar_prodocc_cs(F))$
00093 
00094 
00095 /* **********************
00096    * Dual prime clauses *
00097    **********************
00098 */
00099 
00100 /* Considering F as CNF, the "dual prime clauses" are the prime implicants
00101    of F, while considering F as DNF, the dual prime clauses are the
00102    prime implicates of F.
00103 */
00104 
00105 /* Various ways of computing the set of dual prime clauses of a clause-set F:
00106 
00107    dual_prime_clauses_cs(F) =
00108      min_elements(dual_cs(F)) =
00109      min_2resolution_closure_cs(all_sat_cs(F)) =
00110 
00111      min_resolution_closure_cs(G)[1]
00112 
00113    where G is any DNF representation of F (for example, disjoint DNF
00114    representations are obtained from any splitting tree for F).
00115 */
00116 
00117 /* Note that
00118 
00119      prime_clauses_cs(F) = dual_prime_clauses_cs(dual_prime_clauses_cs(F)),
00120 
00121    and more generally
00122 
00123      prime_clauses_cs(F) = dual_prime_clauses_cs(G),
00124 
00125    where G is any DNF representation of F. This yields
00126 
00127      prime_clauses_cs(F) = min_elements(dual_cs(G)).
00128 
00129 */
00130 
00131 
00132 /* *************************************
00133    * Prime-clauses of full clause-sets *
00134    *************************************
00135 */
00136 
00137 /* The special case of min_resolution_closure_cs where the input clauses
00138    are all full (contain all variables).
00139    In other words, computing all minimal resolvents, i.e., all prime clauses
00140    (for CNF's these are the prime implicates, for DNF's the prime implicants)
00141    for full clause-sets.
00142 */
00143 min_2resolution_closure_cs(F) := block(
00144  [prime_implicates : {}, new_implicates, n : nvar_cs(F)],
00145   for i : 0 thru n do (
00146     [F, new_implicates] : two_subsumption_resolvents_rem_cs(F),
00147     prime_implicates : union(prime_implicates,new_implicates)),
00148   return(prime_implicates))$
00149 /* With monitoring, and returns additionally the list of level sizes: */
00150 min_2resolution_closure_mon_cs(F) := block(
00151  [prime_implicates : {}, new_implicates, n : nvar_cs(F),
00152   counts : [length(F)]],
00153   for i : 0 thru n do (
00154     if oklib_monitor then (
00155       print("min_2resolution_closure_cs: entering level =", n - i),
00156       print("Yet", length(prime_implicates), "prime implicates found.")),
00157     [F, new_implicates] : two_subsumption_resolvents_rem_cs(F),
00158     prime_implicates : union(prime_implicates,new_implicates),
00159     counts : cons(length(F), counts)
00160   ),
00161   return([prime_implicates, reverse(counts)]))$
00162 
00163 
00164 /* ******************************************************
00165    * Minimum equivalent clause-sets of full clause-sets *
00166    ******************************************************
00167 */
00168 
00169 /* Given a full clause-set F, the equivalent clause-sets with a minimal
00170    numbers of clauses and secondly minimal number of literal occurrences
00171    are exactly the minimum transversals of the hypergraph
00172    subsumption_ghg(min_2resolution_closure_cs(F), F)
00173    (see ComputerAlgebra/Hypergraphs/Lisp/Basics.mac for
00174    subsumption_ghg).
00175 */
00176 
00177 /* The subsumption-hypergraph of a full clause-set F: Vertices are the
00178    prime clauses of F, hyperedges are the sets of prime-clauses which
00179    subsume some total assignment:
00180 */
00181 subsumption_hg_full_cs(F) :=
00182  ghg2hg(subsumption_ghg(min_2resolution_closure_cs(F), F))$
00183 
00184 /* Now computing the reduced subsumption-hypergraph (where necessary prime
00185    clauses have been eliminated as well as subsumptions), together with the
00186    set of necessary clauses:
00187 */
00188 rsubsumption_hg_full_cs(F) := rsubsumption_hg(min_2resolution_closure_cs(F), F)$
00189 rsubsumption_hg_full_fcs(FF) := rsubsumption_hg_full_cs(fcs2cs(FF))$
00190 
00191 
00192 /*
00193    Using a simple hypergraph transversal algorithm for computing all minimum
00194    "prime representations" (as a repetition-free list) of a full clause-set F:
00195 */
00196 all_minequiv_bvs_cs(F) :=
00197   minimum_transversals_bvs_hg(subsumption_hg_full_cs(F))$
00198 all_minequiv_bvs_fcs(FF) := all_minequiv_bvs_cs(fcs2cs(FF))$
00199 
00200 /* Computing the list of all minimum prime representations by using the
00201    output S of rsubsumption_hg_full_cs (this is somewhat more efficient):
00202 */
00203 all_minequiv_bvs_rsubhg(S) :=
00204   add_elements_l(S[2], minimum_transversals_bvs_hg(S[1]))$
00205 /* The resulting computation of all minimum prime representations of a
00206    full clause-set F: */
00207 all_minequiv_bvsr_cs(F) := all_minequiv_bvs_rsubhg(rsubsumption_hg_full_cs(F))$
00208 all_minequiv_bvsr_fcs(FF) := all_minequiv_bvsr_cs(fcs2cs(FF))$
00209 /* Allowing the specification of total assignments which the prime clauses
00210    must subsume. */
00211 all_minequiv_bvsr_sub_cs(F, G_sub) :=
00212   all_minequiv_bvs_rsubhg(
00213     rsubsumption_hg(min_2resolution_closure_cs(F), G_sub))$
00214 
00215 
00216 /* *************************************
00217    * Dualisation for full clause-sets  *
00218    *************************************
00219 */
00220 
00221 /* Computing the dual prime clauses, that is, for a full CNF the set of all
00222    prime implicants (minimal satisfying assignments), and for a full DNF the
00223    set of all prime implicates (minimal clauses which follow):
00224 */
00225 dual_min_2resolution_closure_cs(F) :=
00226  comp_cs(min_2resolution_closure_cs(setdifference(full_fcs_v(var_cs(F))[2], F)))$
00227 /* We have
00228    dual_min_2resolution_closure_cs(F) = min_resolution_closure_cs(dual_cs(F))[1]
00229    (for full clause-sets).
00230    Note that here
00231      setdifference(full_fcs_v(var_cs(F))[2], F) = all_sat_cs(F).
00232 */
00233 
00234 /* Computing all minimum "dual prime representations" of a full clause-set F,
00235    using a simple algorithm (as above):
00236 */
00237 dual_all_minequiv_bvs_cs(F)  := block(
00238  [G : setdifference(full_fcs_v(var_cs(F))[2], F)],
00239   map(comp_cs,minimum_transversals_bvs_hg(ghg2hg(
00240     subsumption_ghg(min_2resolution_closure_cs(G), G)))))$
00241 
00242 
00243 /* **************************************************
00244    * Finding contained prime-clauses by SAT solvers *
00245    **************************************************
00246 */
00247 
00248 /* Given a clause-set F (interpreted as CNF) and a clause C which follows from
00249    F, find a prime implicate C' <= S with the help of SAT solver S (which must
00250    be applicable to the closure of {F} under applications of partial
00251    assignments):
00252 */
00253 /* RENAME: contained_prime_clause_cs */
00254 contained_prime_implicate(F,C,S) := block([reduced : true],
00255  while reduced do (
00256    reduced : false,
00257    for x in C unless reduced do block([D : disjoin(x,C)],
00258      if S(apply_pa(comp_sl(D), F)) = false then (
00259        C : D, reduced : true))),
00260  return(C))$
00261 
00262 
00263 /* Replace for a clause-set F (as CNF) each clause C by a prime
00264    implicate C' <= C, using a SAT solver which works on
00265    the closure of {F} under the application of partial
00266    assignments: */
00267 /* RENAME: replace_by_prime_clauses_cs */
00268 replace_by_prime_implicates(F,S) := block([G : {}],
00269   for C in F do G : adjoin(contained_prime_implicate(F,C,S), G),
00270   return(G))$
00271 /* The special case where F is a hitting clause-set: */
00272 /* RENAME: replace_by_prime_clauses_hitting_cs */
00273 replace_by_prime_implicates_hitting(F) :=
00274   replace_by_prime_implicates(F,sat_decision_hitting_cs)$
00275 
00276