Tseitin transformation

AbbreviationComplementary literal#✓fully proved

The complement of a literal \((x, b)\) with variable \(x\) and polarity \(b\) is the literal \((x, \lnot b)\): the same variable with the opposite polarity.

abbrev negLit (l : Nat × Bool) : Nat × Bool := (l.1, !l.2)

Used by 6

Used byTseitin clauses for a conjunction · Tseitin clauses for an implication · Tseitin clauses have at most three literals · Number of defining clauses in the Tseitin encoding · Tseitin clauses for a disjunction · Correctness invariant of the Tseitin encoding

DefinitionTseitin clauses for a conjunction#✓fully proved

For literals \(g\), \(a\) and \(b\), the defining clauses of the gate literal \(g\) for the conjunction of \(a\) and \(b\) are, in this order, the three clauses \(\lnot g \lor a\), \(\lnot g \lor b\) and \(g \lor \lnot a \lor \lnot b\), where \(\lnot \ell\) denotes the complementary literal of \(\ell\) (same variable, opposite polarity).

def andClauses (g a b : Nat × Bool) : CNF :=
  [[negLit g, a], [negLit g, b], [g, negLit a, negLit b]]

Uses 3 · Used by 4

Statement usesComplementary literal · CNF formula · CNF clause

Used byCorrectness invariant of the Tseitin encoding · Linear-time Tseitin builder · The linear-time Tseitin builder agrees with the reference encoding · Tseitin encoding with gates numbered from \(k\)

DefinitionTseitin clauses for a disjunction#✓fully proved

For literals \(g\), \(a\) and \(b\), the defining clauses of the gate literal \(g\) for the disjunction of \(a\) and \(b\) are the three clauses \(\lnot g \lor a \lor b\), \(g \lor \lnot a\) and \(g \lor \lnot b\), where \(\lnot \ell\) denotes the complementary literal of \(\ell\).

def orClauses (g a b : Nat × Bool) : CNF :=
  [[negLit g, a, b], [g, negLit a], [g, negLit b]]

Uses 3 · Used by 4

Statement usesComplementary literal · CNF formula · CNF clause

Used byCorrectness invariant of the Tseitin encoding · Linear-time Tseitin builder · The linear-time Tseitin builder agrees with the reference encoding · Tseitin encoding with gates numbered from \(k\)

DefinitionTseitin clauses for an implication#✓fully proved

For literals \(g\), \(a\) and \(b\), the defining clauses of the gate literal \(g\) for the implication from \(a\) to \(b\) are, in this order, the three clauses \(\lnot g \lor \lnot a \lor b\), \(g \lor a\) and \(g \lor \lnot b\), where \(\lnot \ell\) denotes the complementary literal of \(\ell\) (same variable, opposite polarity).

def impClauses (g a b : Nat × Bool) : CNF :=
  [[negLit g, negLit a, b], [g, a], [g, negLit b]]

Uses 3 · Used by 4

Statement usesComplementary literal · CNF formula · CNF clause

Used byCorrectness invariant of the Tseitin encoding · Linear-time Tseitin builder · The linear-time Tseitin builder agrees with the reference encoding · Tseitin encoding with gates numbered from \(k\)

DefinitionOne step of the Tseitin encoding#✓fully proved

Given a rule \(\mathit{cl}\) assigning to literals \(g\), \(a\), \(b\) a list of defining clauses, and the results \((a, C_A, k_A)\) and \((b, C_B, k_B)\) of encoding the two operands of a binary connective (each a literal, a clause list and a next unused gate number), the step returns the positive literal \(g\) of variable \(2k_B+1\), the clause list \(C_A\), then \(C_B\), then \(\mathit{cl}(g, a, b)\), and the next gate number \(k_B+1\).

def tseitinStep (cl : Nat × Bool → Nat × Bool → Nat × Bool → CNF)
    (ra rb : (Nat × Bool) × CNF × ℕ) : (Nat × Bool) × CNF × ℕ :=
  ((2 * rb.2.2 + 1, true), ra.2.1 ++ rb.2.1 ++ cl (2 * rb.2.2 + 1, true) ra.1 rb.1,
    rb.2.2 + 1)

