Plans regarding the Tseitin translation from DNF to CNF.
More...
Go to the source code of this file.
Detailed Description
Plans regarding the Tseitin translation from DNF to CNF.
 Todo:
 Renaming the file to "CanonicalTranslation.mac"

Then "TseitinTranslation.mac" should be in module PropositionalLogic, where currently we have the Tseitin translation in Formulas.mac. See below for further plans.
 Todo:
 Add statistics

For dualtsplus_fcl.

For rcantrans_fcl2fcl.
 Todo:
 Translation of boolean circuits into boolean CNFclausesets

Where shall the following go ?

In PropositionalLogic/Formulas.mac we have already the Tseitin translation for formulas.

Either there, or even a new module "Circuits".

See [Jackson, Sheridan: Clause Form Conversions for Boolean Circuits; SAT 2004] for more refined forms than the basic Tseitintranslation.

See Satisfiability/Transformers/Generators/plans/TseitinTransformation.hpp for the general considerations.

See Satisfiability/Lisp/PropositionalLogic/plans/TseitinTranslation.hpp for the special case of propositional formulas.

For each gate g in a circuit C, one represents the inputs i by variables v_i, the output by variable o, and then represents the equivalence o <> g( ... v_i ...) by a CNF.

The conjunction of all these CNFs yields the whole CNF, where once the values for all inputs are given, all other variables have a unique value so that the whole CNF becomes true.

This also works for nonboolean circuits and various generalised forms of nonboolean CNFclausesets.
 Todo:
 Understanding dualts_fcl

The following needs to be updated according to the report of MG+OK on boolean functions and their representations.

Then also all variations need to be implemented.

And likely the notion of "dualts" is not appropriate: rename it to "canonical translation".

Perhaps "cantrans_fcl2fcl" ?

The reduced form then "rcantrans_fcl2fcl" ?

And the extended form (currently "plusform") "ecantrans_fcl2fcl" ?

The mathematical notation for reduced resp. extended form could use "" resp. "+".

The extended form can come in three versions: full equivalence, or only one of the two implicationdirections.

And these three extendedversions can also be applied to the reduced form.

Consider a DNF F. The task is to understand the CNF G := dualts_cl(F).

Let n be the number of variables of F, and let c be the number of clauses of F.

Then the variables of G are the n variables of F plus the variables dts(1), ..., dts(c).

The boolean function of G is the conjunction of the equivalences (dts(i) <> C_i) for F = (C_1 or ... or C_c) and the clause D := (dts(1) or ... or dts(c)).

For simplicity we assume that none of the clauses C_i is empty.

Now the natural CNF for an equivalence (a <> (b_1 and ... and b_k)), given by the clauses {a,b_1},...,{a,b_k},{a,b_1,...,b_k} is exactly the set of all primeCNFclauses for this boolean function.

These clauses are also primeCNFclauses of G.

That the clause D is a primeclause of G is equivalent to F being irredundant.

For the applications we have in mind we can assume that F is irredundant (in all our cases it is actually a hitting clauseset (i.e., a disjoint DNF)).

So G is prime (consists only of primeclauses).

G is also irredundant.

The other primeCNFclauses of G are exactly the primeCNFclauses of F.

It is G thus (totally) properly r_1based (see "rbased clausesets" in Investigations/BooleanFunctions/plans/ReductionBasedRepresentations.hpp).
 Todo:
 Strengthening dualts_fcl by adding some redundant clauses

The following needs update: it seems to be implementent by dualtsplus_fcl; see also the todos there.

Given a formal clauselist F as DNF, and a partial assignment phi, there are (of course) forced assignments on phi * dualts(F) which are not derived by unit propagation (while if phi * dualts(F) is unsatisfiable, then {} is in r_1(phi * dualts(F))  so it needs r_2 to compute all forced assignments).

For example the formal DNF [[1,2,3],[{1,2},{1,3}]] has {1} as a forced assignment, however
F : [[1,2,3],[{1,2},{1,3}]]$
G : fcs2cs(fcl2fcs(dualts_fcl(F)));
{{3,1,dts(2)},{2,1,dts(1)},{1,dts(1)},{1,dts(2)},{2,dts(1)},
{3,dts(2)},{dts(1),dts(2)}}
ucp_lpa_0_cs(G)[2];
yields [], not [{1}].

Adding for every literal x the clause (C > x) to dualts(F), where C is the conjunction of dts(i) for every i where x does not occur in the ith clause in F, gives a representation which has that under any partial assignment phi using only variables from F, all forced assignments on phi * F follow by unitclause propagation on dualts_fcl(F).

More generally, adding for some (CNF)clause D the clause (C > D), where C is the conjunction C of all negated indicator variables for clauses which have empty intersection with D, then for partial assignments phi such that D follows from phi * F, D is subsumed by one of the clauses of r_1(phi * F). Moreover, the added clause follows from dualts(F).

Continuing the above example:
G2 : union(G,
{{dts(1),dts(2),1},{1},{dts(1),dts(2),2},{dts(2),2},{dts(1),dts(2),3},{dts(1),3}})$
ucp_lpa_0_cs(G2)[2];
correctly yields [{1}]. One sees here that only additional clauses are interesting where the literal x (as above) occurs in some clause; there are also other strong redundancies.
Definition in file TseitinTranslation.hpp.