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 clausesets into equivalent DNF clausesets, or, equivalently, translating DNF clausesets into equivalent CNF clausesets. 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* DNFrepresentation (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 splittingtree methods all other methods are closely related to finding dual prime clauses.
 Todo:
 Notions

For a clauseset 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 primeclauses for f are exactly the prime clauses for any CNFrepresentation F of f, while the DNF prime clauses for f are exactly the prime clauses for any DNFrepresentation F for f.

A clauseset 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 primeclauses.

A "dual prime clause" of a clauseset 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 DNFrepresentation 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 splittingtree 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 clausesets

Connections:

See "min_2resolution_closure_cs" in Satisfiability/Lisp/Primality/plans/PrimeImplicatesImplicants.hpp for a Maxima function.

See Satisfiability/FiniteFunctions/plans/QuineMcCluskey.hpp for a C++ function.

And see Investigations/BooleanFunctions/plans/QuineMcCluskey.hpp for investigations.

Consider a full clauseset 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:

Consider C with var(C) <= var(F).

C follows from F iff all full clauses D >= C are elements of F.

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.

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.

The map {C clause over var(F)} > [C_,C_+] is injective (since we have C = C_ intersect C_+).

It follows that the number of clauses which follow from F is at most the number of 1 or 2element subsets of F, that is, binom(c,1) + binom(c,2).

Is that upper bound sharp?

It is not sharp if F contains all clauses.

Computing all primeclauses according to the above upper bound:

All clauses C which follow can be found by running through all <=2elementsubsets {D,E} of F, determining C := D intersect E, and determining whether all supsets of C are in F.

The supsettest 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.

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.

Let F' be the set of all clauses which follow from F.

The primeclauses are the subsumptionminimal elements of F.

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 setsystems" in ComputerAlgebra/Hypergraphs/Lisp/plans/SetSystems.hpp.

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.