Uses 2 · Used by 2

Statement usesCNF formula · CNF clause

Used byCorrectness invariant of the Tseitin encoding · Tseitin encoding with gates numbered from \(k\)

DefinitionOne step of the linear-time Tseitin builder#✓fully proved

Let \(c\) map a gate literal and two operand literals to a list of clauses, and let \((a, \varphi_A, k_A)\) and \((b, \varphi_B, k_B)\) be the results for the two operands, each a literal, a clause list and a next free gate number. The step returns the positive literal \(g\) of the variable \(2k_B + 1\), the clause list \(c(g, a, b)\) followed by \(\varphi_B\), and the next free gate number \(k_B + 1\). Neither \(\varphi_A\) nor \(k_A\) is used: in the builder, \(\varphi_B\) is the accumulator, which already holds both operands' clauses.

def accStep (cl : Nat × Bool → Nat × Bool → Nat × Bool → CNF)
    (ra rb : (Nat × Bool) × CNF × ℕ) : (Nat × Bool) × CNF × ℕ :=
  ((2 * rb.2.2 + 1, true), cl (2 * rb.2.2 + 1, true) ra.1 rb.1 ++ rb.2.1, rb.2.2 + 1)

Uses 2 · Used by 1

Statement usesCNF formula · CNF clause

Used byLinear-time Tseitin builder

DefinitionConnective count of a propositional formula#✓fully proved

For a propositional formula \(A\), built from atoms with the binary connectives \(\wedge\), \(\vee\) and \(\to\), the connective count of \(A\) is the number of occurrences of these connectives in \(A\). It is \(0\) for an atom, and for \(B \circ C\), with \(\circ\) one of \(\wedge\), \(\vee\) and \(\to\), it is the count of \(B\) plus the count of \(C\) plus \(1\).

def connectiveCount : Proposition Atom → ℕ
  | atom _ => 0
  | and A B => A.connectiveCount + B.connectiveCount + 1
  | or A B => A.connectiveCount + B.connectiveCount + 1
  | imp A B => A.connectiveCount + B.connectiveCount + 1

Used by 2

Used byNumber of clauses of the Tseitin CNF · Number of defining clauses in the Tseitin encoding

DefinitionTseitin encoding with gates numbered from \(k\)#✓fully proved

Fix a map \(\iota\) from atoms to natural numbers. Given a formula \(A\) and a gate number \(k\), the encoding returns a literal naming \(A\), a list of defining clauses and the next unused gate number. For an atom \(a\) it returns the positive literal of variable \(2\iota(a)\), no clauses, and \(k\). For \(A \circ B\) with \(\circ\) one of \(\wedge\), \(\vee\), \(\to\), it encodes \(A\) from gate \(k\), obtaining a literal \(a\), clauses \(C_A\) and a gate number \(k'\), then \(B\) from gate \(k'\), obtaining \(b\), \(C_B\) and \(k''\); it returns the positive literal \(g\) of variable \(2k''+1\), the clauses \(C_A\), then \(C_B\), then the three defining clauses of \(g\) for \(a \circ b\), and \(k''+1\).

Its list concatenations make it quadratic; the Tseitin CNF is computed by a linear-time builder that produces the same clauses in another order.

def tseitinAux (ι : Atom → ℕ) : Proposition Atom → ℕ → (Nat × Bool) × CNF × ℕ
  | atom a, k => ((2 * ι a, true), [], k)
  | and A B, k =>
    let ra := tseitinAux ι A k
    tseitinStep andClauses ra (tseitinAux ι B ra.2.2)
  | or A B, k =>
    let ra := tseitinAux ι A k
    tseitinStep orClauses ra (tseitinAux ι B ra.2.2)
  | imp A B, k =>
    let ra := tseitinAux ι A k
    tseitinStep impClauses ra (tseitinAux ι B ra.2.2)

