Tseitin transformation

The Tseitin transformation turns any propositional formula into conjunctive normal form with only linear growth, by giving each subformula a name^[1]. For each connective in the formula, a fresh variable $g$ is introduced together with clauses stating that $g$ equals the value of that connective applied to its operands' variables; finally the variable of the whole formula is asserted. Converting to CNF by distributing ∨ over ∧ can make a formula exponentially larger, whereas the Tseitin transformation adds at most three clauses per binary connective. The price is new variables, and the result is not logically equivalent to the original, only equisatisfiable: one is satisfiable exactly when the other is, and satisfying assignments correspond one to one. Grigori Tseitin introduced the construction in 1966 in a study of the length of proofs^[1]. It is the standard way to present formulas and circuits to SAT solvers.

For a formula $\phi$, traverse its subformulas. A variable stands for itself and a negation $\neg a$ is the negated literal of $a$. For each conjunction or disjunction with operand literals $a$ and $b$, introduce a new variable $g$ and the clauses of the equivalence^[1][6]:

Other gates have their own small encodings; exclusive or, $g\leftrightarrow a\oplus b$, needs four clauses of three literals. The output is the conjunction of all the definitions together with the unit clause for the variable of $\phi$ itself.

open Prop
 
(* Tseitin's transformation: every subformula gets a variable standing
   for its value, and a few clauses define that variable in terms of its
   operands. Variables above nvars are new. With polarity = true only
   the implications needed in the direction the subformula is used are
   emitted (Plaisted and Greenbaum). *)
let transform ?(polarity = false) nvars formula =
  let next = ref nvars and clauses = ref [] in
  let emit c = clauses := c :: !clauses in
  (* pos: the subformula occurs positively, so only g → f is needed;
     neg: only f → g. Without polarity both are emitted. *)
  let rec go f pos neg =
    match f with
    | Var v -> v
    | Not a -> - (go a neg pos)
    | And (a, b) ->
      let x = go a pos neg and y = go b pos neg in
      incr next; let g = !next in
      if pos then (emit [ -g; x ]; emit [ -g; y ]);          (* g → x ∧ y *)
      if neg then emit [ g; -x; -y ];                         (* x ∧ y → g *)
      g
    | Or (a, b) ->
      let x = go a pos neg and y = go b pos neg in
      incr next; let g = !next in
      if pos then emit [ -g; x; y ];                          (* g → x ∨ y *)
      if neg then (emit [ g; -x ]; emit [ g; -y ]);           (* x ∨ y → g *)
      g
  in
  let root = go formula true (not polarity) in
  emit [ root ];
  Cnf.of_clauses (List.rev !clauses) |> fun c -> { c with Cnf.nvars = !next }

open Prop

((x1 ∧ x2) ∨ ¬x3)
Tseitin: 7 clauses
  -4 1
  -4 2
  4 -1 -2
  -5 4 -3
  5 -4
  5 3
  5
Plaisted–Greenbaum: 4 clauses
  -4 1
  -4 2
  -5 4 -3
  5

The clauses defining $g$ are satisfied exactly when $g$ has the value of its subformula. Hence in any model of the CNF, by induction from the leaves, every new variable carries the value of its subformula under the original variables, and the asserted root variable being true means that $\phi$ is true. Conversely, any model of $\phi$ extends to a model of the CNF in exactly one way, by giving each new variable the value of its subformula. So the two are equisatisfiable, a model of the CNF restricted to the original variables is a model of $\phi$, and the number of models is the same^[6]. The last property matters for model counting.

open Prop
 
(* Random formulas; check that each transformation is satisfiable exactly
   when the formula is, and that a model of the CNF, restricted to the
   original variables, satisfies the formula. *)
let rec random d = if d = 0 || Random.int 4 = 0 then Var (1 + Random.int 6)
  else match Random.int 3 with
    | 0 -> Not (random (d - 1))
    | 1 -> And (random (d - 1), random (d - 1))
    | _ -> Or (random (d - 1), random (d - 1))
 
let brute f = List.exists (fun bits -> eval (fun v -> bits land (1 lsl v) <> 0) f) (List.init 128 Fun.id)
 
let pairs n = List.init n (fun i -> And (Var (2 * i + 1), Var (2 * i + 2)))
  |> List.fold_left (fun acc t -> match acc with None -> Some t | Some a -> Some (Or (a, t))) None |> Option.get

4000 transformations checked, 0 wrong
size of (x1 ∧ x2) ∨ ... ∨ (x(2n-1) ∧ x(2n)):
n =  1: Tseitin   4 clauses,   3 variables; Plaisted–Greenbaum   3 clauses
n =  2: Tseitin  10 clauses,   7 variables; Plaisted–Greenbaum   6 clauses
n =  4: Tseitin  22 clauses,  15 variables; Plaisted–Greenbaum  12 clauses
n =  8: Tseitin  46 clauses,  31 variables; Plaisted–Greenbaum  24 clauses
n = 12: Tseitin  70 clauses,  47 variables; Plaisted–Greenbaum  36 clauses
n = 16: Tseitin  94 clauses,  63 variables; Plaisted–Greenbaum  48 clauses

On the family $(x_1\wedge x_2)\vee \cdots \vee (x_{2n-1}\wedge x_{2n})$, distributing ∨ over ∧ gives $2^n$ clauses, 65,536 for $n=16$, against 94 for the Tseitin transformation.

Plaisted and Greenbaum observed that only half of each equivalence is needed^[2]. A subformula that occurs positively, under an even number of negations, only has to be implied by its variable, $g\to \psi$: if the CNF is satisfied, the variables that must be true then force their subformulas to be true, which suffices to make $\phi$ true. A subformula that occurs negatively needs only $\psi \to g$. Subformulas that occur with both polarities, as under an equivalence or exclusive or, need both. The result is still equisatisfiable, with fewer clauses, but a model of $\phi$ no longer extends uniquely, so model counts are not preserved, and the one-sided definitions give unit propagation less to work with. In the experiment above, the variant needs 48 clauses where the full transformation needs 94.

