PrimeImplicatesImplicants.hpp File Reference

Plans for Maxima-components regarding computation of prime implicates/implicants of boolean functions and clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans for Maxima-components regarding computation of prime implicates/implicants of boolean functions and clause-sets.

  • Add tests for all functions, including
    • all_minequiv_bvs_rsubhg
    • all_minequiv_bvsr_cs
    • all_minequiv_bvsr_sub_cs
  • DONE (to be moved to ComputerAlgebra/Satisfiability/Lisp/Primality/plans/general.hpp) The resolution-module doesn't seem to be the right place.
  • DONE Perhaps we create a whole new module.
  • The basic tasks for a given *clause-set* to compute "prime clauses" and "dual prime clauses".
  • For a boolean function this means that the prime implicates and prime implicants are to be computed.
  • DONE We have this basic terminology problem:
    1. Coming from boolean functions, an absolute point of view is taken, where implicates belong to the "false" side, and "implicants" to the "true" side.
    2. The other point of view (as taken above with "prime clauses" etc.) is relative: Within the given representation (CNF or DNF based) either stay with the representation and minimise the clauses (given a CNF, this would mean the prime implicates), or "go to the other side" (for a CNF this means prime implicants).
    3. So we use "prime clauses" and "dual prime clauses" for the relative point of view, and "prime implicates" resp. "prime implicants" for the absolute point of view.
  • See "Dualisation" below.
  • See "Connections" below.
  • We need generic testfunctions "okltest_prime_clauses_cs", "okltest_dual_prime_clauses_cs" and the special cases "okltest_prime_clauses_full_cs", "okltest_dual_prime_clauses_full_cs" (since there are many algorithms for computing these fundamental functions).
Best method for prime_clauses_cs
  • hardness_cs uses min_resolution_closure_cs(F)[1], which for okltest_hardness_cs is actually better than the current prime_clauses_cs(F) = min_extdp_prod_cs(F). Is this coincidence, or is there a deeper reason?
  • See "Improving min_extdp_cs" below.
  • See "Fast computation of prime implicates/implicants" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp for the investigation.
Improving min_extdp_cs
  • A first reasonable heuristics seems min_extdp_prod_cs --- is it really reasonable?
  • Can we improve the subsumption-elimination in an elegant way?
  • Currently the name likely is not corrected, since if the input is not a full clause-set, then likely we do not compute the min-closure under 2-subsumption resolution (example?).
  • What is the complexity of min_2resolution_closure_cs(F) ?
    1. If we take the input size as 2^n, then the procedure is trivially polynomial (altogether there are at most 3^n clauses). But the question is whether the running time is polynomial in the real input, that is, in F ?!
    2. We need to count the total number of clauses created.
    3. This is exactly the number of clauses which follow from F (over the same variables; no need to distinguish between the old clauses in F and the new created ones, but just altogether is counted).
    4. If F has 2^n clauses, then altogether 3^n clauses are created, where (2^n)^(log_2(3)) = 3^n.
    5. So one could conjecture that the total number of clauses which follow from a full clause-set F (over the same variables, of course) is at most c(F)^(log_2(3)).
    6. In "Computations of all prime clauses for full clause-sets" in Satisfiability/Lisp/Primality/plans/general.hpp it is shown that that number is at most 1/2 c(F)^2 + 1/2 c(F).
  • Hashing:
    1. Efficient implementations of min_2resolution_closure_cs rely on efficient hashing schemes for clauses.
    2. In Satisfiability/FiniteFunctions/QuineMcCluskey.hpp a "total" hashing scheme is used, that is, simply a boolean array of length 3^n is used, with the bijection from clauses with n variables to {0,...,3^n-1} as indexing (hashing) scheme.
    3. This should be efficient for dense clause-sets, but it is very inefficient for sparse clause-sets (and somewhat larger n).
    4. Alternative hashing schemes need to be developed.
  • Implement the algorithm given by "dual_cs" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Constructions.mac
    1. That is, just subsumption elimination needs to be added.
    2. How to do this in a better way? For example doing subsumption elimination inbetween?
  • DONE Or should this go somewhere else??
  • DONE Should we perhaps have modules "PrimeClauses" and "DualPrimeClauses" ? Or one module "Primality" (which contains those two)?
Hitting clause-sets
  • The input of Quine/McCluskey is a (special) hitting clause-set (namely a full clause-set) --- can we somehow generalise the algorithm to work with arbitrary hitting clause-sets?
  • Given a hitting clause-set F, we can easily compute for each clause C in F a prime implicate C' <= C of F, by greedily removing literals from C and checking whether still F implies C' holds.
    1. Achieved by "replace_by_prime_implicates_hitting".
    2. Can all prime implicates of F be obtained in this way (for fixed F)? Likely not (examples?).
    3. Likely there can be exponentially many prime implicates C' <= C ?
    4. And likely it is hard to find some C' of minimal length?
    5. Once we know phi_C' * F is unsatisfiable, it should be possible to read off directly from this computation which literals from C' can be further dropped.
  • In this way we obtain F' <= F consisting of some prime implicates of F such that F' is equivalent to F. By removing redundant clauses from F' we can further go into the direction of a shortest CNF representation of the underlying boolean function.
    1. Since SAT solvers can be used to obtain F, in this way we can harness the power of SAT solvers (w.r.t. computing small splitting trees) for computing small CNF/DNF representations.
  • It should be possible to compute with polynomial delay all prime implicates which are subsuming some clause from F. See "contained_prime_implicate" below.
  • Write the more general function "all_contained_prime_implicates", which returns the set of all prime implicates contained in S (so now we also allow that C doesn't follow from F, which holds iff the returned clause-set is empty).
  • For a recursive solution the problem is to avoid overlaps.

Definition in file PrimeImplicatesImplicants.hpp.