Uses 6 · Used by 7

Statement usesTseitin clauses for a conjunction · Tseitin clauses for an implication · Tseitin clauses for a disjunction · One step of the Tseitin encoding · CNF formula · CNF clause

Used byTseitin correctness · Tseitin clauses have at most three literals · Number of clauses of the Tseitin CNF · Number of defining clauses in the Tseitin encoding · Correctness invariant of the Tseitin encoding · The linear-time Tseitin builder agrees with the reference encoding · The Tseitin CNF reorders the reference encoding

DefinitionLinear-time Tseitin builder#✓fully proved

Fix a map \(\iota\) from atoms to natural numbers. Given a formula \(A\), a gate number \(k\) and a clause list \(\mathit{acc}\), the builder returns a literal naming \(A\), a clause list and the next unused gate number. For an atom \(a\) it returns the positive literal of variable \(2\iota(a)\), the list \(\mathit{acc}\) unchanged, and \(k\). For \(A \circ B\) with \(\circ\) one of \(\wedge\), \(\vee\), \(\to\), it runs on \(A\) from gate \(k\) with accumulator \(\mathit{acc}\), obtaining a literal \(a\), a list \(L_A\) and a gate number \(k'\), then on \(B\) from gate \(k'\) with accumulator \(L_A\), obtaining \(b\), \(L_B\) and \(k''\); it returns the positive literal \(g\) of variable \(2k''+1\), the three defining clauses of \(g\) for \(a \circ b\) followed by \(L_B\), and \(k''+1\).

Unlike the reference Tseitin encoding, which concatenates the operands' clause lists, it prepends each gate's clauses to the accumulator, so it runs in linear time and the clauses come out in a different order.

def tseitinAcc (ι : Atom → ℕ) : Proposition Atom → ℕ → CNF → (Nat × Bool) × CNF × ℕ
  | atom a, k, acc => ((2 * ι a, true), acc, k)
  | and A B, k, acc =>
    let ra := tseitinAcc ι A k acc
    accStep andClauses ra (tseitinAcc ι B ra.2.2 ra.2.1)
  | or A B, k, acc =>
    let ra := tseitinAcc ι A k acc
    accStep orClauses ra (tseitinAcc ι B ra.2.2 ra.2.1)
  | imp A B, k, acc =>
    let ra := tseitinAcc ι A k acc
    accStep impClauses ra (tseitinAcc ι B ra.2.2 ra.2.1)

Uses 5 · Used by 3

Statement usesOne step of the linear-time Tseitin builder · Tseitin clauses for a conjunction · Tseitin clauses for an implication · Tseitin clauses for a disjunction · CNF formula

Used byTseitin CNF · The linear-time Tseitin builder agrees with the reference encoding · The Tseitin CNF reorders the reference encoding

TheoremThe linear-time Tseitin builder agrees with the reference encoding#✓fully proved

For every map \(\iota\) from atoms to natural numbers, every formula \(A\), every gate number \(k\) and every clause list \(\mathit{acc}\), the linear-time Tseitin builder run on \(A\) from gate \(k\) with accumulator \(\mathit{acc}\) returns the same literal naming \(A\) and the same next unused gate number as the reference Tseitin encoding of \(A\) with gates numbered from \(k\), and its clause list is \(X\) followed by \(\mathit{acc}\) for some list of clauses \(X\) that is a permutation of the defining clauses of the reference encoding.

theorem tseitinAcc_eq (ι : Atom → ℕ) (A : Proposition Atom) (k : ℕ) (acc : CNF) :
    ∃ X : CNF, X.Perm (tseitinAux ι A k).2.1 ∧
      tseitinAcc ι A k acc = ((tseitinAux ι A k).1, X ++ acc, (tseitinAux ι A k).2.2)

Uses 7 · Used by 1

Statement usesCNF formula · CNF clause · Linear-time Tseitin builder · Tseitin encoding with gates numbered from \(k\)

Proof usesTseitin clauses for a conjunction · Tseitin clauses for an implication · Tseitin clauses for a disjunction

