Documentation

Provenance.Tseitin

Tseitin CNF encoding of Boolean circuits #

This file formalises 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) :

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.

Instances For

def instReprLiteral.repr {X✝ : Type} [Repr X✝] :

Literal X✝ → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance instReprLiteral {X✝ : Type} [Repr X✝] :

Repr (Literal X✝)

Equations

instReprLiteral = { reprPrec := instReprLiteral.repr }

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

Evaluate a literal under a valuation.

Equations

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

Instances For

@[reducible, inline]

abbrev Clause (X : Type) :

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

Equations

Clause X = List (Literal X)

Instances For

def Clause.eval {X : Type} (c : Clause X) (v : X → 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

Instances For

@[reducible, inline]

abbrev CNF (X : Type) :

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

Equations

CNF X = List (Clause X)

Instances For

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

A CNF formula is satisfied iff every clause is satisfied.

Equations

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

Instances For

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

The Boolean function denoted by a CNF formula.

Equations

φ.toBoolFunc = φ.eval

Instances For

@[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 }]]

Instances For

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

Instances For

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

Instances For

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

Instances For

@[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.