Plans for Maximacomponents translating from propositional logic to CNF via the Tseitin translation (and variations)
More...
Go to the source code of this file.
Detailed Description
Plans for Maximacomponents translating from propositional logic to CNF via the Tseitin translation (and variations)
 Todo:
 Connections to other modules
 Todo:
 Implementing the Tseitintransformation (with variations)

Given a propositional formula F built from negation, conjunction and disjunction (for simplicity we consider only binary operations here), by the process specified below, a refinement of the Tseitintranslation, we obtain a 3CNF F' over the variables from F plus new auxiliary variable such that

every satisfying assignment for F can (easily) be extended to a satisfying assignment for F';

every satisfying assignment for F' is a satisfying assignment for F (when restricted to the variables in F).

The process F > F' works, using auxiliary variables v(G) for subformulas G of F, by collecting clauses (to avoid renaming of existing variables, let v(a) = a for variables a from F):

For a subformula G of F, where G is of the form op G_1 ... G_n (for us n <= 2), with op one of negation, conjunction or disjunction (written for convenience in prefix form), add the clauses
 (i) (op v(G_1) ... v(G_n)) > v(G)
 (ii) v(G) > (op v(G_1) ... v(G_n))
where in case G occurs positively in F, (i) can be dropped, while if G occurs negatively in F, (ii) can be dropped (so the process might be nondeterministic).

F' is obtained by adding the unitclause {v(F)} to all these clauses.

Is there a general input format for boolean formulas? See "General propositional formulas and circuits" in Interfaces/InputOutput/plans/general.hpp.

Some obvious variations on the transformation F > F':

handling of arbitrary andorarities

performing simplifications on the clauses

either using always (i)+(ii), or exactly one of them, or using some heuristic.

All of the above should be first handled at the Maxima/Lisp level (in module ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions).
 Todo:
 Horn specialities

Is the following useful?

Let us denote by t(F) the result where always one of (i), (ii) is dropped (appropriately).

A class of hornlike formulas is the class of formulas F = C_1 and ... and C_k where each C_i is of the form (P_1 and ... and P_m) > Q where the P_i are arbitrary positive andorformulas, while Q is a positive andformula. So the P_i and all their suboccurrences occur negatively, while Q occurs positively.

Thus t(F) is a 3CNF with (essentially) clauses of the form

(a or b) > c

(a and b) > c

a > (b and c)
where a, b, c are variables (atomic formulas).

Types 1 and 3 translate into 2 binary Hornclauses each, while type 2 is already a Horn clause.

Thus t(F) is a Horn formula. Since t(F) is computable in linear time, and SAT decision for Horn formulas is achievable in linear time, SAT decision for those generalised formulas F is achievable in linear time,
 Todo:
 Translations to CNF/DNF

Write direct translation (without new variables).

Complete the Tseitin translation.
 Todo:
 Reorganisation
 Todo:
 Optimisation
Definition in file TseitinTranslation.hpp.