Used byThe Tseitin CNF reorders the reference encoding

DefinitionTseitin CNF#✓fully proved

For a map \(\iota\) from atoms to natural numbers and a formula \(A\), run the linear-time Tseitin builder on \(A\) with gates numbered from \(0\) and the empty accumulator, obtaining a literal \(\ell\) naming \(A\) and a clause list \(C\). The Tseitin CNF of \(A\) is the unit clause \([\ell]\) followed by \(C\).

def tseitin (ι : Atom → ℕ) (A : Proposition Atom) : CNF :=
  let r := tseitinAcc ι A 0 []
  [r.1] :: r.2.1

Uses 3 · Used by 6

Statement usesCNF formula · CNF clause · Linear-time Tseitin builder

Used byEquisatisfiability of the Tseitin transformation · Tseitin correctness · Tseitin clauses have at most three literals · Number of clauses of the Tseitin CNF · Tseitin CNF with \(\bot\) false · The Tseitin CNF reorders the reference encoding

TheoremThe Tseitin CNF reorders the reference encoding#✓fully proved

For every map \(\iota\) from atoms to natural numbers and every formula \(A\), the Tseitin CNF of \(A\) is the unit clause whose literal is the literal naming \(A\) in the reference Tseitin encoding of \(A\) with gates numbered from \(0\), followed by a list of clauses that is a permutation of the defining clauses of that encoding.

theorem tseitin_eq (ι : Atom → ℕ) (A : Proposition Atom) :
    ∃ X : CNF, X.Perm (tseitinAux ι A 0).2.1 ∧ tseitin ι A = [(tseitinAux ι A 0).1] :: X

Uses 6 · Used by 3

Statement usesCNF formula · CNF clause · Tseitin CNF · Tseitin encoding with gates numbered from \(k\)

Proof usesLinear-time Tseitin builder · The linear-time Tseitin builder agrees with the reference encoding

Used byTseitin correctness · Tseitin clauses have at most three literals · Number of clauses of the Tseitin CNF

DefinitionTseitin CNF with \(\bot\) false#✓fully proved

For an atom type with a distinguished atom \(\bot\), a map \(\iota\) from atoms to natural numbers and a formula \(A\), this is the CNF consisting of the unit clause whose literal is the negative literal of variable \(2\iota(\bot)\), followed by the Tseitin CNF of \(A\) with respect to \(\iota\).

def tseitinBot [Bot Atom] (ι : Atom → ℕ) (A : Proposition Atom) : CNF :=
  [(2 * ι ⊥, false)] :: tseitin ι A

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · Tseitin CNF

Used byEquisatisfiability of the Tseitin transformation

27 fully proved

Size

TheoremNumber of defining clauses in the Tseitin encoding#✓fully proved

For every map \(\iota\) from atoms to natural numbers, every formula \(A\) and every gate number \(k\), the list of defining clauses produced by the Tseitin encoding of \(A\) with gates numbered from \(k\) has length \(3c\), where \(c\) is the number of binary connectives of \(A\).

theorem length_tseitinAux (ι : Atom → ℕ) (A : Proposition Atom) (k : ℕ) :
    (tseitinAux ι A k).2.1.length = 3 * A.connectiveCount

Uses 5 · Used by 1

Statement usesCNF formula · CNF clause · Connective count of a propositional formula · Tseitin encoding with gates numbered from \(k\)

Proof usesComplementary literal

Used byNumber of clauses of the Tseitin CNF

TheoremNumber of clauses of the Tseitin CNF#✓fully proved

For every proposition \(A\) and every map \(\iota\) from atoms to natural numbers, the Tseitin CNF of \(A\) with respect to \(\iota\), as a list of clauses counted with repetition, has length \(3c + 1\), where \(c\) is the number of binary connectives of \(A\): three defining clauses per connective plus the unit clause asserting \(A\).

theorem length_tseitin (ι : Atom → ℕ) (A : Proposition Atom) :
    (tseitin ι A).length = 3 * A.connectiveCount + 1

