OKlibrary  0.2.1.6
general.hpp File Reference

General plans for handling prime clauses and dual prime clauses. More...

Go to the source code of this file.


Detailed Description

General plans for handling prime clauses and dual prime clauses.

This includes:

  • Computation of all prime implicates and/or all prime implicants.
  • Computation of shortest CNF and/or shortest DNF representation of a finite function.
  • Dualisation: Translating CNF clause-sets into equivalent DNF clause-sets, or, equivalently, translating DNF clause-sets into equivalent CNF clause-sets. Or the same as finding for a CNF a collection of satisfying partial assignments which cover all satisfying (total) assignments.
Todo:
Organisation
  • DONE Move ComputerAlgebra/Satisfiability/Lisp/Resolution/PrimeImplicatesImplicants.mac here.
  • The task of just finding *some* DNF-representation (without new variables!) of a CNF seems close enough to finding dual prime clauses to be included in this module.
  • Or should there be a specialisation module "Duality" for this task? But except of the splitting-tree methods all other methods are closely related to finding dual prime clauses.
Todo:
Notions
  • For a clause-set F we simply speak of "prime clauses", which are the minimal clauses derivable by resolution from F.
  • For F as CNF, these are the minimal clauses following from F, while for F as DNF these are the minimal clauses implying F.
  • For boolean functions f we use "CNF prime clauses" for "prime implicates", and "DNF prime clauses" for "prime implicantes".
  • Note that the CNF prime-clauses for f are exactly the prime clauses for any CNF-representation F of f, while the DNF prime clauses for f are exactly the prime clauses for any DNF-representation F for f.
  • A clause-set F is "prime" if all C in F are prime clauses for F, while F is "maximal prime" if F is prime, and actually contains all its prime-clauses.
  • A "dual prime clause" of a clause-set F is a prime clause of the combinatorial dualisation dual_cs(F), which at the boolean function level corresponds to dualisation of "the" boolean function (negation of inputs and outputs; whether CNF- or DNF-representation is used, does not matter(!)), which is the same as considering F as CNF instead of DNF or vice versa.
  • That is, a clause C is a dual prime clause of F iff C is a minimal transversal of F, considered as hypergraph over its literals.
  • Considering F as CNF, the dual prime clauses are exactly the minimal satisfying partial assignments, representing partial assignments as sets of literals set to true.
  • And considering F as DNF, the dual prime clauses are exactly the minimal falsifying partial assignments, representing partial assignments as sets of literals set to false.
  • The prime clauses of F are exactly the dual prime clauses of the set of dual prime clauses of F.
Todo:
Connections / Relations
Todo:
Create milestones.
Todo:
Extract the methods related to splitting trees
  • From the various splitting-tree forms we need to extract the clauses representing the satisfying assignments (in CNF interpretation).
Todo:
Shortest dual representations
Todo:
Computations of all prime clauses for full clause-sets
  • Connections:
    1. See "min_2resolution_closure_cs" in Satisfiability/Lisp/Primality/plans/PrimeImplicatesImplicants.hpp for a Maxima function.
    2. See Satisfiability/FiniteFunctions/plans/QuineMcCluskey.hpp for a C++ function.
    3. And see Investigations/BooleanFunctions/plans/QuineMcCluskey.hpp for investigations.
  • Consider a full clause-set F with c=c(F) clauses: Then at most c*(c+1)/2 = 1/2 c^2 + 1/2 c many clauses C with var(C) <= var(F) follow from F:
    1. Consider C with var(C) <= var(F).
    2. C follows from F iff all full clauses D >= C are elements of F.
    3. Let C_- be the full clause obtained from C by adding all missing negative literals, and lit C_+ be the full clause obtained from C by adding all missing positive literals.
    4. Consider - < +, and using lexicographical order, where the variables of C form the initial segment, we thus have that C follows from F iff the interval [C_-, C_+] is subset of F.
    5. The map {C clause over var(F)} -> [C_-,C_+] is injective (since we have C = C_- intersect C_+).
    6. It follows that the number of clauses which follow from F is at most the number of 1- or 2-element subsets of F, that is, binom(c,1) + binom(c,2).
  • Is that upper bound sharp?
    1. It is not sharp if F contains all clauses.
  • Computing all prime-clauses according to the above upper bound:
    1. All clauses C which follow can be found by running through all <=2-element-subsets {D,E} of F, determining C := D intersect E, and determining whether all supsets of C are in F.
    2. The supset-test can be simply done by running through all elements of F and counting those which contain C; this can be done in time c * n.
    3. Alternatively one can sort F lexicographically, and search for each superset of C using binary search; for very small C the first method should be more efficient, for the rest the second method.
    4. Let F' be the set of all clauses which follow from F.
    5. The prime-clauses are the subsumption-minimal elements of F.
    6. F' is "convex" (contains with C <= D also all clauses inbetween), and thus we can apply the special algorithm for computing minimal elements described in "Minimal elements for convex set-systems" in ComputerAlgebra/Hypergraphs/Lisp/plans/SetSystems.hpp.
    7. Alternatively to first compute F' and then to extract the minimal elements (as above), one could, when computing an new implicant C, already check whether also some C-{x} exists --- only if not, then the clause is included (it's then a prime clause).

Definition in file general.hpp.