Tseitin CNF encoding of Boolean circuits

This file formalizes the Tseitin transformation, which encodes a Boolean circuit c : Circuit X as an equisatisfiable CNF over the extended variable set X ⊕ Circuit X. Each sub-circuit becomes an auxiliary variable, and the CNF clauses encode aux(g) ↔ <gate operation on aux variables of children>.

The transformation is purely structural and produces a CNF whose size is linear in the size of the circuit. It is the standard pre-processing step used before feeding a Boolean formula to a SAT solver or a knowledge compiler (c2d, d4, DSHARP); see Section V-D step 3 of Sen, Maniu & Senellart, ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data.

The main correctness result is Circuit.tseitin_equisat: a circuit is satisfiable iff its Tseitin CNF encoding is satisfiable. The proof is the explicit bijection between models of the circuit and models of the CNF: each valuation v : X → Bool lifts uniquely to a (X ⊕ Circuit X) → Bool that satisfies the CNF iff c.eval v = true, and any model of the CNF restricted to the original variables is a model of the circuit.

Main definitions

• Literal X, Clause X, CNF X – syntactic CNF infrastructure with eval semantics.
• Circuit.gateClauses – per-gate Tseitin clauses encoding aux(c) ↔ ... (no recursion into sub-circuits).
• Circuit.tseitinClauses – the full recursive clause set covering every sub-circuit.
• Circuit.tseitin – the Tseitin CNF: gate clauses plus a unit clause asserting that the root's aux variable is true.
• Circuit.tseitinValuation – the canonical lift of a valuation v : X → Bool to (X ⊕ Circuit X) → Bool (aux variables receive their sub-circuit's evaluation under v).

Main results

• Circuit.tseitin_eval_tseitinValuation – CNF.eval c.tseitin (tseitinValuation v) = c.eval v: the lifted valuation always satisfies the per-gate clauses, and the root assertion exactly tracks the circuit's truth value.
• Circuit.tseitin_models_restrict – any model w of c.tseitin restricts (via Sum.inl) to a model of c.
• Circuit.tseitin_equisat – the bidirectional equisatisfiability theorem.

References

• Sen, Maniu & Senellart (Section V-D step 3)

structure Literal (X : Type) : Type

A literal: a variable together with a polarity flag. isPos = true means the positive literal var, isPos = false means the negative literal ¬var.

• var : X

  The variable underlying the literal.

• isPos : Bool

  Polarity: true for positive, false for negative.

@[instance_reducible]

instance instReprLiteral {X✝ : Type} [Repr X✝] : Repr (Literal X✝)

Equations

• instReprLiteral = { reprPrec := instReprLiteral.repr }

def instReprLiteral.repr {X✝ : Type} [Repr X✝] : Literal X✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Literal.eval {X : Type} (l : Literal X) (v : X → Bool) : Bool

Evaluate a literal under a valuation.

Equations

• l.eval v = if l.isPos = true then v l.var else !v l.var

@[reducible, inline]

abbrev Clause (X : Type) : Type

A clause: a disjunction of literals, represented as a List. The empty clause is unsatisfiable.

Equations

• Clause X = List (Literal X)

def Clause.eval {X : Type} (c : Clause X) (v : X → Bool) : Bool

A clause is satisfied iff some literal in it evaluates to true.

Equations

• c.eval v = List.any c fun (l : Literal X) => l.eval v

@[reducible, inline]

abbrev CNF (X : Type) : Type

A CNF formula: a conjunction of clauses. The empty conjunction is satisfied vacuously (equal to true).

Equations

• CNF X = List (Clause X)

def CNF.eval {X : Type} (φ : CNF X) (v : X → Bool) : Bool

A CNF formula is satisfied iff every clause is satisfied.

Equations

• φ.eval v = List.all φ fun (c : Clause X) => c.eval v

def CNF.toBoolFunc {X : Type} (φ : CNF X) : BoolFunc X

The Boolean function denoted by a CNF formula.

Equations

• φ.toBoolFunc = φ.eval

@[simp]

theorem CNF.eval_nil {X : Type} (v : X → Bool) : eval [] v = true

@[simp]

theorem CNF.eval_cons {X : Type} (c : Clause X) (φ : CNF X) (v : X → Bool) : eval (c :: φ) v = (c.eval v && φ.eval v)

theorem CNF.eval_append {X : Type} (φ ψ : CNF X) (v : X → Bool) : (φ ++ ψ).eval v = (φ.eval v && ψ.eval v)

def Circuit.gateClauses {X : Type} : Circuit X → CNF (X ⊕ Circuit X)

Per-gate Tseitin clauses encoding aux(c) ↔ <gate operation on aux of children>. Does not recurse into sub-circuits – see Circuit.tseitinClauses for the full recursive collection.

Equations

• One or more equations did not get rendered due to their size.
• (Circuit.const true).gateClauses = [[{ var := Sum.inr (Circuit.const true), isPos := true }]]
• (Circuit.const false).gateClauses = [[{ var := Sum.inr (Circuit.const false), isPos := false }]]
• c'.not.gateClauses = [[{ var := Sum.inr c'.not, isPos := false }, { var := Sum.inr c', isPos := false }], [{ var := Sum.inr c'.not, isPos := true }, { var := Sum.inr c', isPos := true }]]

def Circuit.tseitinClauses {X : Type} : Circuit X → CNF (X ⊕ Circuit X)

The full recursive Tseitin clause set: per-gate clauses for the current node, plus all the clauses for its sub-circuits.

Equations

• (Circuit.const b).tseitinClauses = (Circuit.const b).gateClauses
• (Circuit.var x_1).tseitinClauses = (Circuit.var x_1).gateClauses
• c'.not.tseitinClauses = c'.not.gateClauses ++ c'.tseitinClauses
• (c₁.and c₂).tseitinClauses = (c₁.and c₂).gateClauses ++ c₁.tseitinClauses ++ c₂.tseitinClauses
• (c₁.or c₂).tseitinClauses = (c₁.or c₂).gateClauses ++ c₁.tseitinClauses ++ c₂.tseitinClauses

def Circuit.tseitin {X : Type} (c : Circuit X) : CNF (X ⊕ Circuit X)

The Tseitin CNF encoding: a unit clause asserting that the root's aux variable is true, followed by all per-gate sub-circuit clauses.

Equations

• c.tseitin = [{ var := Sum.inr c, isPos := true }] :: c.tseitinClauses

def Circuit.tseitinValuation {X : Type} (v : X → Bool) : X ⊕ Circuit X → Bool

The canonical lift of an original-variable valuation v : X → Bool to the Tseitin variable space X ⊕ Circuit X: original variables map to their v-value, aux variables map to the corresponding sub-circuit's evaluation under v.

Equations

• Circuit.tseitinValuation v (Sum.inl x_1) = v x_1
• Circuit.tseitinValuation v (Sum.inr c) = c.eval v

@[simp]

theorem Circuit.tseitinValuation_inl {X : Type} (v : X → Bool) (x : X) : tseitinValuation v (Sum.inl x) = v x

@[simp]

theorem Circuit.tseitinValuation_inr {X : Type} (v : X → Bool) (c : Circuit X) : tseitinValuation v (Sum.inr c) = c.eval v

Forward direction: every model of the circuit lifts to a model of

the Tseitin CNF.

theorem Circuit.tseitinClauses_eval_tseitinValuation {X : Type} (c : Circuit X) (v : X → Bool) : c.tseitinClauses.eval (tseitinValuation v) = true

Every per-gate Tseitin clause is satisfied by the lifted valuation. The proof is structural induction on the circuit, with each case discharged by case analysis on the Boolean value of the children.

theorem Circuit.tseitin_eval_tseitinValuation {X : Type} (c : Circuit X) (v : X → Bool) : c.tseitin.eval (tseitinValuation v) = c.eval v

The Tseitin CNF evaluates under the lifted valuation to exactly the circuit's truth value: the unit root clause [(aux(c), +)] is satisfied iff c.eval v = true, and all other clauses are tautologically satisfied under the lift.

Backward direction: every model of the Tseitin CNF restricts to a

model of the circuit.

theorem Circuit.tseitinClauses_imp_root {X : Type} (c : Circuit X) (w : X ⊕ Circuit X → Bool) (hw : c.tseitinClauses.eval w = true) : w (Sum.inr c) = c.eval fun (x : X) => w (Sum.inl x)

If the per-gate Tseitin clauses for a circuit c are all satisfied by a valuation w, then w correctly evaluates c's root aux variable to c.eval (w ∘ Sum.inl). Proved by induction on c: each gate's clauses encode the iff aux(c) ↔ <gate on children's aux>, and the IH supplies the children's correctness.

theorem Circuit.tseitin_models_restrict {X : Type} (c : Circuit X) (w : X ⊕ Circuit X → Bool) (hw : c.tseitin.eval w = true) : (c.eval fun (x : X) => w (Sum.inl x)) = true

Any model w of the full Tseitin CNF c.tseitin restricts (via Sum.inl) to a model of the original circuit c. The root unit clause forces w (Sum.inr c) = true, and the gate clauses force this to equal c.eval (w ∘ Sum.inl) via tseitinClauses_imp_root.

Equisatisfiability

theorem Circuit.tseitin_equisat {X : Type} (c : Circuit X) : (∃ (v : X → Bool), c.eval v = true) ↔ ∃ (w : X ⊕ Circuit X → Bool), c.tseitin.eval w = true

Tseitin equisatisfiability. A Boolean circuit c : Circuit X is satisfiable iff its Tseitin CNF encoding c.tseitin : CNF (X ⊕ Circuit X) is satisfiable. The forward direction lifts a circuit-satisfying valuation v via tseitinValuation v; the backward direction restricts a CNF-satisfying valuation w via Sum.inl.

Home · Documentation · Publications · Contributors · Source · Cite