Uses 7

Statement usesCNF clause · Connective count of a propositional formula · Tseitin CNF

Proof usesCNF formula · Number of defining clauses in the Tseitin encoding · Tseitin encoding with gates numbered from \(k\) · The Tseitin CNF reorders the reference encoding

TheoremTseitin clauses have at most three literals#✓fully proved

For every proposition \(A\) and every map \(\iota\) from atoms to natural numbers, every clause of the Tseitin CNF of \(A\) with respect to \(\iota\) has at most three literals.

theorem length_le_three_of_mem_tseitin (ι : Atom → ℕ) (A : Proposition Atom)
    {C : CNFClause} (hC : C ∈ tseitin ι A) : C.length ≤ 3

Uses 6

Statement usesCNF formula · CNF clause · Tseitin CNF

Proof usesComplementary literal · Tseitin encoding with gates numbered from \(k\) · The Tseitin CNF reorders the reference encoding

Literal semantics and gate clauses

AbbreviationTruth value of a literal#✓fully proved

Let \(\sigma\) assign a Boolean value to every natural-number variable, and let \(\ell = (x, b)\) be a literal with variable \(x\) and polarity \(b\). The truth value of \(\ell\) under \(\sigma\) is true exactly when \(\sigma(x) = b\).

abbrev litVal (σ : ℕ → Bool) (l : Nat × Bool) : Bool := σ l.1 == l.2

Used by 3

Used byTseitin correctness · Tseitin encoding invariant · Correctness invariant of the Tseitin encoding

TheoremSatisfying a concatenation of CNF formulas#✓fully proved

For every assignment \(\sigma\) of Boolean values to the natural-number variables and all CNF formulas \(\varphi\) and \(\psi\), \(\sigma\) satisfies the formula consisting of the clauses of \(\varphi\) followed by those of \(\psi\) if and only if \(\sigma\) satisfies both \(\varphi\) and \(\psi\).

@[deprecated "use Cslib.Logic.PL.CNF.satisfies_append instead" (since := "2026-10-15")]
theorem satisfies_append {σ : ℕ → Bool} {φ ψ : CNF} :
    (φ ++ ψ).Satisfies σ ↔ φ.Satisfies σ ∧ ψ.Satisfies σ

Uses 4

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause

Proof usesSatisfaction of a clause

The invariant of one encoding step

DefinitionGate variables in a range#✓fully proved

