The Tseytin transformation, alternatively written Tseitin transformation, takes as input an arbitrary combinatorial logic circuit and produces an equisatisfiable boolean formula in conjunctive normal form (CNF). The length of the formula is linear in the size of the circuit. Input vectors that make the circuit output "true" are in 1-to-1 correspondence with assignments that satisfy the formula. This reduces the problem of circuit satisfiability on any circuit (including any formula) to the satisfiability problem on 3-CNF formulas. It was discovered by the Russian scientist Grigori Tseitin.
Motivation The naive approach is to write the circuit as a Boolean expression, and use De Morgan's law and the distributive property to convert it to CNF. However, this can result in an exponential increase in equation size. The Tseytin transformation outputs a formula whose size grows linearly relative to the input circuit's. The original application involved making 'statistical riders' for a Nordic transportation company from a day's single-trip tickets, effectively joining unlabeled trips that could be a single person.
Approach The output equation is the constant 1 set equal to an expression. This expression is a conjunction of sub-expressions, where the satisfaction of each sub-expression enforces the proper operation of a single gate in the input circuit. The satisfaction of the entire output expression thus enforces that the entire input circuit is operating properly. For each gate, a new variable representing its output is introduced. A small pre-calculated CNF expression that relates the inputs and outputs is appended (via the "and" operation) to the output expression. Note that inputs to these gates can be either the original literals or the introduced variables representing outputs of sub-gates. Though the output expression contains more variables than the input, it remains equisatisfiable, meaning that it is satisfiable if, and only if, the original input equation is satisfiable. When a satisfying assignment of variables is found, those assignments for the introduced variables can simply be discarded. A final clause is appended with a single literal: the final gate's output variable. If this literal is complemented, then the satisfaction of this clause enforces the output expression's to false; otherwise the expression is forced true.
Examples Consider the following formula
ϕ := ( ( p ∨ q ) ∧ r ) → ( ¬ s ) . {\displaystyle \phi :=((p\lor q)\land r)\to (\neg s).}
Consider all subformulas (excluding simple variables):
¬ s , p ∨ q , ( p ∨ q ) ∧ r , ( ( p ∨ q ) ∧ r ) → ( ¬ s ) . {\displaystyle {\begin{aligned}&\neg s,\\&p\lor q,\\&(p\lor q)\land r,\\&((p\lor q)\land r)\to (\neg s).\end{aligned}}}
Introduce a new variable for each subformula:
x 1 ↔ ¬ s , x 2 ↔ p ∨ q , x 3 ↔ x 2 ∧ r , x 4 ↔ x 3 → x 1 . {\displaystyle {\begin{aligned}x_{1}&\leftrightarrow \neg s,\\x_{2}&\leftrightarrow p\lor q,\\x_{3}&\leftrightarrow x_{2}\land r,\\x_{4}&\leftrightarrow x_{3}\to x_{1}.\end{aligned}}}
Conjunct all substitutions and the substitution for ϕ {\displaystyle \phi } :
… excerpt ends here. Continue reading the full article.
