OKlibrary  0.2.1.6
TseitinTranslation.hpp File Reference

Plans for Maxima-components 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 Maxima-components translating from propositional logic to CNF via the Tseitin translation (and variations)

Todo:
Connections to other modules
Todo:
Implementing the Tseitin-transformation (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 Tseitin-translation, we obtain a 3-CNF F' over the variables from F plus new auxiliary variable such that
1. every satisfying assignment for F can (easily) be extended to a satisfying assignment for F';
2. 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):
1. For a sub-formula 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 non-deterministic).
2. F' is obtained by adding the unit-clause {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':
1. handling of arbitrary and-or-arities
2. performing simplifications on the clauses
3. 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 horn-like 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 and-or-formulas, while Q is a positive and-formula. So the P_i and all their sub-occurrences occur negatively, while Q occurs positively.
• Thus t(F) is a 3-CNF with (essentially) clauses of the form
1. (a or b) -> c
2. (a and b) -> c
3. a -> (b and c)
where a, b, c are variables (atomic formulas).
• Types 1 and 3 translate into 2 binary Horn-clauses 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.