OKlibrary  0.2.1.6
TseitinTranslation.hpp File Reference

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 CNF-clause-sets
  • Where shall the following go ?
    1. In PropositionalLogic/Formulas.mac we have already the Tseitin translation for formulas.
    2. 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 Tseitin-translation.
  • 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 non-boolean circuits and various generalised forms of non-boolean CNF-clause-sets.
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".
    1. Perhaps "cantrans_fcl2fcl" ?
    2. The reduced form then "rcantrans_fcl2fcl" ?
    3. And the extended form (currently "plus-form") "ecantrans_fcl2fcl" ?
    4. The mathematical notation for reduced resp. extended form could use "-" resp. "+".
    5. The extended form can come in three versions: full equivalence, or only one of the two implication-directions.
    6. And these three extended-versions 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 prime-CNF-clauses for this boolean function.
  • These clauses are also prime-CNF-clauses of G.
  • That the clause D is a prime-clause 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 clause-set (i.e., a disjoint DNF)).
  • So G is prime (consists only of prime-clauses).
  • G is also irredundant.
  • The other prime-CNF-clauses of G are exactly the prime-CNF-clauses of F.
  • It is G thus (totally) properly r_1-based (see "r-based clause-sets" 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 clause-list 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 i-th 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 unit-clause 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.