The transformation applies unchanged to Boolean circuits, directed acyclic graphs in which a gate may feed several others: each gate is named once, however many gates use it. This is how hardware verification problems and bit-blasted arithmetic reach SAT solvers, and a circuit is often simplified first, by structural hashing of identical gates and by rewriting, which shrinks the CNF considerably^[8][5]. Tree-shaped formulas in which the same subformula is written out several times benefit from detecting the repetition, since each copy would otherwise get its own variable. For formulas given as circuits, Jackson and Sheridan compared the Tseitin and Plaisted–Greenbaum encodings with further refinements that avoid naming gates with a single fanout^[7].

Tseitin's paper was about proofs, not encodings. He introduced the extension rule, which allows a proof to define a new variable as an abbreviation for a formula of existing ones, exactly as the transformation does, and showed that resolution with this rule, extended resolution, can be much stronger than resolution alone^[1]. Cook later used extended resolution to give polynomial-size proofs of the pigeonhole principle, which has no short resolution proofs^[4]. The same paper also introduced what are now called Tseitin formulas, which state that the edges of a graph can be labelled so that every vertex has a prescribed parity, and proved lower bounds on restricted resolution proofs for them; Urquhart showed in 1987 that on expander graphs they require exponentially long resolution refutations of any kind^[3].

Tseitin presented “On the complexity of derivation in propositional calculus” at a Leningrad seminar in 1966; it was published in Russian in 1968 and in English translation in 1970^[1]. Its CNF construction became part of the folklore of automated reasoning, and Plaisted and Greenbaum published the polarity-based refinement in 1986 in the context of first-order clause-form translation^[2]. With the rise of SAT-based hardware verification in the late 1990s and 2000s, the transformation became the standard front end for circuits, usually combined with circuit simplification^[8][5].

• CNFA propositional formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, each clause a disjunction of literals, and each literal a variable or its negation. Every formula is equivalent to one in CNF, but the equivalent CNF can be exponentially larger; the Tseitin transformation instead produces an equisatisfiable CNF of linear size by adding variables. CNF is the input format of SAT solvers and resolution provers, and restricted forms such as Horn clauses and 2-CNF can be solved in linear time.
• SATThe Boolean satisfiability problem, SAT, asks whether some assignment of true and false to the variables of a propositional formula makes the formula true. It was the first problem shown to be NP-complete, so every problem in NP reduces to it, and no polynomial-time algorithm is known. In practice SAT solvers based on conflict-driven clause learning decide industrial instances with millions of variables, which has made SAT a general-purpose engine for hardware and software verification, planning, scheduling and combinatorics.
• DIMACS CNFDIMACS CNF is the standard plain-text format for Boolean formulas in conjunctive normal form, read by essentially every SAT solver. After optional comment lines beginning with c, a header p cnf V C gives the number of variables and clauses; each clause is then a list of non-zero integers, v for a variable and −v for its negation, terminated by 0. It was defined for the Second DIMACS Implementation Challenge in 1993 and has variants for quantified formulas (QDIMACS), weighted MaxSAT (WCNF) and unsatisfiability proofs (DRAT).
• Bit-blastingBit-blasting decides formulas over fixed-width bit-vectors, the machine integers of programs and hardware, by translating every variable into one Boolean variable per bit and every operation into a Boolean circuit, then handing the resulting clauses to a SAT solver. Addition becomes a ripple-carry adder and multiplication a shift-and-add array of adders, encoded with the Tseitin transformation. It is complete and simple, and it is how SMT solvers handle bit-vectors after word-level simplification; its weak point is multiplication, whose circuits are large and hard for SAT solvers.
• ResolutionResolution is the inference rule that derives, from two clauses containing a variable with opposite signs, the clause of all their other literals: from C ∨ x and D ∨ ¬x, infer C ∨ D. It is sound and refutation complete for propositional logic, so a set of clauses is unsatisfiable exactly when the empty clause can be derived. Resolution is the proof system behind SAT solvers, whose runs on unsatisfiable formulas are resolution refutations, and behind first-order theorem provers and logic programming. Some formulas, such as the pigeonhole formulas, have only exponentially long resolution refutations.

1. [1]G. S. Tseitin, “On the complexity of derivation in propositional calculus”, in Studies in Constructive Mathematics and Mathematical Logic, Part II (1968; English translation 1970).
2. [2]D. A. Plaisted, S. Greenbaum, “A structure-preserving clause form translation”, Journal of Symbolic Computation 2 (1986).
3. [3]A. Urquhart, “Hard examples for resolution”, Journal of the ACM 34 (1987).
4. [4]S. A. Cook, “A short proof of the pigeon hole principle using extended resolution”, SIGACT News 8 (1976).
5. [5]N. Eén, A. Mishchenko, N. Sörensson, “Applying logic synthesis for speeding up SAT”, SAT, Lecture Notes in Computer Science 4501 (2007).
6. [6]S. D. Prestwich, “CNF encodings”, in A. Biere et al. (eds.), Handbook of Satisfiability, IOS Press (2nd ed., 2021).
7. [7]P. Jackson, D. Sheridan, “Clause form conversions for Boolean circuits”, SAT, Lecture Notes in Computer Science 3542 (2005).
8. [8]A. Kuehlmann, V. Paruthi, F. Krohm, M. K. Ganai, “Robust Boolean reasoning for equivalence checking and functional property verification”, IEEE Transactions on Computer-Aided Design 21 (2002).

last updated 28 September 2026