Tseitin transformation

A translation of a propositional formula into CNF that introduces a fresh variable $g$ for each subformula $φ$ and adds the clauses of $g \leftrightarrow φ$ . The result is equisatisfiable with the input rather than equivalent, and its size is linear in the input's.

For a gate with inputs $a$ and $b$ , already replaced by the variables or literals standing for them, each definition is three clauses:

g \leftrightarrow (a \land b) \equiv (\neg g \lor a) \land (\neg g \lor b) \land (g \lor \neg a \lor \neg b)

g \leftrightarrow (a \lor b) \equiv (g \lor \neg a) \land (g \lor \neg b) \land (\neg g \lor a \lor b)

Negation needs no new variable, since $\neg a$ is already a literal. The encoding of a formula is the conjunction of every gate's clauses and the unit clause asserting the root's variable.

It is equisatisfiable because the definitions determine every gate variable from the input variables. A satisfying assignment of the input extends to one of the encoding by evaluating each gate, and any satisfying assignment of the encoding restricts to one of the input, since the root is asserted and each gate variable equals its subformula. For the same reason the two have the same number of models.

One fresh variable per binary gate. Variables 1 to nvars are the input's.

let tseitin f nvars =
  let next = ref nvars and clauses = ref [] in
  let emit c = clauses := c :: !clauses in
  let rec go = function
    | Var v -> v
    | Not a -> - go a
    | And (a, b) ->
        let a = go a and b = go b in
        incr next; let g = !next in
        emit [ -g; a ]; emit [ -g; b ]; emit [ g; -a; -b ]; g
    | Or (a, b) ->
        let a = go a and b = go b in
        incr next; let g = !next in
        emit [ g; -a ]; emit [ g; -b ]; emit [ -g; a; b ]; g
  in
  let root = go f in
  emit [ root ];
  (!next, List.rev !clauses)

For the disjunction of n conjunctions (x_i and y_i), with 2n input variables. The encoding has 3 clauses per gate and 1 for the root, so 3(2n - 1) + 1 = 6n - 2.

 n   distributed   tseitin (clauses, variables)
 1             2         4, 3
 2             4        10, 7
 5            32        28, 19
10          1024        58, 39
15         32768        88, 59

When a subformula occurs with only one polarity, one direction of its definition is enough. Under an even number of negations it suffices to have $g \to φ$ , which drops the third clause of each gate above. This is the Plaisted–Greenbaum encoding.^[2] It is still equisatisfiable, but no longer preserves the number of models, because a gate variable constrained in one direction can sometimes take either value.