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.