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)

Connections to other modules
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).
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,
Translations to CNF/DNF
  • Write direct translation (without new variables).
  • Complete the Tseitin translation.

Definition in file TseitinTranslation.hpp.