For natural numbers \(k\) and \(k'\), a variable \(x \in \mathbb{N}\) is a gate in range \([k, k')\) if \(x = 2j + 1\) for some \(j \in \mathbb{N}\) with \(k \le j < k'\).

def IsGate (k k' x : ℕ) : Prop := ∃ j, k ≤ j ∧ j < k' ∧ x = 2 * j + 1

Used by 4

Used byAllowed variables for a gate range · Tseitin correctness · Tseitin encoding invariant · Correctness invariant of the Tseitin encoding

DefinitionAllowed variables for a gate range#✓fully proved

For natural numbers \(k\) and \(k'\), a variable \(x \in \mathbb{N}\) is allowed for the gate range \([k, k')\) if \(x\) is even (it names an atom) or \(x\) is a gate in range \([k, k')\), that is, \(x = 2j + 1\) for some \(j \in \mathbb{N}\) with \(k \le j < k'\).

def Allowed (k k' x : ℕ) : Prop := (∃ n, x = 2 * n) ∨ IsGate k k' x

Uses 1 · Used by 2

Statement usesGate variables in a range

Used byTseitin encoding invariant · Correctness invariant of the Tseitin encoding

DefinitionFunctions of the atom variables#✓fully proved

A function \(f\) from assignments \(\sigma : \mathbb{N} \to \mathrm{Bool}\) to Booleans depends only on the atom variables if \(f(\sigma) = f(\tau)\) for all assignments \(\sigma\) and \(\tau\) with \(\sigma(2n) = \tau(2n)\) for every \(n \in \mathbb{N}\).

def AtomDependent (val : (ℕ → Bool) → Bool) : Prop :=
  ∀ σ τ : ℕ → Bool, (∀ n, σ (2 * n) = τ (2 * n)) → val σ = val τ

Used by 1

Used byCorrectness invariant of the Tseitin encoding

StructureTseitin encoding invariant#✓fully proved

Let \(k\) be a natural number, let \(r = (\ell, \Phi, k')\) consist of a literal \(\ell\), a CNF formula \(\Phi\) and a natural number \(k'\), and let \(v\) map each assignment of Boolean values to the natural-number variables to a Boolean value. Call a variable a gate in range if it equals \(2j + 1\) for some \(j\) with \(k \le j < k'\). The invariant holds for \(k\), \(r\) and \(v\) when \(k \le k'\); the variable of \(\ell\) and every variable occurring in a literal of \(\Phi\) is even or a gate in range; every assignment \(\sigma\) that satisfies \(\Phi\) gives \(\ell\) the value \(v(\sigma)\); and for every assignment \(\sigma\) there is an assignment \(\tau\) that agrees with \(\sigma\) on every variable that is not a gate in range, satisfies \(\Phi\) and gives \(\ell\) the value \(v(\sigma)\).

Here \(r\) is meant to be the result (literal, clauses, next gate) of encoding a proposition with gates numbered from \(k\), and \(v\) the value of that proposition.

structure Spec (k : ℕ) (r : (Nat × Bool) × CNF × ℕ) (val : (ℕ → Bool) → Bool) : Prop where
  le : k ≤ r.2.2
  allowed_lit : Allowed k r.2.2 r.1.1
  allowed_clauses : ∀ C ∈ r.2.1, ∀ l ∈ C, Allowed k r.2.2 l.1
  sound : ∀ σ, r.2.1.Satisfies σ → litVal σ r.1 = val σ
  complete : ∀ σ, ∃ τ, (∀ x, ¬ IsGate k r.2.2 x → τ x = σ x) ∧ r.2.1.Satisfies τ ∧
    litVal τ r.1 = val σ

Uses 6 · Used by 2

Statement usesAllowed variables for a gate range · Gate variables in a range · Truth value of a literal · CNF formula · Satisfaction of a CNF formula · CNF clause

Used byTseitin correctness · Correctness invariant of the Tseitin encoding

TheoremSatisfaction depends only on the occurring variables#✓fully proved

Let \(\varphi\) be a CNF formula and let \(\sigma\) and \(\tau\) be assignments of Boolean values to the natural-number variables that agree on every variable occurring in a literal of \(\varphi\). If \(\sigma\) satisfies \(\varphi\), then \(\tau\) satisfies \(\varphi\).

theorem satisfies_of_agree {φ : CNF} {σ τ : ℕ → Bool}
    (hagree : ∀ C ∈ φ, ∀ l ∈ C, σ l.1 = τ l.1) (hσ : φ.Satisfies σ) : φ.Satisfies τ

Uses 5 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause

Proof usesSatisfaction of a clause · Satisfaction of a literal

Used byCorrectness invariant of the Tseitin encoding

AbbreviationValue of a proposition read off the atom variables#✓fully proved

Given a map \(\iota\) from atoms to natural numbers, a proposition \(A\) and an assignment \(\sigma : \mathbb{N} \to \mathrm{Bool}\), this is the truth value of \(A\) under the valuation that gives each atom \(a\) the value \(\sigma(2\iota(a))\).

abbrev atomVal (ι : Atom → ℕ) (A : Proposition Atom) (σ : ℕ → Bool) : Bool :=
  A.evalBool (fun a ↦ σ (2 * ι a))

Uses 1 · Used by 2

Statement usesTruth-table evaluation

Used byTseitin correctness · Correctness invariant of the Tseitin encoding

TheoremCorrectness invariant of the Tseitin encoding#✓fully proved

Let \(\iota\) map atoms to natural numbers, let \(A\) be a proposition and \(k\) a natural number, and let \((\ell, \Phi, k')\) be the reference Tseitin encoding of \(A\) with gates numbered from \(k\): the literal naming \(A\), its defining clauses and the next unused gate number. For an assignment \(\sigma\) of Boolean values to the natural-number variables, let \(A[\sigma]\) be the truth value of \(A\) when each atom \(a\) gets the value \(\sigma(2\iota(a))\), and call a variable a gate in range if it equals \(2j + 1\) for some \(j\) with \(k \le j < k'\). Then \(k \le k'\); the variable of \(\ell\) and every variable occurring in a literal of \(\Phi\) is even or a gate in range; every assignment \(\sigma\) that satisfies \(\Phi\) gives \(\ell\) the value \(A[\sigma]\); and for every assignment \(\sigma\) there is an assignment \(\tau\) that agrees with \(\sigma\) on every variable that is not a gate in range, satisfies \(\Phi\) and gives \(\ell\) the value \(A[\sigma]\).

theorem spec_tseitinAux (ι : Atom → ℕ) (A : Proposition Atom) (k : ℕ) :
    Spec k (tseitinAux ι A k) (atomVal ι A)

Uses 19 · Used by 1

Statement usesTseitin encoding invariant · Value of a proposition read off the atom variables · Tseitin encoding with gates numbered from \(k\)

Proof usesAllowed variables for a gate range · Functions of the atom variables · Gate variables in a range · Tseitin clauses for a conjunction · Tseitin clauses for an implication · Truth value of a literal · Complementary literal · Tseitin clauses for a disjunction · Satisfaction depends only on the occurring variables · One step of the Tseitin encoding · CNF formula · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Truth-table evaluation

Used byTseitin correctness

Main theorems

TheoremTseitin correctness#✓fully proved

Let \(\iota\) be an injective map from atoms to natural numbers, let \(A\) be a proposition and let \(v\) be a valuation of the atoms. Then \(A\) is true under \(v\) if and only if some assignment \(\sigma : \mathbb{N} \to \mathrm{Bool}\) with \(\sigma(2\iota(a)) = v(a)\) for every atom \(a\) satisfies the Tseitin CNF of \(A\) with respect to \(\iota\).

theorem evalBool_iff_exists_satisfies_tseitin {ι : Atom → ℕ} (hι : Function.Injective ι)
    (A : Proposition Atom) (v : Atom → Bool) :
    A.evalBool v = true ↔
      ∃ σ : ℕ → Bool, (∀ a, σ (2 * ι a) = v a) ∧ (tseitin ι A).Satisfies σ

Uses 14 · Used by 1

Statement usesSatisfaction of a CNF formula · Truth-table evaluation · Tseitin CNF

Proof usesGate variables in a range · Tseitin encoding invariant · Value of a proposition read off the atom variables · Truth value of a literal · Correctness invariant of the Tseitin encoding · CNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Tseitin encoding with gates numbered from \(k\) · The Tseitin CNF reorders the reference encoding

Used byEquisatisfiability of the Tseitin transformation

TheoremEquisatisfiability of the Tseitin transformation#✓fully proved

Let the atoms have a distinguished atom \(\bot\), let \(\iota\) be an injective map from atoms to natural numbers and let \(A\) be a proposition. The Tseitin CNF of \(A\) with respect to \(\iota\), together with the unit clause making the variable \(2\iota(\bot)\) false, is satisfiable if and only if \(A\) is true under some valuation \(v\) of the atoms with \(v(\bot)\) false.

theorem cnfSat_tseitinBot_iff [Bot Atom] {ι : Atom → ℕ} (hι : Function.Injective ι)
    (A : Proposition Atom) :
    CNFSat (tseitinBot ι A) ↔ ∃ v : Atom → Bool, v ⊥ = false ∧ A.evalBool v = true

Uses 10

Statement usesSatisfiability of a CNF formula · Truth-table evaluation · Tseitin CNF with \(\bot\) false

Proof usesCNF formula · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause · Tseitin correctness · Tseitin CNF · Satisfiability means having a satisfying assignment

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.