3-satisfiability

DefinitionThree-literal clause test#✓fully proved

For a CNF formula \(\varphi\), this Boolean test holds exactly when every clause of \(\varphi\) has at most three literals.

def is3 (φ : CNF) : Bool := φ.all fun C => decide (C.length ≤ 3)

Uses 2 · Used by 9

Statement usesCNF formula · CNF clause

Used byAnswer of the SAT host · The SAT verifier is polynomial-time · The TM2 SAT verifier · Answer of the SAT host with the three-literal filter · 3SAT is in NP · The SAT-to-3SAT translation yields clauses of length at most three · Correctness of the clause-length filter · Correctness of the SAT-to-3SAT reduction on bit strings · The 3SAT decision problem

DefinitionThe 3SAT decision problem#✓fully proved

3SAT accepts a bit string \(x\) exactly when \(x\) is the binary code of a satisfiable CNF formula in which every clause has at most three literals.

noncomputable def sat3Dec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  decide (∃ φ : CNF, encodeCNF φ = x ∧ is3 φ = true ∧ CNFSat φ)

Uses 5 · Used by 5

Statement usesThree-literal clause test · Length-prefixed binary code of a CNF formula · CNF formula · Satisfiability of a CNF formula · Decision problems

Used by3SAT is in NP · Correctness of the SAT-to-3SAT reduction on bit strings · SAT reduces to 3SAT · 3SAT is NP-complete · 3SAT is NP-hard

DefinitionRenaming of the original variables#✓fully proved

Variable index \(n\) is renamed to \(2n\), so the variables of the original formula get even indices.

def ren (n : ℕ) : ℕ := 2 * n

Used by 9

Used byCompleteness of the chain of one clause · Soundness of the chain of one clause · Completeness of the tail of a chain · Soundness of the tail of a chain · The SAT-to-3SAT translation preserves satisfiability · The lifted assignment on renamed variables · Renaming a literal · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation

DefinitionFresh variable indices#✓fully proved

For \(u \in \mathbb{N}\), the \(u\)-th fresh variable has index \(2^{u+1} + 1\), an odd number.

def fresh (u : ℕ) : ℕ := 2 ^ (u + 1) + 1

Used by 18

Used byThe chain of clauses replacing one clause · Completeness of the chain of one clause · Soundness of the chain of one clause · The tail of a clause chain · Completeness of the tail of a chain · Soundness of the tail of a chain · Code of a fresh literal · Binary representation of a fresh name · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · Chain clauses have at most three literals · Chain-tail clauses have at most three literals · The lifted assignment on fresh variables · Output clause of one literal · One literal of the emitter · Closing an output clause in the SAT-to-3SAT emitter · Completeness of the auxiliary 3SAT translation · Walking a whole clause gives its chain

DefinitionRenaming a literal#✓fully proved

The literal with variable index \(n\) and polarity \(b\) is renamed to the literal with variable index \(2n\) and the same polarity \(b\).

def renLit (l : ℕ × Bool) : ℕ × Bool := (ren l.1, l.2)

Uses 1 · Used by 13

Statement usesRenaming of the original variables

Used byThe chain of clauses replacing one clause · Completeness of the chain of one clause · Soundness of the chain of one clause · The tail of a clause chain · Completeness of the tail of a chain · Soundness of the tail of a chain · Code of a renamed literal · Chain clauses have at most three literals · Chain-tail clauses have at most three literals · Output clause of one literal · One literal of the emitter · Copying a renamed name · Walking a whole clause gives its chain

DefinitionThe tail of a clause chain#✓fully proved

Write \(y_v\) for the variable with index \(2^{v+1} + 1\) (the \(v\)-th fresh variable), \(\ell'\) for a literal \(\ell\) whose variable index \(n\) is replaced by \(2n\) with the same polarity, and \(z \ominus j\) for \(\max(z - j, 0)\). Given literals \(\ell_1, \dots, \ell_m\) and a natural number \(z\), the result is the empty formula if \(m = 0\), and otherwise the \(m\) clauses \((\neg y_{z \ominus (i - 1)} \lor \ell_i' \lor y_{z \ominus i})\) for \(i = 1, \dots, m - 1\), followed by \((\neg y_{z \ominus (m - 1)} \lor \ell_m')\).

Here \(z\) is the fresh number of the variable asserted by the clause before the tail; fresh numbers decrease along the chain.

def chainTail : List (ℕ × Bool) → ℕ → CNF
  | [], _ => []
  | [l], z => [[(fresh z, false), renLit l]]
  | l :: l' :: ls, z =>
      [(fresh z, false), renLit l, (fresh (z - 1), true)] :: chainTail (l' :: ls) (z - 1)

Uses 4 · Used by 8

Statement usesFresh variable indices · Renaming a literal · CNF formula · CNF clause

Used byThe chain of clauses replacing one clause · Completeness of the chain of one clause · Soundness of the chain of one clause · Completeness of the tail of a chain · Soundness of the tail of a chain · Chain clauses have at most three literals · Chain-tail clauses have at most three literals · Walking a whole clause gives its chain

DefinitionThe chain of clauses replacing one clause#✓fully proved

Write \(y_v\) for the variable with index \(2^{v+1} + 1\) (the \(v\)-th fresh variable) and \(\ell'\) for a literal \(\ell\) whose variable index \(n\) is replaced by \(2n\), with the same polarity. Given a clause \(C\) and a natural number \(u\), the empty clause is replaced by the empty clause alone, a one-literal clause \(\ell_1\) by the clause \(\ell_1'\), and a clause \(\ell_1 \lor \dots \lor \ell_k\) with \(k \ge 2\) by the \(k\) clauses \((\ell_1' \lor y_{u+k-2})\), then \((\neg y_{u+k-i} \lor \ell_i' \lor y_{u+k-i-1})\) for \(i = 2, \dots, k - 1\), then \((\neg y_u \lor \ell_k')\). A clause of length \(k \ge 2\) thus uses the fresh numbers \(u\) to \(u + k - 2\).

def chain : CNFClause → ℕ → CNF
  | [], _ => [[]]
  | [l], _ => [[renLit l]]
  | l :: l' :: ls, u =>
      [renLit l, (fresh (u + ls.length), true)] :: chainTail (l' :: ls) (u + ls.length)

Uses 5 · Used by 11

Statement usesThe tail of a clause chain · Fresh variable indices · Renaming a literal · CNF formula · CNF clause

Used byCompleteness of the chain of one clause · Soundness of the chain of one clause · The 3SAT emitter processes one clause · The 3SAT emitter processes a whole formula · Chain clauses have at most three literals · Clauses of the auxiliary 3SAT translation have at most three literals · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Clause-by-clause translation with a fresh-number counter · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation · Walking a whole clause gives its chain

DefinitionFresh variables reserved for a clause#✓fully proved

The number of fresh variables reserved for a CNF clause \(C\) in the SAT-to-3SAT translation: \(k - 1\) if \(C\) has \(k \ge 1\) literals, and \(0\) if \(C\) is empty.

def used (C : CNFClause) : ℕ := C.length - 1

Uses 1 · Used by 6

Statement usesCNF clause

Used byCompleteness of the chain of one clause · The 3SAT emitter processes one clause · The 3SAT emitter processes a whole formula · Values of the fresh variables in the 3SAT translation · Clause-by-clause translation with a fresh-number counter · Completeness of the auxiliary 3SAT translation

DefinitionClause-by-clause translation with a fresh-number counter#✓fully proved

For a CNF formula this returns a pair \((N, \psi)\) of a natural number \(N\) and a CNF formula \(\psi\). The empty formula gives \(N = 0\) and \(\psi\) empty. A formula with first clause \(C\) and remaining clauses \(\varphi'\), whose pair is \((N', \psi')\), gives \(N = N' + \max(|C| - 1, 0)\) and, as \(\psi\), the chain of clauses replacing \(C\) with fresh numbers from \(N'\) on, followed by the clauses of \(\psi'\).

Fresh numbers are thus handed out from the last clause backwards, and \(N\) is the next free one.

def to3Aux : CNF → ℕ × CNF
  | [] => (0, [])
  | C :: φ => let r := to3Aux φ; (r.1 + used C, chain C r.1 ++ r.2)

Uses 4 · Used by 9

Statement usesThe chain of clauses replacing one clause · Fresh variables reserved for a clause · CNF formula · CNF clause

Used byThe SAT-to-3SAT translation preserves satisfiability · The 3SAT emitter processes a whole formula · Values of the fresh variables in the 3SAT translation · The SAT-to-3SAT translation yields clauses of length at most three · Clauses of the auxiliary 3SAT translation have at most three literals · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · The SAT-to-3SAT translation · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation

DefinitionThe SAT-to-3SAT translation#✓fully proved

For a CNF formula with clauses \(C_1, \dots, C_m\), the translation is the concatenation, in order, of the chains of clauses replacing \(C_1, \dots, C_m\), where the chain for \(C_i\) uses fresh numbers from \(u_i = \sum_{j > i} \max(|C_j| - 1, 0)\) on.

def to3 (φ : CNF) : CNF := (to3Aux φ).2

Uses 2 · Used by 8

Statement usesClause-by-clause translation with a fresh-number counter · CNF formula

Used byThe SAT-to-3SAT translation preserves satisfiability · The SAT-to-3SAT emitter · The 3SAT emitter processes a whole formula · The SAT-to-3SAT reduction is polynomial-time · The SAT-to-3SAT translation yields clauses of length at most three · The SAT-to-3SAT reduction on bit strings · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionThe SAT-to-3SAT reduction on bit strings#✓fully proved

A bit string that decodes, with no bits left over, to a CNF formula \(\varphi\) is sent to the binary code of the SAT-to-3SAT translation of \(\varphi\); any other bit string is sent to the empty string.

def reduce3 (x : List Bool) : List Bool :=
  match decodeCNF x with
  | some φ => encodeCNF (to3 φ)
  | none => []

Uses 4 · Used by 3

Statement usesThe SAT-to-3SAT translation · Decoding a complete length-prefixed CNF formula · Length-prefixed binary code of a CNF formula · CNF formula

Used byThe SAT-to-3SAT reduction is polynomial-time · Correctness of the SAT-to-3SAT reduction on bit strings · SAT reduces to 3SAT

TheoremChain-tail clauses have at most three literals#✓fully proved

For every clause \(C\) and natural number \(z\), every clause of \(\mathrm{chainTail}(C, z)\) has at most three literals.

theorem length_le_three_of_mem_chainTail :
    ∀ {ls : CNFClause} {z : ℕ}, ∀ D ∈ chainTail ls z, D.length ≤ 3

Uses 5 · Used by 1

Statement usesThe tail of a clause chain · CNF formula · CNF clause

Proof usesFresh variable indices · Renaming a literal

Used byChain clauses have at most three literals

TheoremChain clauses have at most three literals#✓fully proved

For every clause \(C\) and natural number \(u\), every clause of \(\mathrm{chain}(C, u)\) has at most three literals.

theorem length_le_three_of_mem_chain {C : CNFClause} {u : ℕ} :
    ∀ D ∈ chain C u, D.length ≤ 3

Uses 7 · Used by 1

Statement usesThe chain of clauses replacing one clause · CNF formula · CNF clause

Proof usesThe tail of a clause chain · Fresh variable indices · Chain-tail clauses have at most three literals · Renaming a literal

Used byClauses of the auxiliary 3SAT translation have at most three literals

TheoremClauses of the auxiliary 3SAT translation have at most three literals#✓fully proved

For every CNF formula \(\varphi\), every clause of the clause list produced by the auxiliary SAT-to-3SAT translation of \(\varphi\) (which replaces each clause by its chain of clauses with fresh variables) has at most three literals.

theorem length_le_three_of_mem_to3Aux : ∀ {φ : CNF}, ∀ D ∈ (to3Aux φ).2, D.length ≤ 3

Uses 5 · Used by 1

Statement usesClause-by-clause translation with a fresh-number counter · CNF formula · CNF clause

Proof usesThe chain of clauses replacing one clause · Chain clauses have at most three literals

Used byThe SAT-to-3SAT translation yields clauses of length at most three

TheoremThe SAT-to-3SAT translation yields clauses of length at most three#✓fully proved

For every CNF formula \(\varphi\), every clause of the translation \(\mathrm{to3}(\varphi)\) has at most three literals.

theorem is3_to3 (φ : CNF) : is3 (to3 φ) = true

Uses 6 · Used by 1

Statement usesThree-literal clause test · The SAT-to-3SAT translation · CNF formula

Proof usesClauses of the auxiliary 3SAT translation have at most three literals · Clause-by-clause translation with a fresh-number counter · CNF clause

Used byCorrectness of the SAT-to-3SAT reduction on bit strings

TheoremSoundness of the tail of a chain#✓fully proved

Let \(C\) be a nonempty clause and \(z\) a natural number. If an assignment \(v'\) satisfies every clause of \(\mathrm{chainTail}(C, z)\) and gives the fresh variable \(\mathrm{fresh}(z)\) the value true, then the assignment \(n \mapsto v'(2n)\) satisfies \(C\).

theorem chainTail_sound {v' : ℕ → Bool} {ls : CNFClause} :
    ∀ {l : ℕ × Bool} {z : ℕ}, CNF.Satisfies v' (chainTail (l :: ls) z) →
      v' (fresh z) = true → CNFClause.Satisfies (fun n => v' (ren n)) (l :: ls)

Uses 9 · Used by 1

Statement usesThe tail of a clause chain · Fresh variable indices · Renaming of the original variables · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause

Proof usesRenaming a literal · CNF formula · Satisfaction of a literal

Used bySoundness of the chain of one clause

TheoremSoundness of the chain of one clause#✓fully proved

Let \(C\) be a clause and \(u\) a natural number. If an assignment \(v'\) satisfies every clause of \(\mathrm{chain}(C, u)\), then the assignment \(n \mapsto v'(2n)\) satisfies \(C\).

theorem chain_sound {v' : ℕ → Bool} {C : CNFClause} {u : ℕ}
    (h : CNF.Satisfies v' (chain C u)) : CNFClause.Satisfies (fun n => v' (ren n)) C

Uses 11 · Used by 1

Statement usesThe chain of clauses replacing one clause · Renaming of the original variables · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause

Proof usesThe tail of a clause chain · Soundness of the tail of a chain · Fresh variable indices · Renaming a literal · CNF formula · Satisfaction of a literal

Used bySoundness of the auxiliary 3SAT translation

TheoremSoundness of the auxiliary 3SAT translation#✓fully proved

For every assignment \(v' : \mathbb{N} \to \mathrm{Bool}\) and every CNF formula \(\varphi\), if \(v'\) satisfies the clause list produced by the auxiliary SAT-to-3SAT translation of \(\varphi\), then the assignment \(n \mapsto v'(2n)\) satisfies \(\varphi\).

theorem to3Aux_sound {v' : ℕ → Bool} :
    ∀ {φ : CNF}, CNF.Satisfies v' (to3Aux φ).2 → CNF.Satisfies (fun n => v' (ren n)) φ

Uses 8 · Used by 1

Statement usesRenaming of the original variables · Clause-by-clause translation with a fresh-number counter · CNF formula · Satisfaction of a CNF formula

Proof usesThe chain of clauses replacing one clause · Soundness of the chain of one clause · CNF clause · Satisfaction of a clause

Used byThe SAT-to-3SAT translation preserves satisfiability

TheoremCompleteness of the tail of a chain#✓fully proved

Let \(v\) and \(v'\) be assignments with \(v'(2n) = v(n)\) for every \(n\), let \(C\) be a nonempty clause with \(m + 1\) literals and let \(z\) be a natural number. Suppose that for every \(j \le m\), \(v'\) gives the fresh variable \(\mathrm{fresh}(z - j)\) the value true exactly when \(v\) satisfies some literal of the clause obtained from \(C\) by dropping its first \(j\) literals, where \(z - j\) is truncated subtraction (\(0\) when \(j > z\)). Then \(v'\) satisfies every clause of \(\mathrm{chainTail}(C, z)\).

theorem chainTail_complete {v v' : ℕ → Bool} (hv : ∀ n, v' (ren n) = v n) {ls : CNFClause} :
    ∀ {l : ℕ × Bool} {z : ℕ},
      (∀ j ≤ ls.length, v' (fresh (z - j)) = clauseSatisfied v ((l :: ls).drop j)) →
      CNF.Satisfies v' (chainTail (l :: ls) z)

Uses 9 · Used by 1

Statement usesBoolean clause satisfaction check · The tail of a clause chain · Fresh variable indices · Renaming of the original variables · Satisfaction of a CNF formula · CNF clause

Proof usesRenaming a literal · CNF formula · Satisfaction of a clause

Used byCompleteness of the chain of one clause

TheoremCompleteness of the chain of one clause#✓fully proved

Let \(v\) and \(v'\) be assignments with \(v'(2n) = v(n)\) for every \(n\), let \(C\) be a clause and \(u\) a natural number, and write \(k = \mathrm{used}(C)\). Suppose that \(v\) satisfies \(C\), and that for every \(w\) with \(u \le w < u + k\), \(v'\) gives the fresh variable \(\mathrm{fresh}(w)\) the value true exactly when \(v\) satisfies some literal of the clause obtained from \(C\) by dropping its first \(u + k - w\) literals. Then \(v'\) satisfies every clause of \(\mathrm{chain}(C, u)\).

theorem chain_complete {v v' : ℕ → Bool} (hv : ∀ n, v' (ren n) = v n) {C : CNFClause} {u : ℕ}
    (hC : CNFClause.Satisfies v C)
    (hz : ∀ w, u ≤ w → w < u + used C →
      v' (fresh w) = clauseSatisfied v (C.drop (u + used C - w))) :
    CNF.Satisfies v' (chain C u)

Uses 13 · Used by 1

Statement usesBoolean clause satisfaction check · The chain of clauses replacing one clause · Fresh variable indices · Renaming of the original variables · Fresh variables reserved for a clause · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause

Proof usesThe tail of a clause chain · Completeness of the tail of a chain · Renaming a literal · CNF formula · Satisfaction of a literal

Used byCompleteness of the auxiliary 3SAT translation

DefinitionValues of the fresh variables in the 3SAT translation#✓fully proved

For an assignment \(v : \mathbb{N} \to \mathrm{Bool}\), a CNF formula \(\varphi\) and a natural number \(w\), the value \(f_v(\varphi, w)\) is defined by recursion on \(\varphi\). For the empty formula it is false. For a formula with first clause \(C\) and remaining clauses \(\varphi'\), let \(N'\) be the next free fresh number of the clause-by-clause translation of \(\varphi'\), and let \(k = \max(|C| - 1, 0)\) be the number of fresh variables reserved for \(C\). If \(w < N'\), then \(f_v(\varphi, w)\) is \(f_v(\varphi', w)\); otherwise \(f_v(\varphi, w)\) is true exactly when \(v\) satisfies some literal of the clause obtained from \(C\) by dropping its first \(N' + k - w\) literals, where the subtraction is truncated at \(0\).

The chain of clauses replacing \(C\) uses the fresh numbers \(N'\) to \(N' + k - 1\), so for these \(w\) the value records whether \(v\) satisfies one of the last \(w - N' + 1\) literals of \(C\).

def freshVal (v : ℕ → Bool) : CNF → ℕ → Bool
  | [], _ => false
  | C :: φ, w =>
      if w < (to3Aux φ).1 then freshVal v φ w
      else clauseSatisfied v (C.drop ((to3Aux φ).1 + used C - w))

Uses 5 · Used by 4

Statement usesBoolean clause satisfaction check · Clause-by-clause translation with a fresh-number counter · Fresh variables reserved for a clause · CNF formula · CNF clause

Used byLifting an assignment to the 3SAT translation · The lifted assignment on fresh variables · The lifted assignment on renamed variables · Completeness of the auxiliary 3SAT translation

TheoremCompleteness of the auxiliary 3SAT translation#✓fully proved

Let \(v, v' : \mathbb{N} \to \mathrm{Bool}\) be assignments with \(v'(2n) = v(n)\) for every \(n\), let \(\varphi\) be a CNF formula satisfied by \(v\), and let \(N\) be the next free fresh number of the auxiliary SAT-to-3SAT translation of \(\varphi\). If for every \(w < N\) the assignment \(v'\) gives fresh variable number \(w\), the variable \(2^{w+1} + 1\), the fresh-variable value of \(w\) built from \(v\) and \(\varphi\), then \(v'\) satisfies the clause list produced by the auxiliary translation of \(\varphi\).

theorem to3Aux_complete {v v' : ℕ → Bool} (hv : ∀ n, v' (ren n) = v n) :
    ∀ {φ : CNF}, CNF.Satisfies v φ → (∀ w < (to3Aux φ).1, v' (fresh w) = freshVal v φ w) →
      CNF.Satisfies v' (to3Aux φ).2

Uses 12 · Used by 1

Statement usesFresh variable indices · Values of the fresh variables in the 3SAT translation · Renaming of the original variables · Clause-by-clause translation with a fresh-number counter · CNF formula · Satisfaction of a CNF formula

Proof usesBoolean clause satisfaction check · The chain of clauses replacing one clause · Completeness of the chain of one clause · Fresh variables reserved for a clause · CNF clause · Satisfaction of a clause

Used byThe SAT-to-3SAT translation preserves satisfiability

DefinitionLifting an assignment to the 3SAT translation#✓fully proved

Given an assignment \(v : \mathbb{N} \to \mathrm{Bool}\) and a CNF formula \(\varphi\), the lifted assignment sends an even variable \(n\) to \(v(n/2)\) and an odd variable \(n\) to the fresh-variable value built from \(v\) and \(\varphi\) at the number \(\lfloor \log_2 (n - 1) \rfloor - 1\), where \(\lfloor \log_2 0 \rfloor\) is taken to be \(0\) and subtraction is truncated at \(0\).

def lift (v : ℕ → Bool) (φ : CNF) (n : ℕ) : Bool :=
  if n % 2 = 0 then v (n / 2) else freshVal v φ (Nat.log2 (n - 1) - 1)

Uses 2 · Used by 3

Statement usesValues of the fresh variables in the 3SAT translation · CNF formula

Used byThe SAT-to-3SAT translation preserves satisfiability · The lifted assignment on fresh variables · The lifted assignment on renamed variables

TheoremThe lifted assignment on renamed variables#✓fully proved

For every assignment \(v : \mathbb{N} \to \mathrm{Bool}\), every CNF formula \(\varphi\) and every \(n \in \mathbb{N}\), the assignment lifted from \(v\) for the 3SAT translation of \(\varphi\) gives the renamed variable \(2n\) the value \(v(n)\).

theorem lift_ren (v : ℕ → Bool) (φ : CNF) (n : ℕ) : lift v φ (ren n) = v n

Uses 4 · Used by 1

Statement usesLifting an assignment to the 3SAT translation · Renaming of the original variables · CNF formula

Proof usesValues of the fresh variables in the 3SAT translation

Used byThe SAT-to-3SAT translation preserves satisfiability

TheoremThe lifted assignment on fresh variables#✓fully proved

For every assignment \(v : \mathbb{N} \to \mathrm{Bool}\), every CNF formula \(\varphi\) and every \(w \in \mathbb{N}\), the assignment lifted from \(v\) for the 3SAT translation of \(\varphi\) gives fresh variable number \(w\), that is variable \(2^{w+1} + 1\), the fresh-variable value of \(w\) built from \(v\) and \(\varphi\).

theorem lift_fresh (v : ℕ → Bool) (φ : CNF) (w : ℕ) : lift v φ (fresh w) = freshVal v φ w

Uses 4 · Used by 1

Statement usesFresh variable indices · Values of the fresh variables in the 3SAT translation · Lifting an assignment to the 3SAT translation · CNF formula

Used byThe SAT-to-3SAT translation preserves satisfiability

TheoremThe SAT-to-3SAT translation preserves satisfiability#✓fully proved

For every CNF formula \(\varphi\), the translation \(\mathrm{to3}(\varphi)\) is satisfiable if and only if \(\varphi\) is satisfiable.

theorem cnfSat_to3_iff (φ : CNF) : CNFSat (to3 φ) ↔ CNFSat φ

Uses 12 · Used by 1

Statement usesThe SAT-to-3SAT translation · CNF formula · Satisfiability of a CNF formula

Proof usesLifting an assignment to the 3SAT translation · The lifted assignment on fresh variables · The lifted assignment on renamed variables · Renaming of the original variables · Clause-by-clause translation with a fresh-number counter · Completeness of the auxiliary 3SAT translation · Soundness of the auxiliary 3SAT translation · Satisfaction of a CNF formula · Satisfiability means having a satisfying assignment

Used byCorrectness of the SAT-to-3SAT reduction on bit strings

TheoremCNF encodings are nonempty#✓fully proved

For every CNF formula \(\varphi\), the binary encoding of \(\varphi\) is not the empty bit string.

theorem encodeCNF_ne_nil (φ : CNF) : encodeCNF φ ≠ []

Uses 4 · Used by 1

Statement usesLength-prefixed binary code of a CNF formula · CNF formula

Proof usesLength-prefixed binary code of a clause · CNF clause

Used byCorrectness of the SAT-to-3SAT reduction on bit strings

TheoremCorrectness of the SAT-to-3SAT reduction on bit strings#✓fully proved

For every bit string \(x\), SAT accepts \(x\) (that is, \(x\) encodes a satisfiable CNF formula) exactly when 3SAT accepts the image of \(x\) under the SAT-to-3SAT reduction (that is, the image encodes a satisfiable CNF formula in which every clause has at most three literals).

theorem satDec_eq_sat3Dec_reduce3 (x : List Bool) : satDec x = sat3Dec (reduce3 x)

Uses 27 · Used by 1

Statement usesThe SAT-to-3SAT reduction on bit strings · The 3SAT decision problem · SAT as a decision problem

Proof usesThe SAT-to-3SAT translation preserves satisfiability · CNF encodings are nonempty · Three-literal clause test · The SAT-to-3SAT translation yields clauses of length at most three · The SAT-to-3SAT translation · The SAT language · Decoding a complete length-prefixed CNF formula · Decoding a length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Decoding a length-prefixed clause · Decoding a fixed number of clauses · Decoding a literal · Decoding a fixed number of literals · Decoding a prefix-coded natural number · Length-prefixed binary code of a CNF formula · Length-prefixed binary code of a clause · Binary code of a literal · Prefix-free code of a natural number · Reading a unary length prefix · CNF formula · CNF clause · Satisfiability of a CNF formula · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Used bySAT reduces to 3SAT

TheoremBinary representation of a fresh name#✓fully proved

For every natural number \(z\), the binary representation (least significant bit first) of \(\mathrm{fresh}(z) = 2^{z+1} + 1\) is \(\mathrm{true}\), then \(z\) copies of \(\mathrm{false}\), then \(\mathrm{true}\).

theorem encodeNat_fresh (z : ℕ) :
    encodeNat (fresh z) = true :: (List.replicate z false ++ [true])

Uses 1 · Used by 1

Statement usesFresh variable indices

Used byCode of a fresh literal

TheoremCode of a fresh literal#✓fully proved

For every natural number \(z\) and every polarity \(b\), the binary code of the literal \((\mathrm{fresh}(z), b)\), where \(\mathrm{fresh}(z) = 2^{z+1} + 1\), is \(\mathrm{true}, \mathrm{true}\), then \(z\) copies of the pair \(\mathrm{true}, \mathrm{false}\), then \(\mathrm{true}, \mathrm{true}, \mathrm{false}, b\).

theorem encodeLit_fresh (z : ℕ) (b : Bool) :
    encodeLit (fresh z, b) = [true, true] ++ rep [true, false] z ++ [true, true, false, b]

Uses 6 · Used by 1

Statement usesFresh variable indices · Binary code of a literal · Repeated block

Proof usesBinary representation of a fresh name · Prefix-free code of a natural number · Self-delimiting form of a bitstring

Used byFresh-literal subroutine of the 3SAT emitter

TheoremCode of a renamed literal#✓fully proved

For every literal \((n, p)\), the binary code of the renamed literal \((2n, p)\) is: the pair \(\mathrm{true}, \mathrm{false}\) if \(n \neq 0\) and nothing if \(n = 0\), then the pair \(\mathrm{true}, b\) for each bit \(b\) of the binary representation of \(n\) (least significant bit first, no bits for \(n = 0\)), then \(\mathrm{false}, p\).

theorem encodeLit_renLit (l : ℕ × Bool) :
    encodeLit (renLit l) = (if l.1 = 0 then [] else [true, false]) ++
      (encodeNat l.1).flatMap (fun b => [true, b]) ++ [false, l.2]

Uses 4 · Used by 1

Statement usesRenaming a literal · Binary code of a literal

Proof usesPrefix-free code of a natural number · Self-delimiting form of a bitstring

Used byCopying a renamed name

InductiveStacks of the 3SAT emitter#✓fully proved

The 3SAT emitter machine has six stacks: the token stack \(T\), the output stack \(O\), the fresh counter \(U\), two scratch counters \(Z\) and \(W\), and the output clause count \(C\).

inductive K | T | O | U | Z | W | C
  deriving DecidableEq

Used by 16

Used byThe 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · The SAT-to-3SAT emitter · The stacks of the 3SAT emitter · The 3SAT emitter processes a whole formula · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · The SAT-to-3SAT reduction is polynomial-time · One literal of the emitter · The literals of a clause in the emitter · Copying a renamed name · The SAT-to-3SAT emitter machine · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Stack contents of the SAT-to-3SAT emitter · Closing an output clause in the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter

DefinitionStack alphabets of the SAT-to-3SAT emitter#✓fully proved

The output stack of the emitter machine holds Booleans; each of its other stacks (the token stack, the fresh counter, the two scratch counters and the output clause count) holds symbols of the SAT verifier's token alphabet.

The counters are unary: they hold only the clause token.

@[reducible] def Γ : K → Type
  | .O => Bool
  | _ => Sym

Uses 2 · Used by 14

Statement usesStacks of the 3SAT emitter · Stack alphabet of the SAT verifier

Used byThe 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · The SAT-to-3SAT emitter · The 3SAT emitter processes a whole formula · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · The SAT-to-3SAT reduction is polynomial-time · One literal of the emitter · The literals of a clause in the emitter · Copying a renamed name · The SAT-to-3SAT emitter machine · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Stack contents of the SAT-to-3SAT emitter · Closing an output clause in the SAT-to-3SAT emitter

InductiveControl labels of the SAT-to-3SAT emitter#✓fully proved

The emitter machine has the labels \(\mathrm{start}\), \(\mathrm{clause}\), \(\mathrm{fin}\) and \(\mathrm{done}\), and, for Booleans \(f, p, s, x, e\), the labels \(\mathrm{lit}(f)\), \(\mathrm{fa}(s, x)\), \(\mathrm{fb}(s, x)\), \(\mathrm{fc}(s, x)\), \(\mathrm{fd}(s, x)\), \(\mathrm{fe}(s, x)\), \(\mathrm{body}(f, p)\), \(\mathrm{cp}(f, e)\), \(\mathrm{aft}(f)\) and \(\mathrm{sfx}(f)\), all distinct; equality of labels is decidable.

At \(\mathrm{lit}(f)\) the machine pops a literal marker, \(f\) telling whether it is the first literal walked in its clause. The labels \(\mathrm{fa}\) to \(\mathrm{fe}\) prepend the fresh literal \((2^{z+1} + 1, s)\) for the current counter \(z\), where \(x\) is the polarity of the pending literal when \(s\) is true and its first-literal flag when \(s\) is false. The labels \(\mathrm{body}\) and \(\mathrm{cp}\) prepend the renamed literal, and \(\mathrm{aft}\) and \(\mathrm{sfx}\) close the output clause.

inductive Lab
  | start | clause | lit (f : Bool)
  | fa (s x : Bool) | fb (s x : Bool) | fc (s x : Bool) | fd (s x : Bool) | fe (s x : Bool)
  | body (f p : Bool) | cp (f ne : Bool) | aft (f : Bool) | sfx (f : Bool) | fin | done
  deriving DecidableEq

Used by 16

Used byThe 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · The SAT-to-3SAT emitter · The 3SAT emitter processes a whole formula · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · The SAT-to-3SAT reduction is polynomial-time · One literal of the emitter · The literals of a clause in the emitter · Copying a renamed name · Entry label of a literal · The SAT-to-3SAT emitter machine · Return label of the fresh-literal subroutine · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Start label of the SAT-to-3SAT emitter · Closing an output clause in the SAT-to-3SAT emitter

DefinitionLiteral-marker test of the 3SAT emitter#✓fully proved

For an optional token \(s\) (the top of a stack, absent when the stack is empty), the test is true exactly when \(s\) is present and is a literal marker, of either polarity.

def isLit : Option Sym → Bool
  | some (.lit _) => true
  | _ => false

Uses 1 · Used by 8

Statement usesStack alphabet of the SAT verifier

Used byThe CLIQUE emitter machine · Clique emitter: moving the walk side back · Clique emitter: one clause · The 3SAT emitter processes one clause · One literal of the emitter · The literals of a clause in the emitter · The SAT-to-3SAT emitter machine · Closing an output clause in the SAT-to-3SAT emitter

DefinitionEntry label of a literal#✓fully proved

For Booleans \(f\) and \(p\), the label where the emitter continues after popping the marker of a literal of polarity \(p\) is \(\mathrm{body}(\text{true}, p)\), which copies the name directly, if \(f\) holds (the literal is the first walked in its clause), and \(\mathrm{fa}(\text{true}, p)\), which first prepends the fresh literal of the current counter with polarity true, otherwise.

def pre (f p : Bool) : Lab := if f then .body true p else .fa true p

Uses 1 · Used by 2

Statement usesControl labels of the SAT-to-3SAT emitter

Used byThe 3SAT emitter reads a literal marker · The SAT-to-3SAT emitter machine

DefinitionReturn label of the fresh-literal subroutine#✓fully proved

For Booleans \(s\) and \(x\), the label where the emitter continues after prepending the fresh literal of polarity \(s\) is \(\mathrm{body}(\text{false}, x)\) if \(s\) is true, which copies the name of the pending literal of polarity \(x\), and \(\mathrm{sfx}(x)\) if \(s\) is false, which closes the output clause, \(x\) being the first-literal flag.

def ret : Bool → Bool → Lab
  | true, p => .body false p
  | false, f => .sfx f

Uses 1 · Used by 3

Statement usesControl labels of the SAT-to-3SAT emitter

Used byFresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · Closing an output clause in the SAT-to-3SAT emitter

DefinitionThe SAT-to-3SAT emitter machine#✓fully proved

The emitter is the multi-stack machine on the stacks \(T, O, U, Z, W, C\) of the emitter (\(O\) holds bits, the others token symbols), with the labels of the emitter and one internal Boolean variable. A unit is the clause symbol, and prepending bits \(b_1, \dots, b_k\) to \(O\) pushes them so that \(O\) reads \(b_1, \dots, b_k\) from the top. The labels act as follows.

• \(\mathrm{start}\): if \(T\) is empty, push \(\text{false}\) on \(O\) and go to \(\mathrm{fin}\); otherwise pop \(T\) and go to \(\mathrm{clause}\).
• \(\mathrm{clause}\): if the top of \(T\) is a literal marker, go to \(\mathrm{lit}(\text{true})\); otherwise push a unit on \(C\), push \(\text{false}\) on \(O\) and go to \(\mathrm{start}\).
• \(\mathrm{lit}(f)\): pop \(T\), set the variable \(p\) to whether the popped symbol is the literal marker of polarity true, and go to \(\mathrm{body}(\text{true}, p)\) if \(f\) holds and to \(\mathrm{fa}(\text{true}, p)\) otherwise.
• \(\mathrm{fa}(s, x)\): prepend \(\text{true}, \text{true}, \text{false}, s\) to \(O\) and go to \(\mathrm{fb}(s, x)\).
• \(\mathrm{fb}(s, x)\): pop \(U\) until it is empty, pushing a unit on \(Z\) and on \(W\) per popped symbol, then go to \(\mathrm{fc}(s, x)\).
• \(\mathrm{fc}(s, x)\): pop \(W\) until it is empty, pushing a unit on \(U\) per popped symbol, then go to \(\mathrm{fd}(s, x)\).
• \(\mathrm{fd}(s, x)\): pop \(Z\) until it is empty, prepending \(\text{true}, \text{false}\) to \(O\) per popped symbol, then go to \(\mathrm{fe}(s, x)\).
• \(\mathrm{fe}(\text{true}, p)\): push a unit on \(U\), prepend \(\text{true}, \text{true}\) to \(O\) and go to \(\mathrm{body}(\text{false}, p)\). \(\mathrm{fe}(\text{false}, f)\): prepend \(\text{true}, \text{true}\) to \(O\) and go to \(\mathrm{sfx}(f)\).
• \(\mathrm{body}(f, p)\): prepend \(\text{false}, p\) to \(O\) and go to \(\mathrm{cp}(f, \text{false})\).
• \(\mathrm{cp}(f, e)\): if the top of \(T\) is a bit symbol \(b\), pop it, prepend \(\text{true}, b\) to \(O\) and go to \(\mathrm{cp}(f, \text{true})\); otherwise prepend \(\text{true}, \text{false}\) to \(O\) if \(e\) holds, and go to \(\mathrm{aft}(f)\).
• \(\mathrm{aft}(f)\): if the top of \(T\) is a literal marker, go to \(\mathrm{fa}(\text{false}, f)\); otherwise push a unit on \(C\), prepend \(k\) copies of \(\text{true}\) and then \(\text{false}\) to \(O\), where \(k = 1\) if \(f\) holds and \(k = 2\) otherwise, and go to \(\mathrm{start}\).
• \(\mathrm{sfx}(f)\): push a unit on \(C\), prepend \(k\) copies of \(\text{true}\) and then \(\text{false}\) to \(O\), where \(k = 2\) if \(f\) holds and \(k = 3\) otherwise, and go to \(\mathrm{lit}(\text{false})\).
• \(\mathrm{fin}\): pop \(C\) until it is empty, prepending \(\text{true}\) to \(O\) per popped symbol, then go to \(\mathrm{done}\).
• \(\mathrm{done}\): halt.

Each test of a stack top and each pop of a loop also stores its outcome in the internal variable.

Cslib.Complexity.Karp.Emit3.prog · 25 lines

def prog : Lab → TM2.Stmt Γ Lab Bool
  | .start => .peek .T (fun _ o => o.isNone) <| .branch id
      (.push .O (fun _ => false) (.goto fun _ => .fin))
      (.pop .T (fun s _ => s) (.goto fun _ => .clause))
  | .clause => .peek .T (fun _ o => isLit o) <| .branch id (.goto fun _ => .lit true)
      (.push .C (fun _ => Sym.cl) <| .push .O (fun _ => false) <| .goto fun _ => .start)
  | .lit f => .pop .T (fun _ o => o == some (.lit true)) (.goto fun s => pre f s)
  | .fa s x => emitR .O [true, true, false, s] (.fb s x)
  | .fb s x => xfer .U [⟨.Z, Sym.cl⟩, ⟨.W, Sym.cl⟩] (.fb s x) (.fc s x)
  | .fc s x => xfer .W [⟨.U, Sym.cl⟩] (.fc s x) (.fd s x)
  | .fd s x => xferE .Z .O [true, false] (.fd s x) (.fe s x)
  | .fe true p => .push .U (fun _ => Sym.cl) (emitR .O [true, true] (.body false p))
  | .fe false f => emitR .O [true, true] (.sfx f)
  | .body f p => emitR .O [false, p] (.cp f false)
  | .cp f ne => .peek .T (fun _ o => isBit Sym.bit? o) <| .branch id
      (.peek .T (fun _ o => o == some (.bit true)) <| .pop .T (fun s _ => s) <|
        .push .O id <| .push .O (fun _ => true) <| .goto fun _ => .cp f true)
      (if ne then emitR .O [true, false] (.aft f) else .goto fun _ => .aft f)
  | .aft f => .peek .T (fun _ o => isLit o) <| .branch id (.goto fun _ => .fa false f)
      (.push .C (fun _ => Sym.cl) <|
        emitR .O (List.replicate (if f then 1 else 2) true ++ [false]) .start)
  | .sfx f => .push .C (fun _ => Sym.cl) <|
      emitR .O (List.replicate (if f then 2 else 3) true ++ [false]) (.lit false)
  | .fin => xferE .C .O [true] .fin .done
  | .done => .halt

Uses 12 · Used by 11

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · Literal-marker test of the 3SAT emitter · Entry label of a literal · Stack alphabets of the SAT-to-3SAT emitter · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Flag bit of a machine state · Prepending a constant list · Bit test for the top of a stack · Counter transfer loop · Draining a counter while prepending a block

Used byThe 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · The SAT-to-3SAT emitter · The 3SAT emitter processes a whole formula · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · One literal of the emitter · The literals of a clause in the emitter · Copying a renamed name · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Closing an output clause in the SAT-to-3SAT emitter

DefinitionStart label of the SAT-to-3SAT emitter#✓fully proved

The start label of the emitter machine is its label \(\mathrm{start}\), at which the machine begins each input clause or, once the token stack is empty, moves on to its final phase, which writes the output clause count.

def start : Lab := .start

Uses 1 · Used by 2

Statement usesControl labels of the SAT-to-3SAT emitter

Used byThe SAT-to-3SAT emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time

DefinitionStack contents of the SAT-to-3SAT emitter#✓fully proved

For a list \(t\) of tokens, a list \(o\) of bits and \(z, c \in \mathbb{N}\), \(\mathrm{st}(t, o, z, c)\) is the stack contents of the emitter machine in which the token stack holds \(t\), the output stack holds \(o\), the fresh counter holds exactly \(z\) copies of the clause token \(\mathrm{cl}\), the output clause count holds exactly \(c\) copies of \(\mathrm{cl}\), and the two scratch counters are empty.

def st (t : List Sym) (o : List Bool) (z c : ℕ) : ∀ k, List (Γ k)
  | .T => t
  | .O => o
  | .U => cnt Sym.cl z
  | .Z => []
  | .W => []
  | .C => cnt Sym.cl c

Uses 4 · Used by 10

Statement usesStacks of the 3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Stack alphabet of the SAT verifier · Unary counter

Used byThe 3SAT emitter processes one clause · Name copy loop of the 3SAT emitter · The 3SAT emitter processes a whole formula · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · One literal of the emitter · The literals of a clause in the emitter · Copying a renamed name · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Closing an output clause in the SAT-to-3SAT emitter

TheoremFresh-literal subroutine of the 3SAT emitter#✓fully proved

For all booleans \(s\) and \(x\), every token list \(t\), output bit list \(o\), natural numbers \(z\) and \(c\), and flag \(v\), there is a flag \(v'\) such that the 3SAT emitter machine, started at the fresh-literal label for \((s, x)\) with flag \(v\), token stack \(t\), output stack \(o\), fresh counter \(z\), clause count \(c\) and empty scratch counters, reaches in exactly \(3z + 5\) steps the return label for \((s, x)\) with flag \(v'\), token stack \(t\), output stack the code of the literal \((\mathrm{fresh}(z), s)\) followed by \(o\), where \(\mathrm{fresh}(z) = 2^{z+1} + 1\), fresh counter \(z + 1\) if \(s\) is true and \(z\) if \(s\) is false, clause count \(c\) and empty scratch counters. The return label is the renamed-literal label for a literal of polarity \(x\) that is not the first walked in its clause if \(s\) is true, and the clause-closing label for first-flag \(x\) if \(s\) is false.

The subroutine prepends \(\mathrm{true}, \mathrm{true}, \mathrm{false}, s\), copies the fresh counter \(U\) into the scratch counter \(Z\) (restoring \(U\) through the scratch counter \(W\)), prepends \(\mathrm{true}, \mathrm{false}\) per unit of \(Z\), then prepends \(\mathrm{true}, \mathrm{true}\), and for \(s\) true adds one to \(U\).

theorem fresh_run (s x : Bool) (t : List Sym) (o : List Bool) (z c : ℕ) (v : Bool) :
    ∃ v', Run prog (3 * z + 5) ⟨some (.fa s x), v, st t o z c⟩
      ⟨some (ret s x), v', st t (encodeLit (fresh z, s) ++ o) (z + if s then 1 else 0) c⟩

Uses 20 · Used by 2

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Return label of the fresh-literal subroutine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Fresh variable indices · Stack alphabet of the SAT verifier · Binary code of a literal · Exact-length runs of a TM2 machine

Proof usesCode of a fresh literal · Flag bit of a machine state · A single step executes the statement at the current label · Unary counter · Copying a counter through a scratch stack · Pushing a constant list · Prepending a constant list · Pushing a list of symbols onto one stack · Repeated block · Draining a counter while prepending a block

Used byThe 3SAT emitter reads a literal marker · Closing an output clause in the SAT-to-3SAT emitter

TheoremName copy loop of the 3SAT emitter#✓fully proved

Let \(f\) and \(e\) be booleans, \(R\) a token list whose first token, if there is one, is not a name bit, \(z\) and \(c\) natural numbers, \(b_1, \dots, b_m\) bits, \(v\) a flag and \(o\) an output bit list. Then there is a flag \(v'\) such that the 3SAT emitter machine, started at the copy label for \((f, e)\) with flag \(v\), token stack the name-bit tokens \(b_1, \dots, b_m\) followed by \(R\), output stack \(o\), fresh counter \(z\), clause count \(c\) and empty scratch counters, reaches in exactly \(m + 1\) steps the after-literal label for \(f\) with flag \(v'\), token stack \(R\), output stack \(P, \mathrm{true}, b_m, \mathrm{true}, b_{m-1}, \dots, \mathrm{true}, b_1\) followed by \(o\), and the same counters, where \(P\) is the pair \(\mathrm{true}, \mathrm{false}\) if \(e\) is true or \(m > 0\), and is empty otherwise.

Each name bit \(b\) read prepends \(b\) and then \(\mathrm{true}\); the leading pair \(\mathrm{true}, \mathrm{false}\) codes the low bit \(0\) of a renamed name \(2n\).

theorem cp_run (f : Bool) (R : List Sym) (hR : R.head?.bind Sym.bit? = none) (z c : ℕ) :
    ∀ (rb : List Bool) (ne v : Bool) (o : List Bool),
      ∃ v', Run prog (rb.length + 1) ⟨some (.cp f ne), v, st (rb.map Sym.bit ++ R) o z c⟩
        ⟨some (.aft f), v', st R ((if ne || !rb.isEmpty then [true, false] else []) ++
          rb.reverse.flatMap (fun b => [true, b]) ++ o) z c⟩

Uses 12 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label · Prepending a constant list · Bit test for the top of a stack · Pushing a list of symbols onto one stack

Used byCopying a renamed name

TheoremCopying a renamed name#✓fully proved

Write \(\langle \ell, w, t, o, z, c\rangle\) for the configuration of the emitter machine at label \(\ell\) with internal variable \(w\), token stack \(t\), output stack \(o\), fresh counter \(z\), output-clause count \(c\) and empty scratch stacks. Let \(l = (n, b)\) be a literal, \(f\) and \(v\) Booleans, \(R\) a token stack whose top, if any, is not a bit symbol, \(o\) an output stack and \(z\), \(c\) natural numbers. Let \(B\) be the \(k\) binary digits of \(n\) as bit symbols, most significant first (\(k = 0\) for \(n = 0\)), and \(e\) the encoding of the renamed literal \((2n, b)\). Then for some \(w'\) the machine goes in exactly \(k + 2\) steps from \(\langle \mathrm{body}(f, b), v, B R, o, z, c\rangle\) to \(\langle \mathrm{aft}(f), w', R, e\,o, z, c\rangle\), where juxtaposition is concatenation of stacks, top first.

theorem name_run (f : Bool) (l : ℕ × Bool) (R : List Sym) (hR : R.head?.bind Sym.bit? = none)
    (o : List Bool) (z c : ℕ) (v : Bool) :
    ∃ v', Run prog ((encodeNat l.1).length + 2)
      ⟨some (.body f l.2), v, st (((encodeNat l.1).map Sym.bit).reverse ++ R) o z c⟩
      ⟨some (.aft f), v', st R (encodeLit (renLit l) ++ o) z c⟩

Uses 14 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Renaming a literal · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Binary code of a literal · Exact-length runs of a TM2 machine

Proof usesName copy loop of the 3SAT emitter · Code of a renamed literal · A single step executes the statement at the current label · Pushing a list of symbols onto one stack

Used byOne literal of the emitter

TheoremThe 3SAT emitter reads a literal marker#✓fully proved

For all booleans \(f\) and \(p\), every token list \(t\), output bit list \(o\), natural numbers \(z\) and \(c\), and flag \(v\), there is a flag \(v'\) such that the 3SAT emitter machine, started at the literal label for \(f\) with flag \(v\), token stack the literal marker of polarity \(p\) followed by \(t\), output stack \(o\), fresh counter \(z\), clause count \(c\) and empty scratch counters, reaches the renamed-literal label for \((f, p)\) with flag \(v'\) and token stack \(t\) as follows. If \(f\) is true (the literal is the first walked in its clause), this takes exactly \(1\) step and leaves the output stack and the fresh counter unchanged. If \(f\) is false, it takes exactly \(3z + 6\) steps, the output stack becomes the code of the literal \((\mathrm{fresh}(z), \mathrm{true})\) followed by \(o\), where \(\mathrm{fresh}(z) = 2^{z+1} + 1\), and the fresh counter becomes \(z + 1\). In both cases the clause count stays \(c\) and the scratch counters stay empty.

theorem head_run (f : Bool) (p : Bool) (t : List Sym) (o : List Bool) (z c : ℕ) (v : Bool) :
    ∃ v', Run prog (if f then 1 else 3 * z + 6) ⟨some (.lit f), v, st (.lit p :: t) o z c⟩
      ⟨some (.body f p), v', st t ((if f then [] else encodeLit (fresh z, true)) ++ o)
        (z + if f then 0 else 1) c⟩

Uses 13 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Fresh variable indices · Stack alphabet of the SAT verifier · Binary code of a literal · Exact-length runs of a TM2 machine

Proof usesFresh-literal subroutine of the 3SAT emitter · Entry label of a literal · Return label of the fresh-literal subroutine · A single step executes the statement at the current label

Used byOne literal of the emitter

TheoremClosing an output clause in the SAT-to-3SAT emitter#✓fully proved

Let \(f\) be a Boolean, \(R\) a list of tokens, \(o\) a list of bits and \(z, c \in \mathbb{N}\), and let \(m = 1\) if \(f\) is true and \(m = 2\) otherwise. Start the emitter machine at its clause-closing label \(\mathrm{aft}(f)\), with any internal state, with stack contents \(\mathrm{st}(R, o, z, c)\): token stack \(R\), output stack \(o\), fresh counter \(z\), output clause count \(c\) and empty scratch counters.

If the top of \(R\) is a literal marker, then after exactly \(3z + 7\) steps the machine is at the label \(\mathrm{lit}(\mathrm{false})\) with stack contents \(\mathrm{st}(R, o', z, c + 1)\), where the list \(o'\) consists of \(m + 1\) copies of true, then false, then the code of the literal \((\mathrm{fresh}(z), \mathrm{false})\), then \(o\). Otherwise (in particular when \(R\) is empty), after exactly one step the machine is at the label \(\mathrm{start}\) with stack contents \(\mathrm{st}(R, o', z, c + 1)\), where \(o'\) consists of \(m\) copies of true, then false, then \(o\). In both cases the final internal state is unspecified.

theorem tail_run (f : Bool) (R : List Sym) (o : List Bool) (z c : ℕ) (v : Bool) :
    ∃ v', Run prog (if isLit R.head? then 3 * z + 7 else 1) ⟨some (.aft f), v, st R o z c⟩
      ⟨some (if isLit R.head? then .lit false else .start), v',
        st R (List.replicate ((if f then 1 else 2) + if isLit R.head? then 1 else 0) true ++
          false :: ((if isLit R.head? then encodeLit (fresh z, false) else []) ++ o)) z
          (c + 1)⟩

Uses 15 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · Literal-marker test of the 3SAT emitter · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Fresh variable indices · Stack alphabet of the SAT verifier · Binary code of a literal · Exact-length runs of a TM2 machine

Proof usesFresh-literal subroutine of the 3SAT emitter · Return label of the fresh-literal subroutine · A single step executes the statement at the current label · Prepending a constant list · Pushing a list of symbols onto one stack

Used byOne literal of the emitter

DefinitionOutput clause of one literal#✓fully proved

For Booleans \(f\) and \(g\), a counter \(z\) and a literal \(l = (n, b)\), let \(z' = z\) if \(f\) holds and \(z' = z + 1\) otherwise. The output clause of \(l\) is the clause consisting of, in this order: the literal \((2^{z'+1} + 1, \text{false})\) unless \(g\) holds, then the renamed literal \((2n, b)\), then the literal \((2^{z+1} + 1, \text{true})\) unless \(f\) holds. Here \(f\) tells whether \(l\) is the first literal walked in its clause, \(g\) whether it is the last one, and \(z'\) is the counter after \(l\).

def litCl (f g : Bool) (z : ℕ) (l : ℕ × Bool) : CNFClause :=
  (if g then [] else [(fresh (z + if f then 0 else 1), false)]) ++
    renLit l :: (if f then [] else [(fresh z, true)])

Uses 3 · Used by 5

Statement usesFresh variable indices · Renaming a literal · CNF clause

Used byThe 3SAT emitter processes one clause · One literal of the emitter · The literals of a clause in the emitter · Output clauses of a walked list of literals · Walking a whole clause gives its chain

DefinitionFresh numbers used by a run of literals#✓fully proved

For a list \(L\) of literals and a Boolean \(f\), the number of fresh numbers used up by walking \(L\) is \(|L| - 1\) (truncated at \(0\)) if \(f\) holds and \(|L|\) otherwise; \(f\) tells whether the last literal of \(L\) is the first literal walked in its clause.

def nz (Ls : List (ℕ × Bool)) (f : Bool) : ℕ := if f then Ls.length - 1 else Ls.length

Used by 4

Used byThe 3SAT emitter processes one clause · The literals of a clause in the emitter · Output clauses of a walked list of literals · Walking a whole clause gives its chain

DefinitionOutput clauses of a walked list of literals#✓fully proved

For a list \(L\) of literals of a clause, Booleans \(f\) and \(g\), and \(z \in \mathbb{N}\), \(\mathrm{walkF}(L, f, g, z)\) is the list of output clauses of the literals of \(L\), in reading order, when \(L\) is walked from its last literal with counter \(z\); \(f\) tells whether the last literal of \(L\) is the first walked in its clause, and \(g\) whether the first literal of \(L\) is the last walked. It is defined by recursion on \(L\). The empty list gives no clauses. If \(L\) has first literal \(l\) and remaining literals \(L'\), the first clause is the output clause of \(l\) whose first-walked flag is true exactly when \(f\) is true and \(L'\) is empty, whose last-walked flag is \(g\), and whose counter is \(z + n\), where \(n\) is the number of fresh numbers used up by walking \(L'\) (\(|L'| - 1\) if \(f\) is true, with \(0 - 1 = 0\), and \(|L'|\) otherwise); it is followed by \(\mathrm{walkF}(L', f, \mathrm{false}, z)\).

def walkF : List (ℕ × Bool) → Bool → Bool → ℕ → CNF
  | [], _, _, _ => []
  | l :: Ls, f, g, z => litCl (f && Ls.isEmpty) g (z + nz Ls f) l :: walkF Ls f false z

Uses 4 · Used by 4

Statement usesOutput clause of one literal · Fresh numbers used by a run of literals · CNF formula · CNF clause

Used byThe 3SAT emitter processes one clause · The literals of a clause in the emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Walking a whole clause gives its chain

TheoremWalking a whole clause gives its chain#✓fully proved

For every non-empty clause \(C\) and every \(z \in \mathbb{N}\), the output clauses of the literals of \(C\), walked from its last literal with counter \(z\), with both the first-walked flag and the last-walked flag true, that is, \(\mathrm{walkF}(C, \mathrm{true}, \mathrm{true}, z)\), are the chain of clauses replacing \(C\) with fresh numbers from \(z\) on.

theorem walkF_chain (C : CNFClause) (hC : C ≠ []) (z : ℕ) : walkF C true true z = chain C z

Uses 9 · Used by 2

Statement usesOutput clauses of a walked list of literals · The chain of clauses replacing one clause · CNF formula · CNF clause

Proof usesOutput clause of one literal · Fresh numbers used by a run of literals · The tail of a clause chain · Fresh variable indices · Renaming a literal

Used byThe 3SAT emitter processes one clause · The SAT-to-3SAT emitter writes the encoded translation in quadratic time

TheoremOne literal of the emitter#✓fully proved

Write \(\langle \ell, w, t, o, z, c\rangle\) for the configuration of the emitter machine at label \(\ell\) with internal variable \(w\), token stack \(t\), output stack \(o\), fresh counter \(z\), output-clause count \(c\) and empty scratch stacks. Let \(l = (n, b)\) be a literal, \(f\) and \(v\) Booleans, \(R\) a token stack whose top, if any, is not a bit symbol, \(o\) an output stack, and \(z\), \(c\), \(Z_b\) natural numbers with \(z + d \le Z_b\), where \(d = 0\) if \(f\) holds and \(d = 1\) otherwise. Let \(T_l\) be the token block of \(l\): the literal marker of polarity \(b\) above the binary digits of \(n\), most significant first (no digits for \(n = 0\)). Let \(g\) be true exactly when the top of \(R\) is not a literal marker (in particular when \(R\) is empty), let \(\ell'\) be \(\mathrm{start}\) if \(g\) holds and \(\mathrm{lit}(\text{false})\) otherwise, and let \(e\) be the encoding of the output clause of \(l\) with flags \(f\), \(g\) and counter \(z\). Then for some \(w'\) the machine goes in at most \(|T_l| + 6 Z_b + 14\) steps from \(\langle \mathrm{lit}(f), v, T_l R, o, z, c\rangle\) to \(\langle \ell', w', R, e\,o, z + d, c + 1\rangle\), where juxtaposition is concatenation of stacks, top first.

theorem lit_run (Zb : ℕ) (f : Bool) (l : ℕ × Bool) (R : List Sym)
    (hR : R.head?.bind Sym.bit? = none) (o : List Bool) (z c : ℕ)
    (hz : z + (if f then 0 else 1) ≤ Zb) (v : Bool) :
    ∃ v', RunLe prog ((Check.litRev l).length + 6 * Zb + 14)
      ⟨some (.lit f), v, st (Check.litRev l ++ R) o z c⟩
      ⟨some (if isLit R.head? then .lit false else .start), v',
        st R (encodeClause (litCl f (!isLit R.head?) z l) ++ o) (z + if f then 0 else 1)
          (c + 1)⟩

Uses 20 · Used by 2

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · Literal-marker test of the 3SAT emitter · Output clause of one literal · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Length-prefixed binary code of a clause · Runs within a step budget

Proof usesThe 3SAT emitter reads a literal marker · Copying a renamed name · Closing an output clause in the SAT-to-3SAT emitter · Fresh variable indices · Renaming a literal · Binary code of a literal · CNF clause · Exact-length runs of a TM2 machine

Used byThe 3SAT emitter processes one clause · The literals of a clause in the emitter

TheoremThe literals of a clause in the emitter#✓fully proved

Write \(\langle \ell, w, t, o, z, c\rangle\) for the configuration of the emitter machine at label \(\ell\) with internal variable \(w\), token stack \(t\), output stack \(o\), fresh counter \(z\), output-clause count \(c\) and empty scratch stacks. Let \(Z_b\) be a natural number, \(L = (l_1, \dots, l_k)\) a list of literals, \(R\) a token stack whose top is a literal marker, \(f\) and \(v\) Booleans, \(o\) an output stack and \(z\), \(c\) natural numbers with \(z + m \le Z_b\), where \(m\) is \(k - 1\) (truncated at \(0\)) if \(f\) holds and \(k\) otherwise. The token block of a literal \((n, b)\) is the literal marker of polarity \(b\) above the binary digits of \(n\), most significant first (no digits for \(n = 0\)); let \(T\) be the concatenation of the token blocks of \(l_k, \dots, l_1\), in this order. For \(1 \le i \le k\) let \(z_i = z + m_i\), where \(m_i\) is \(k - i - 1\) (truncated at \(0\)) if \(f\) holds and \(k - i\) otherwise, let \(f_i\) be true exactly when \(f\) holds and \(i = k\), and let \(e_i\) be the encoding of the output clause of \(l_i\) with flags \(f_i\), false and counter \(z_i\). Let \(E = e_1 \cdots e_k\) (empty for \(k = 0\)), and let \(f'\) be true exactly when \(f\) holds and \(k = 0\). Then for some \(w'\) the machine goes in at most \(|T| + k (6 Z_b + 14)\) steps from \(\langle \mathrm{lit}(f), v, T R, o, z, c\rangle\) to \(\langle \mathrm{lit}(f'), w', R, E\,o, z + m, c + k\rangle\), where juxtaposition is concatenation of stacks, top first.

theorem lits_run (Zb : ℕ) :
    ∀ (Ls : List (ℕ × Bool)) (R : List Sym), isLit R.head? = true →
      ∀ (f : Bool) (o : List Bool) (z c : ℕ) (v : Bool), z + nz Ls f ≤ Zb →
      ∃ v', RunLe prog ((Ls.flatMap Check.litRev).length + Ls.length * (6 * Zb + 14))
        ⟨some (.lit f), v, st (Ls.reverse.flatMap Check.litRev ++ R) o z c⟩
        ⟨some (.lit (f && Ls.isEmpty)), v',
          st R ((walkF Ls f false z).flatMap encodeClause ++ o) (z + nz Ls f) (c + Ls.length)⟩

Uses 18 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · Literal-marker test of the 3SAT emitter · Fresh numbers used by a run of literals · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Output clauses of a walked list of literals · Stack alphabets of the SAT-to-3SAT emitter · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Length-prefixed binary code of a clause · CNF clause · Runs within a step budget

Proof usesOutput clause of one literal · One literal of the emitter · Reading a symbol as a name bit · CNF formula · Exact-length runs of a TM2 machine

Used byThe 3SAT emitter processes one clause

TheoremThe 3SAT emitter processes one clause#✓fully proved

Let \(C\) be a clause, \(Z_b\), \(z\) and \(c\) natural numbers with \(z + \mathrm{used}(C) \le Z_b\), where \(\mathrm{used}(C) = \max(|C| - 1, 0)\), let \(R\) be a token list that is empty or starts with a clause token, \(o\) an output bit list and \(v\) a flag. Let \(\mathrm{clRev}(C)\) be the tokens of \(C\) as they lie on the token stack (a clause token, then the tokens of its literals, last literal first), and let \(D_1, \dots, D_k\) be the clauses of \(\mathrm{chain}(C, z)\). Then there is a flag \(v'\) such that the 3SAT emitter machine, started at its start label with flag \(v\), token stack \(\mathrm{clRev}(C)\) followed by \(R\), output stack \(o\), fresh counter \(z\), clause count \(c\) and empty scratch counters, reaches in at most \(|\mathrm{clRev}(C)| \cdot (6 Z_b + 15)\) steps its start label with flag \(v'\), token stack \(R\), output stack \(\mathrm{enc}(D_1) \cdots \mathrm{enc}(D_k)\) followed by \(o\), fresh counter \(z + \mathrm{used}(C)\), clause count \(c + k\) and empty scratch counters, where \(\mathrm{enc}\) is the binary clause encoding.

theorem clause_run (Zb : ℕ) (C : CNFClause) (R : List Sym) (hR : R = [] ∨ R.head? = some .cl)
    (o : List Bool) (z c : ℕ) (hz : z + used C ≤ Zb) (v : Bool) :
    ∃ v', RunLe prog ((Check.clRev C).length * (6 * Zb + 15))
      ⟨some .start, v, st (Check.clRev C ++ R) o z c⟩
      ⟨some .start, v', st R ((chain C z).flatMap encodeClause ++ o) (z + used C)
        (c + (chain C z).length)⟩

Uses 25 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · The chain of clauses replacing one clause · Fresh variables reserved for a clause · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · Length-prefixed binary code of a clause · CNF clause · Runs within a step budget

Proof usesLiteral-marker test of the 3SAT emitter · Output clause of one literal · One literal of the emitter · The literals of a clause in the emitter · Fresh numbers used by a run of literals · Output clauses of a walked list of literals · Walking a whole clause gives its chain · A literal's tokens on the token stack · Reading a symbol as a name bit · Binary code of a literal · CNF formula · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byThe 3SAT emitter processes a whole formula

TheoremThe 3SAT emitter processes a whole formula#✓fully proved

Let \(\varphi = C_1 \cdots C_m\) be a CNF formula, \(u = \sum_{i=1}^{m} \max(|C_i| - 1, 0)\) the number of fresh variables its 3SAT translation uses, \(Z_b \ge u\) a natural number, \(R\) a token list that is empty or starts with a clause token, \(o\) an output bit list and \(v\) a flag. Let \(T\) be the token list \(\mathrm{clRev}(C_m) \cdots \mathrm{clRev}(C_1)\), where \(\mathrm{clRev}(C)\) is the list of tokens of \(C\) as they lie on the token stack, and let \(D_1, \dots, D_k\) be the clauses of the 3SAT translation \(\mathrm{to3}(\varphi)\). Then there is a flag \(v'\) such that the 3SAT emitter machine, started at its start label with flag \(v\), token stack \(T\) followed by \(R\), output stack \(o\), fresh counter \(0\), clause count \(0\) and empty scratch counters, reaches in at most \(|T| \cdot (6 Z_b + 15)\) steps its start label with flag \(v'\), token stack \(R\), output stack \(\mathrm{enc}(D_1) \cdots \mathrm{enc}(D_k)\) followed by \(o\), fresh counter \(u\), clause count \(k\) and empty scratch counters, where \(\mathrm{enc}\) is the binary clause encoding.

theorem formula_run (Zb : ℕ) :
    ∀ (φ : CNF) (R : List Sym), (R = [] ∨ R.head? = some .cl) → ∀ (o : List Bool) (v : Bool),
      (to3Aux φ).1 ≤ Zb →
      ∃ v', RunLe prog ((φ.reverse.flatMap Check.clRev).length * (6 * Zb + 15))
        ⟨some .start, v, st (φ.reverse.flatMap Check.clRev ++ R) o 0 0⟩
        ⟨some .start, v', st R ((to3 φ).flatMap encodeClause ++ o) (to3Aux φ).1
          (to3 φ).length⟩

Uses 17 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Stack contents of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · The SAT-to-3SAT translation · Clause-by-clause translation with a fresh-number counter · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · Length-prefixed binary code of a clause · CNF formula · CNF clause · Runs within a step budget

Proof usesThe 3SAT emitter processes one clause · The chain of clauses replacing one clause · Fresh variables reserved for a clause · Exact-length runs of a TM2 machine

Used byThe SAT-to-3SAT emitter writes the encoded translation in quadratic time

TheoremRepeating a single bit#✓fully proved

For every bit \(x\) and every \(n \in \mathbb{N}\), the repeated block \(\mathrm{rep}([x], n)\) is the list consisting of \(n\) copies of \(x\).

theorem rep_single (x : Bool) (n : ℕ) : rep [x] n = List.replicate n x

Uses 1 · Used by 2

Statement usesRepeated block

Used byClique emitter: the instance prefix · The SAT-to-3SAT emitter writes the encoded translation in quadratic time

TheoremThe SAT-to-3SAT emitter writes the encoded translation in quadratic time#✓fully proved

Let \(\varphi\) be a CNF formula, \(o\) a list of bits and \(T\) the token sequence of \(\varphi\). Start the emitter machine at its start label, with any internal state, with the token stack holding \(T\) reversed (so that the first token of \(T\) is at the bottom), the output stack holding \(o\), and every other stack empty. Then after at most \(8(|T| + 1)^2\) steps the machine reaches its label \(\mathrm{done}\), with some internal state and stack contents in which the output stack, read from the top, holds the binary code of the SAT-to-3SAT translation of \(\varphi\) followed by \(o\).

theorem run (φ : CNF) (o : List Bool) (v : Bool) (St : ∀ k, List (Γ k))
    (hT : St .T = (toks φ).reverse) (hO : St .O = o) (h0 : ∀ k, k ≠ .T → k ≠ .O → St k = []) :
    ∃ v' S', RunLe prog (8 * ((toks φ).length + 1) ^ 2) ⟨some start, v, St⟩
      ⟨some .done, v', S'⟩ ∧ S' .O = encodeCNF (to3 φ) ++ o

Uses 31 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · Start label of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · The SAT-to-3SAT translation · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · Length-prefixed binary code of a CNF formula · CNF formula · Runs within a step budget

Proof usesThe 3SAT emitter processes a whole formula · Repeating a single bit · Stack contents of the SAT-to-3SAT emitter · Output clauses of a walked list of literals · Walking a whole clause gives its chain · The chain of clauses replacing one clause · Clause-by-clause translation with a fresh-number counter · A clause's tokens on the token stack · A literal's tokens on the token stack · Tokens of a clause · Tokens of a literal · Length-prefixed binary code of a clause · CNF clause · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Unary counter · Pushing a list of symbols onto one stack · Repeated block · Draining a counter while prepending a block

Used byThe SAT-to-3SAT emitter

InductiveStacks of the 3SAT clause-length filter#✓fully proved

The filter has exactly two stacks: the token stack \(T\) and the side stack \(U\).

inductive K | T | U
  deriving DecidableEq

Used by 25

Used byPlacement of the filter's stacks in the host · Stack embedding of the clause-length filter into the host · Program of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier · The return phase ends on an empty side stack · The 3SAT filter's return phase moves the side stack back · One step of the 3SAT filter's return phase · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · Conditional move between stacks · The clause-length filter program · Correctness of the clause-length filter · Filter stacks from two lists · Statements of the filter · One step of the clause-length walk · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

InductiveLabels of the 3SAT clause-length filter#✓fully proved

The filter has exactly seven labels: the walking labels \(w_0, w_1, w_2, w_3\), at which it walks the token stack having seen that many literals of the current clause (\(w_3\): three or more); the return label \(\mathsf{back}\), at which it moves the tokens back; and the exits \(\mathsf{pass}\) and \(\mathsf{fail}\).

inductive Lab | w0 | w1 | w2 | w3 | back | pass | fail
  deriving DecidableEq

Used by 31

Used byHost labels as a sum type · Filter exits in the SAT verifier host · Labels of the SAT verifier host · Program of the SAT verifier host · Tokenizer labels in the host machine · The tokenizer embeds in the SAT verifier host · The SAT verifier machine · The TM2 SAT verifier · The return phase ends on an empty side stack · The 3SAT filter's return phase moves the side stack back · One step of the 3SAT filter's return phase · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · Conditional move between stacks · Next walking label · The clause-length filter program · Correctness of the clause-length filter · Start label of the filter · Statements of the filter · Label after a token · One step of the clause-length walk · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token · Walking label for a literal count

AbbreviationStatements of the filter#✓fully proved

The statements of a multi-stack Turing machine (Mathlib's TM2 model) with the two stacks \(T\) and \(U\), each over the symbol alphabet of the SAT verifier, the labels of the filter, and a Boolean internal state.

abbrev Stmt := TM2.Stmt (fun _ : K => Sym) Lab Bool

Uses 3 · Used by 14

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · Stack alphabet of the SAT verifier

Used byThe 3SAT filter's return phase moves the side stack back · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · The 3SAT filter walks a list of clauses within the cap · The filter walks a clause's literals within the cap · Conditional move between stacks · The clause-length filter program · Correctness of the clause-length filter · One step of the clause-length walk · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

DefinitionWalking label for a literal count#✓fully proved

The walking label after \(n\) literals of the current clause: \(w_0\), \(w_1\), \(w_2\) for \(n = 0, 1, 2\), and \(w_3\) for every \(n \ge 3\).

def wl : ℕ → Lab
  | 0 => .w0
  | 1 => .w1
  | 2 => .w2
  | _ => .w3

Uses 1 · Used by 12

Statement usesLabels of the 3SAT clause-length filter

Used byA clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · Correctness of the clause-length filter · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

DefinitionNext walking label#✓fully proved

Write \(w_i\) for the walking label after \(i\) literals of the current clause (\(w_3\): three or more). For a Boolean \(c\) (whether the filter is capped), the label after one more literal sends \(w_0\) to \(w_1\), \(w_1\) to \(w_2\) and \(w_2\) to \(w_3\); it sends \(w_3\) to the failure label when \(c\) is true and to \(w_3\) when \(c\) is false; every other label is unchanged.

def nxt (cap : Bool) : Lab → Lab
  | .w0 => .w1
  | .w1 => .w2
  | .w2 => .w3
  | .w3 => if cap then .fail else .w3
  | l => l

Uses 1 · Used by 6

Statement usesLabels of the 3SAT clause-length filter

Used byLabel after a token · One step of the clause-length walk · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

DefinitionConditional move between stacks#✓fully proved

For stacks \(a\) and \(b\) of the filter, a symbol \(s\), a label \(\ell\) and a statement \(q\): the statement that tests whether the top of stack \(a\) is \(s\) and sets the internal state to the outcome; if it is, it pops \(a\), pushes \(s\) onto \(b\) and jumps to \(\ell\), and otherwise it runs \(q\).

def mvIf (a b : K) (s : Sym) (l : Lab) (q : Stmt) : Stmt :=
  peek a (fun _ o => decide (o = some s)) <| branch id
    (pop a (fun v _ => v) <| push b (fun _ => s) <| goto fun _ => l) q

Uses 4 · Used by 4

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · Statements of the filter · Stack alphabet of the SAT verifier

Used byThe return phase ends on an empty side stack · The clause-length filter program · One step of the clause-length walk · An empty token stack ends the walk

DefinitionOne step of the clause-length walk#✓fully proved

Write \(w_0, w_1, w_2, w_3\) for the walking labels after zero, one, two, and three or more literals of the current clause. For a Boolean cap flag \(\mathrm{cap}\) and a label \(\ell\), the filter statement run at \(\ell\): if the token stack is empty, go to the label \(\mathrm{back}\); if its top is the clause marker, move it onto the side stack and go to \(w_0\); if its top is a polarity marker, move it onto the side stack and go to \(w_1\), \(w_2\), \(w_3\) when \(\ell\) is \(w_0\), \(w_1\), \(w_2\) respectively, to \(\mathrm{fail}\) when \(\ell = w_3\) and \(\mathrm{cap}\) is true, and to \(\ell\) otherwise; if its top is a name bit, move it onto the side stack and stay at \(\ell\); on any other symbol, go to \(\mathrm{fail}\) without moving it. Each test stores its outcome in the local variable.

def walk (cap : Bool) (l : Lab) : Stmt :=
  peek .T (fun _ o => o.isNone) <| branch id (goto fun _ => .back) <|
    mvIf .T .U .cl .w0 <| mvIf .T .U (.lit true) (nxt cap l) <|
    mvIf .T .U (.lit false) (nxt cap l) <| mvIf .T .U (.bit true) l <|
    mvIf .T .U (.bit false) l <| goto fun _ => .fail

Uses 6 · Used by 3

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · Statements of the filter · Conditional move between stacks · Next walking label · Stack alphabet of the SAT verifier

Used byThe clause-length filter program · An empty token stack ends the walk · One step of the clause-length walk on a token

DefinitionThe clause-length filter program#✓fully proved

For a Boolean \(c\) (whether the filter is capped), the program on the labels of the filter: at a walking label it runs one walking step with cap \(c\); at the label back it moves the top of the side stack \(U\) onto the token stack \(T\) and stays at back when that top is a token (a clause marker, a literal marker or a name bit), goes to the label pass when \(U\) is empty, and goes to the label fail otherwise; at pass and at fail it halts. Each test records its outcome in the internal state.

def prog (cap : Bool) : Lab → Stmt
  | .w0 => walk cap .w0
  | .w1 => walk cap .w1
  | .w2 => walk cap .w2
  | .w3 => walk cap .w3
  | .back => peek .U (fun _ o => o.isNone) <| branch id (goto fun _ => .pass) <|
      mvIf .U .T .cl .back <| mvIf .U .T (.lit true) .back <| mvIf .U .T (.lit false) .back <|
      mvIf .U .T (.bit true) .back <| mvIf .U .T (.bit false) .back <| goto fun _ => .fail
  | .pass => halt
  | .fail => halt

Uses 6 · Used by 18

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · Statements of the filter · Conditional move between stacks · One step of the clause-length walk · Stack alphabet of the SAT verifier

Used byProgram of the SAT verifier host · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier · The return phase ends on an empty side stack · The 3SAT filter's return phase moves the side stack back · One step of the 3SAT filter's return phase · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · Correctness of the clause-length filter · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

DefinitionStart label of the filter#✓fully proved

The filter starts at the walking label \(w_0\), the label for having seen no literal of the current clause.

def start : Lab := .w0

Uses 1 · Used by 4

Statement usesLabels of the 3SAT clause-length filter

Used byTokenizer labels in the host machine · The tokenizer embeds in the SAT verifier host · The TM2 SAT verifier · Correctness of the clause-length filter

DefinitionToken symbols of the 3SAT filter#✓fully proved

A symbol of the SAT verifier's alphabet is a token symbol when it is the clause marker, a literal marker of either polarity, or a name bit. The value markers and the dead marker are not token symbols.

def IsTok : Sym → Prop
  | .cl | .lit _ | .bit _ => True
  | _ => False

Uses 1 · Used by 4

Statement usesStack alphabet of the SAT verifier

Used byThe 3SAT filter's return phase moves the side stack back · One step of the 3SAT filter's return phase · Correctness of the clause-length filter · One step of the clause-length walk on a token

DefinitionLabel after a token#✓fully proved

Write \(w_i\) for the walking label after \(i\) literals of the current clause (\(w_3\): three or more). For a Boolean \(c\) (whether the filter is capped) and a label \(\ell\), the label reached from \(\ell\) on a symbol \(s\) is: \(w_0\) if \(s\) is a clause marker; if \(s\) is a literal marker, \(w_1\), \(w_2\) or \(w_3\) when \(\ell\) is \(w_0\), \(w_1\) or \(w_2\) respectively, the failure label when \(\ell = w_3\) and \(c\) is true, and \(\ell\) itself otherwise; and \(\ell\) itself for every other symbol.

def tgt (cap : Bool) (l : Lab) : Sym → Lab
  | .cl => .w0
  | .lit _ => nxt cap l
  | _ => l

Uses 3 · Used by 6

Statement usesLabels of the 3SAT clause-length filter · Next walking label · Stack alphabet of the SAT verifier

Used byA clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · Walking over name bits keeps the label · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

DefinitionFilter stacks from two lists#✓fully proved

For lists of symbols \(t\) and \(u\), the stack contents that put \(t\) on the token stack \(T\) and \(u\) on the side stack \(U\).

def st (t u : List Sym) : ∀ _ : K, List Sym
  | .T => t
  | .U => u

Uses 2 · Used by 16

Statement usesStacks of the 3SAT clause-length filter · Stack alphabet of the SAT verifier

Used byThe TM2 SAT verifier · The return phase ends on an empty side stack · The 3SAT filter's return phase moves the side stack back · One step of the 3SAT filter's return phase · A clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · The capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap · Correctness of the clause-length filter · Walking over name bits keeps the label · An empty token stack ends the walk · Walking over a literal advances the literal count · A capped walk fails on a literal past the third · One step of the clause-length walk on a token

TheoremOne step of the clause-length walk on a token#✓fully proved

Let \(\mathrm{cap}\) be a Boolean, \(n \in \mathbb{N}\), \(s\) a token (a name bit, a polarity marker or the clause marker), \(R\) and \(U\) lists of symbols and \(v\) a Boolean; stacks are lists written top first, and \(w_m\) is the walking label after \(m\) literals. Let \(t\) be \(w_0\) if \(s\) is the clause marker, \(w_n\) if \(s\) is a name bit, and, if \(s\) is a polarity marker, \(\mathrm{fail}\) when \(\mathrm{cap}\) is true and \(n \ge 3\) and \(w_{n+1}\) otherwise. The clause-length filter with cap flag \(\mathrm{cap}\) goes in exactly one step from label \(w_n\), local variable \(v\), token stack \(s\) on top of \(R\) and side stack \(U\) to label \(t\), local variable true, token stack \(R\) and side stack \(s\) on top of \(U\).

theorem walk_step (cap : Bool) (n : ℕ) (s : Sym) (hs : IsTok s) (R U : List Sym) (v : Bool) :
    Run (prog cap) 1 ⟨some (wl n), v, st (s :: R) U⟩
      ⟨some (tgt cap (wl n) s), true, st R (s :: U)⟩

Uses 13 · Used by 5

Statement usesToken symbols of the 3SAT filter · Stacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Label after a token · Walking label for a literal count · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · Next walking label · One step of the clause-length walk · A single step executes the statement at the current label

Used byA clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · Walking over name bits keeps the label · Walking over a literal advances the literal count · A capped walk fails on a literal past the third

TheoremWalking over name bits keeps the label#✓fully proved

Let \(\mathrm{cap}\) be a Boolean, \(n \in \mathbb{N}\) and \(R\) a list of symbols; stacks are lists written top first, \(w_n\) is the walking label after \(n\) literals and \(\mathrm{bit}(b)\) is the name-bit symbol carrying the Boolean \(b\). For all Booleans \(b_1, \dots, b_k\), every list of symbols \(U\) and every Boolean \(v\) there is a Boolean \(v'\) such that the clause-length filter with cap flag \(\mathrm{cap}\) goes in exactly \(k\) steps from label \(w_n\), local variable \(v\), token stack \(\mathrm{bit}(b_1), \dots, \mathrm{bit}(b_k)\) on top of \(R\) and side stack \(U\) to label \(w_n\), local variable \(v'\), token stack \(R\) and side stack \(\mathrm{bit}(b_k), \dots, \mathrm{bit}(b_1)\) on top of \(U\).

theorem walk_bits (cap : Bool) (n : ℕ) (R : List Sym) :
    ∀ (bs : List Bool) (U : List Sym) (v : Bool), ∃ v',
      Run (prog cap) bs.length ⟨some (wl n), v, st (bs.map Sym.bit ++ R) U⟩
        ⟨some (wl n), v', st R ((bs.map Sym.bit).reverse ++ U)⟩

Uses 10 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · Label after a token · One step of the clause-length walk on a token

Used byWalking over a literal advances the literal count

TheoremWalking over a literal advances the literal count#✓fully proved

Let \(\mathrm{cap}\) be a Boolean and \(n \in \mathbb{N}\) with \(\mathrm{cap}\) false or \(n < 3\); stacks are lists written top first, \(w_m\) is the walking label after \(m\) literals, \(\mathrm{bit}(b)\) is the name-bit symbol carrying the Boolean \(b\) and \(\mathrm{lit}(p)\) is the polarity marker of polarity \(p\). Let \(l = (i, p)\) be a literal with variable index \(i \in \mathbb{N}\) and polarity \(p\), let \(e_1, \dots, e_k\) be the binary encoding \(\mathrm{encodeNat}(i)\) of \(i\), let \(R\) and \(U\) be lists of symbols and \(v\) a Boolean. Then there is a Boolean \(v'\) such that the clause-length filter with cap flag \(\mathrm{cap}\) goes in exactly \(k + 1\) steps from label \(w_n\), local variable \(v\), token stack \(\mathrm{lit}(p), \mathrm{bit}(e_k), \dots, \mathrm{bit}(e_1)\) on top of \(R\) and side stack \(U\) to label \(w_{n+1}\), local variable \(v'\), token stack \(R\) and side stack \(\mathrm{bit}(e_1), \dots, \mathrm{bit}(e_k), \mathrm{lit}(p)\) on top of \(U\).

theorem walk_lit (cap : Bool) (n : ℕ) (hn : (cap && 3 ≤ n) = false) (l : ℕ × Bool)
    (R U : List Sym) (v : Bool) : ∃ v',
      Run (prog cap) (litRev l).length ⟨some (wl n), v, st (litRev l ++ R) U⟩
        ⟨some (wl (n + 1)), v', st R ((litRev l).reverse ++ U)⟩

Uses 13 · Used by 2

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · Next walking label · Label after a token · Walking over name bits keeps the label · One step of the clause-length walk on a token

Used byThe capped filter fails on a clause with too many literals · The filter walks a clause's literals within the cap

TheoremA capped walk fails on a literal past the third#✓fully proved

Let \(n \in \mathbb{N}\) with \(n \ge 3\) and let \(w_n\) be the walking label after \(n\) literals; stacks are lists written top first, \(\mathrm{bit}(b)\) is the name-bit symbol carrying the Boolean \(b\) and \(\mathrm{lit}(p)\) is the polarity marker of polarity \(p\). Let \(l = (i, p)\) be a literal with variable index \(i \in \mathbb{N}\) and polarity \(p\), let \(e_1, \dots, e_m\) be the binary encoding \(\mathrm{encodeNat}(i)\) of \(i\), let \(R\) and \(U\) be lists of symbols and \(v\) a Boolean. Then there are a Boolean \(v'\) and stacks \(S'\) such that the capped clause-length filter (cap flag true) goes in exactly one step from label \(w_n\), local variable \(v\), token stack \(\mathrm{lit}(p), \mathrm{bit}(e_m), \dots, \mathrm{bit}(e_1)\) on top of \(R\) and side stack \(U\) to the label \(\mathrm{fail}\) with local variable \(v'\) and stacks \(S'\).

theorem walk_lit_fail (n : ℕ) (hn : 3 ≤ n) (l : ℕ × Bool) (R U : List Sym) (v : Bool) :
    ∃ v' S', Run (prog true) 1 ⟨some (wl n), v, st (litRev l ++ R) U⟩ ⟨some .fail, v', S'⟩

Uses 12 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · Next walking label · Label after a token · One step of the clause-length walk on a token

Used byThe capped filter fails on a clause with too many literals

TheoremThe filter walks a clause's literals within the cap#✓fully proved

Let \(c\) be a Boolean (whether the filter is capped), let \(\ell_1, \dots, \ell_k\) be literals (pairs of a variable index and a polarity), let \(n\) be a natural number with \(c\) false or \(n + k \le 3\), and let \(w\) be the concatenation of the stack tokens of \(\ell_1, \dots, \ell_k\). For all lists of symbols \(R\) and \(U\) and every internal state \(v\), the filter program with cap \(c\), started at the walking label for \(n\) literals with internal state \(v\), token stack \(wR\) (top first) and side stack \(U\), reaches in exactly \(|w|\) steps the walking label for \(n + k\) literals, with some internal state, token stack \(R\) and side stack \(w^{\mathrm{rev}} U\), where \(w^{\mathrm{rev}}\) is \(w\) reversed.

theorem lits_ok (cap : Bool) (R : List Sym) : ∀ (ls : List (ℕ × Bool)) (n : ℕ) (U : List Sym)
    (v : Bool), (cap = false ∨ n + ls.length ≤ 3) → ∃ v',
      Run (prog cap) (ls.flatMap litRev).length ⟨some (wl n), v, st (ls.flatMap litRev ++ R) U⟩
        ⟨some (wl (n + ls.length)), v', st R ((ls.flatMap litRev).reverse ++ U)⟩

Uses 10 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · Walking over a literal advances the literal count

Used byThe 3SAT filter walks one clause within the cap

TheoremThe capped filter fails on a clause with too many literals#✓fully proved

Let \(n \le 3\), let \(\ell_1, \dots, \ell_k\) be literals (pairs of a variable index and a polarity) with \(3 < n + k\), and let \(w\) be the concatenation of the stack tokens of \(\ell_1, \dots, \ell_k\). For all lists of symbols \(R\) and \(U\) and every internal state \(v\), the capped filter program, started at the walking label for \(n\) literals with internal state \(v\), token stack \(wR\) (top first) and side stack \(U\), reaches the failure label, with some internal state and some stacks, in at most \(|w|\) steps.

theorem lits_fail (R : List Sym) : ∀ (ls : List (ℕ × Bool)) (n : ℕ) (U : List Sym) (v : Bool),
    n ≤ 3 → 3 < n + ls.length → ∃ v' S',
      RunLe (prog true) (ls.flatMap litRev).length ⟨some (wl n), v, st (ls.flatMap litRev ++ R) U⟩
        ⟨some .fail, v', S'⟩

Uses 11 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A literal's tokens on the token stack · Stack alphabet of the SAT verifier · Runs within a step budget

Proof usesWalking over a literal advances the literal count · A capped walk fails on a literal past the third · Exact-length runs of a TM2 machine

Used byA clause with more than three literals makes the capped 3SAT filter fail

TheoremThe 3SAT filter walks one clause within the cap#✓fully proved

Let \(C\) be a clause, and suppose the cap flag is off or \(C\) has at most three literals. Let \(\overline{C}\) be the tokens of \(C\) as they lie on the token stack (the clause marker on top, then the literals' tokens, last literal first), and let \(w_n\) be the walking label after \(n\) literals. For every \(n\), all lists of symbols \(R\) and \(U\) and every value \(v\) of the Boolean variable, there is a value \(v'\) such that the 3SAT clause-length filter takes exactly \(|\overline{C}|\) steps from label \(w_n\) with variable \(v\), token stack \(\overline{C}\) on top of \(R\) and side stack \(U\) to label \(w_{|C|}\) with variable \(v'\), token stack \(R\), and side stack the reversal of \(\overline{C}\) on top of \(U\).

The clause marker resets the literal count, and each literal then advances it.

theorem clause_ok (cap : Bool) (C : CNFClause) (hC : cap = false ∨ C.length ≤ 3) (n : ℕ)
    (R U : List Sym) (v : Bool) : ∃ v',
      Run (prog cap) (clRev C).length ⟨some (wl n), v, st (clRev C ++ R) U⟩
        ⟨some (wl C.length), v', st R ((clRev C).reverse ++ U)⟩

Uses 14 · Used by 2

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · CNF clause · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · The filter walks a clause's literals within the cap · Label after a token · One step of the clause-length walk on a token · A literal's tokens on the token stack

Used byA long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap

TheoremA clause with more than three literals makes the capped 3SAT filter fail#✓fully proved

Let \(C\) be a clause with more than three literals, let \(\overline{C}\) be its tokens as they lie on the token stack (the clause marker on top, then the literals' tokens, last literal first), and let \(w_n\) be the walking label after \(n\) literals. For every \(n\), all lists of symbols \(R\) and \(U\) and every value \(v\) of the Boolean variable, the 3SAT clause-length filter with the cap on reaches label \(\mathsf{fail}\), with some value of the variable and some stacks, in at most \(|\overline{C}|\) steps from label \(w_n\) with variable \(v\), token stack \(\overline{C}\) on top of \(R\), and side stack \(U\).

theorem clause_fail (C : CNFClause) (hC : 3 < C.length) (n : ℕ) (R U : List Sym) (v : Bool) :
    ∃ v' S', RunLe (prog true) (clRev C).length ⟨some (wl n), v, st (clRev C ++ R) U⟩
      ⟨some .fail, v', S'⟩

Uses 15 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · CNF clause · Runs within a step budget

Proof usesStatements of the filter · The capped filter fails on a clause with too many literals · Label after a token · One step of the clause-length walk on a token · A literal's tokens on the token stack · Exact-length runs of a TM2 machine

Used byA long clause makes the capped 3SAT filter fail on a list of clauses

TheoremThe 3SAT filter walks a list of clauses within the cap#✓fully proved

For a clause \(C\) let \(\overline{C}\) be its tokens as they lie on the token stack (the clause marker on top, then the literals' tokens, last literal first). Let \(C_1, \dots, C_k\) be clauses such that, for each \(i\), the cap flag is off or \(C_i\) has at most three literals. Let \(X\) be the concatenation \(\overline{C_1} \cdots \overline{C_k}\) with \(\overline{C_1}\) on top, and let \(w_n\) be the walking label after \(n\) literals. For every list of symbols \(R\), every \(n\), every list of symbols \(U\) and every value \(v\) of the Boolean variable, there are \(m\) and a value \(v'\) such that the 3SAT clause-length filter takes exactly \(|X|\) steps from label \(w_n\) with variable \(v\), token stack \(X\) on top of \(R\) and side stack \(U\) to label \(w_m\) with variable \(v'\), token stack \(R\), and side stack the reversal of \(X\) on top of \(U\).

theorem cls_ok (cap : Bool) (R : List Sym) : ∀ (cs : List CNFClause),
    (∀ C ∈ cs, cap = false ∨ C.length ≤ 3) → ∀ (n : ℕ) (U : List Sym) (v : Bool), ∃ m v',
      Run (prog cap) (cs.flatMap clRev).length ⟨some (wl n), v, st (cs.flatMap clRev ++ R) U⟩
        ⟨some (wl m), v', st R ((cs.flatMap clRev).reverse ++ U)⟩

Uses 11 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · CNF clause · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · The 3SAT filter walks one clause within the cap

Used byCorrectness of the clause-length filter

TheoremA long clause makes the capped 3SAT filter fail on a list of clauses#✓fully proved

For a clause \(C\) let \(\overline{C}\) be its tokens as they lie on the token stack (the clause marker on top, then the literals' tokens, last literal first). For a list of clauses \(C_1, \dots, C_k\), let \(X\) be the concatenation \(\overline{C_1} \cdots \overline{C_k}\) with \(\overline{C_1}\) on top, and let \(w_n\) be the walking label after \(n\) literals. If some \(C_i\) has more than three literals, then for every list of symbols \(R\), every \(n\), every list of symbols \(U\) and every value \(v\) of the Boolean variable, the 3SAT clause-length filter with the cap on reaches label \(\mathsf{fail}\), with some value of the variable and some stacks, in at most \(|X|\) steps from label \(w_n\) with variable \(v\), token stack \(X\) on top of \(R\), and side stack \(U\).

theorem cls_fail (R : List Sym) : ∀ (cs : List CNFClause), (∃ C ∈ cs, 3 < C.length) →
    ∀ (n : ℕ) (U : List Sym) (v : Bool), ∃ v' S',
      RunLe (prog true) (cs.flatMap clRev).length ⟨some (wl n), v, st (cs.flatMap clRev ++ R) U⟩
        ⟨some .fail, v', S'⟩

Uses 12 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · A clause's tokens on the token stack · Stack alphabet of the SAT verifier · CNF clause · Runs within a step budget

Proof usesA clause with more than three literals makes the capped 3SAT filter fail · The 3SAT filter walks one clause within the cap · Exact-length runs of a TM2 machine

Used byCorrectness of the clause-length filter

TheoremAn empty token stack ends the walk#✓fully proved

Let \(\mathrm{cap}\) be a Boolean, \(n \in \mathbb{N}\), \(U\) a list of symbols and \(v\) a Boolean, and let \(w_n\) be the walking label after \(n\) literals. The clause-length filter with cap flag \(\mathrm{cap}\) goes in exactly one step from label \(w_n\), local variable \(v\), empty token stack and side stack \(U\) to the label \(\mathrm{back}\), local variable true, empty token stack and side stack \(U\).

theorem walk_end (cap : Bool) (n : ℕ) (U : List Sym) (v : Bool) :
    Run (prog cap) 1 ⟨some (wl n), v, st [] U⟩ ⟨some .back, true, st [] U⟩

Uses 12 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Walking label for a literal count · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · Conditional move between stacks · Next walking label · One step of the clause-length walk · A single step executes the statement at the current label

Used byCorrectness of the clause-length filter

TheoremOne step of the 3SAT filter's return phase#✓fully proved

For either value of the cap flag, every token symbol \(s\), all lists of symbols \(R\) and \(M\) and every value \(v\) of the Boolean variable, the 3SAT clause-length filter takes exactly one step from label \(\mathsf{back}\) with variable \(v\), token stack \(R\) and side stack \(s\) on top of \(M\) to label \(\mathsf{back}\) with variable true, token stack \(s\) on top of \(R\), and side stack \(M\).

theorem back_step (cap : Bool) (s : Sym) (hs : IsTok s) (R M : List Sym) (v : Bool) :
    Run (prog cap) 1 ⟨some .back, v, st R (s :: M)⟩ ⟨some .back, true, st (s :: R) M⟩

Uses 8 · Used by 1

Statement usesToken symbols of the 3SAT filter · Stacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesA single step executes the statement at the current label

Used byThe 3SAT filter's return phase moves the side stack back

TheoremThe 3SAT filter's return phase moves the side stack back#✓fully proved

For either value of the cap flag, all lists of symbols \(M\) and \(R\) such that every symbol of \(M\) is a token symbol, and every value \(v\) of the Boolean variable, there is a value \(v'\) such that the 3SAT clause-length filter takes exactly \(|M|\) steps from label \(\mathsf{back}\) with variable \(v\), token stack \(R\) and side stack \(M\) to label \(\mathsf{back}\) with variable \(v'\), token stack the reversal of \(M\) on top of \(R\), and empty side stack.

theorem back_run (cap : Bool) : ∀ (M R : List Sym), (∀ s ∈ M, IsTok s) → ∀ v : Bool, ∃ v',
    Run (prog cap) M.length ⟨some .back, v, st R M⟩ ⟨some .back, v', st (M.reverse ++ R) []⟩

Uses 9 · Used by 1

Statement usesToken symbols of the 3SAT filter · Stacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesStatements of the filter · One step of the 3SAT filter's return phase

Used byCorrectness of the clause-length filter

TheoremThe return phase ends on an empty side stack#✓fully proved

For either value of the cap flag, every list of symbols \(R\) and every value \(v\) of the Boolean variable, the 3SAT clause-length filter takes exactly one step from label \(\mathsf{back}\) with variable \(v\), token stack \(R\) and empty side stack to label \(\mathsf{pass}\) with variable true, token stack \(R\) and empty side stack.

theorem back_end (cap : Bool) (R : List Sym) (v : Bool) :
    Run (prog cap) 1 ⟨some .back, v, st R []⟩ ⟨some .pass, true, st R []⟩

Uses 8 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Filter stacks from two lists · Stack alphabet of the SAT verifier · Exact-length runs of a TM2 machine

Proof usesConditional move between stacks · A single step executes the statement at the current label

Used byCorrectness of the clause-length filter

TheoremCorrectness of the clause-length filter#✓fully proved

Let \(c\) be a Boolean (whether the filter is capped), \(\varphi\) a CNF formula and \(v\) an internal state, and let \(S\) be stacks holding the reversed token list of \(\varphi\) on the token stack \(T\) and nothing on the side stack \(U\). Let \(b\) be the condition that \(c\) is false or every clause of \(\varphi\) has at most three literals, and let \(N\) be the number of tokens of \(\varphi\). Then the filter program with cap \(c\), started at its start label with internal state \(v\) and stacks \(S\), reaches within \(2N + 2\) steps the label pass if \(b\) holds and the label fail otherwise, with some internal state \(v'\) and stacks \(S'\); and if \(b\) holds, then \(S' = S\).

theorem run (cap : Bool) (φ : CNF) (v : Bool) (St : ∀ _ : K, List Sym)
    (hT : St .T = (toks φ).reverse) (hU : St .U = []) :
    ∃ v' S', RunLe (prog cap) (2 * (toks φ).length + 2) ⟨some start, v, St⟩
      ⟨some (if (!cap || is3 φ) then .pass else .fail), v', S'⟩ ∧
      ((!cap || is3 φ) = true → S' = St)

Uses 24 · Used by 1

Statement usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Start label of the filter · Three-literal clause test · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Proof usesToken symbols of the 3SAT filter · Statements of the filter · The return phase ends on an empty side stack · The 3SAT filter's return phase moves the side stack back · A long clause makes the capped 3SAT filter fail on a list of clauses · The 3SAT filter walks a list of clauses within the cap · Filter stacks from two lists · An empty token stack ends the walk · Walking label for a literal count · A clause's tokens on the token stack · A literal's tokens on the token stack · Tokens of a clause · Tokens of a literal · CNF clause · Exact-length runs of a TM2 machine

Used byThe TM2 SAT verifier

StructureEmitter#✓fully proved

An emitter is a multi-stack machine, given by a type of stacks and a type of labels (both with decidable equality), an alphabet for each stack and a program with boolean state, together with a start label and a different exit label at which the program halts, a token stack and a different output stack, a bijection from the SAT token symbols to the token stack's alphabet, a bijection from the output stack's alphabet to the booleans, an output map \(g\) from CNF formulas to bit strings, a bit string reserved as the output for undecodable inputs, and a monotone step bound \(B : \mathbb{N} \to \mathbb{N}\). It must satisfy: for every CNF formula \(\varphi\) whose token sequence has length \(n\), every initial state, and all stack contents in which the token stack holds the token sequence of \(\varphi\) in reverse, each token translated by the token bijection, and every other stack is empty, the program goes from the start label to the exit label in at most \(B(n)\) steps and ends with the output stack holding \(g(\varphi)\), each bit translated by the inverse of the output bijection.

Cslib.Complexity.Karp.Emitter · 37 lines

structure Emitter where
  /-- Stacks. -/
  K : Type
  [decK : DecidableEq K]
  /-- Alphabets. -/
  Γ : K → Type
  /-- Labels. -/
  L : Type
  [decL : DecidableEq L]
  /-- The program. -/
  prog : L → TM2.Stmt Γ L Bool
  /-- Start label. -/
  start : L
  /-- Exit label. -/
  done : L
  start_ne_done : start ≠ done
  prog_done : prog done = .halt
  /-- The token stack. -/
  cT : K
  /-- The output stack. -/
  cO : K
  cT_ne_cO : cT ≠ cO
  /-- Token symbols on `cT`. -/
  iT : Sym ≃ Γ cT
  /-- Output symbols on `cO` are bits. -/
  eO : Γ cO ≃ Bool
  /-- The output for a decodable input. -/
  g : CNF → List Bool
  /-- The output for an undecodable input. -/
  noOut : List Bool
  /-- The step bound, in the token count. -/
  B : ℕ → ℕ
  B_mono : Monotone B
  run : ∀ (φ : CNF) (v : Bool) (St : ∀ k, List (Γ k)), St cT = (toks φ).reverse.map iT →
    St cO = [] → (∀ k, k ≠ cT → k ≠ cO → St k = []) →
    ∃ v' S', RunLe prog (B (toks φ).length) ⟨some start, v, St⟩ ⟨some done, v', S'⟩ ∧
      S' cO = (g φ).map eO.symm

Uses 4 · Used by 24

Statement usesStack alphabet of the SAT verifier · Token sequence of a CNF formula · CNF formula · Runs within a step budget

Used byThe 3-COLOR emitter · The SAT-to-3-COLOR reduction is polynomial-time · The CLIQUE emitter · SAT ≤ CLIQUE is polynomial-time · The HAMPATH emitter · SAT ≤ HAMPATH is polynomial-time · The tokenize-then-emit machine as a host component · Emitter labels in the tokenize-then-emit machine · Tokenizer stacks in the tokenize-then-emit machine · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · The SAT-to-3SAT emitter · Exit label of the tokenize-then-emit machine · Initial stacks of the tokenize-then-emit machine · Emitter reductions out of SAT are polynomial-time · The SAT-to-3SAT reduction is polynomial-time · Stacks of the tokenize-then-emit machine · Labels of the tokenize-then-emit machine · Output of an emitter on a bit string · Program of the tokenize-then-emit machine · Tokenize, then emit · Start label of the tokenize-then-emit machine · Renaming the tokenizer's labels · Alphabets of the tokenize-then-emit machine

DefinitionOutput of an emitter on a bit string#✓fully proved

For an emitter \(E\) with output map \(g\) and a bit string \(x\): if the length-prefixed CNF decoder reads a CNF formula \(\varphi\) from \(x\) with no bits left over, the output is \(g(\varphi)\); otherwise it is the bit string that \(E\) reserves as the output for undecodable inputs.

def out (x : List Bool) : List Bool :=
  match decodeCNF x with
  | some φ => E.g φ
  | none => E.noOut

Uses 3 · Used by 6

Statement usesEmitter · Decoding a complete length-prefixed CNF formula · CNF formula

Used byThe SAT-to-3-COLOR reduction is polynomial-time · SAT ≤ CLIQUE is polynomial-time · SAT ≤ HAMPATH is polynomial-time · Emitter reductions out of SAT are polynomial-time · The SAT-to-3SAT reduction is polynomial-time · Tokenize, then emit

AbbreviationStacks of the tokenize-then-emit machine#✓fully proved

The stacks of the tokenize-then-emit machine for an emitter \(E\) are the disjoint union of the SAT tokenizer's stacks and \(E\)'s stacks.

The copy of the tokenizer's own token stack \(T\) stays unused: the tokenizer writes its tokens on \(E\)'s token stack.

abbrev K := Tokenizer.K ⊕ E.K

Uses 2 · Used by 9

Statement usesEmitter · Stacks of the SAT tokenizer

Used byThe tokenize-then-emit machine as a host component · Tokenizer stacks in the tokenize-then-emit machine · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · Initial stacks of the tokenize-then-emit machine · Emitter reductions out of SAT are polynomial-time · Program of the tokenize-then-emit machine · Tokenize, then emit · Alphabets of the tokenize-then-emit machine

DefinitionAlphabets of the tokenize-then-emit machine#✓fully proved

For an emitter \(E\), every stack of the combined machine that comes from the SAT tokenizer has the tokenizer's symbol alphabet, and every stack \(k\) that comes from \(E\) has the alphabet of \(k\) in \(E\).

@[reducible] def Γ : K E → Type
  | .inl _ => Sym
  | .inr k => E.Γ k

Uses 4 · Used by 7

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer

Used byThe tokenize-then-emit machine as a host component · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · Initial stacks of the tokenize-then-emit machine · Emitter reductions out of SAT are polynomial-time · Program of the tokenize-then-emit machine · Tokenize, then emit

AbbreviationLabels of the tokenize-then-emit machine#✓fully proved

For an emitter \(E\), the labels of the combined machine form the disjoint union of the SAT tokenizer's labels, the labels of \(E\), and the two booleans: false labels the step that writes the output \(E\) fixes for undecodable input, and true is the exit label.

abbrev L := Tokenizer.Lab ⊕ E.L ⊕ Bool

Uses 2 · Used by 8

Statement usesEmitter · Labels of the SAT tokenizer

Used byThe tokenize-then-emit machine as a host component · Emitter labels in the tokenize-then-emit machine · Exit label of the tokenize-then-emit machine · Emitter reductions out of SAT are polynomial-time · Program of the tokenize-then-emit machine · Tokenize, then emit · Start label of the tokenize-then-emit machine · Renaming the tokenizer's labels

DefinitionExit label of the tokenize-then-emit machine#✓fully proved

The labels of the tokenize-then-emit machine for an emitter \(E\) are the SAT tokenizer's labels, \(E\)'s labels and two extra labels indexed by the booleans; the exit label is the extra label indexed by true.

def fin : L E := .inr (.inr true)

Uses 3 · Used by 4

Statement usesEmitter · Labels of the tokenize-then-emit machine · Labels of the SAT tokenizer

Used byEmitter labels in the tokenize-then-emit machine · Emitter reductions out of SAT are polynomial-time · Program of the tokenize-then-emit machine · Tokenize, then emit

DefinitionTokenizer stacks in the tokenize-then-emit machine#✓fully proved

The map from the SAT tokenizer's stacks to the stacks of the tokenize-then-emit machine for an emitter \(E\) that sends the tokenizer's token stack \(T\) to \(E\)'s token stack, and each other tokenizer stack (\(X\), \(W\), \(B\), \(CC\), \(LC\)) to its own copy among the tokenizer stacks of the combined machine.

def eT : Tokenizer.K → K E
  | .T => .inr E.cT
  | .X => .inl .X
  | .W => .inl .W
  | .B => .inl .B
  | .CC => .inl .CC
  | .LC => .inl .LC

Uses 3 · Used by 2

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Stacks of the SAT tokenizer

Used byEmbedding the tokenizer's stacks into tokenize-then-emit · Tokenize, then emit

DefinitionEmbedding the tokenizer's stacks into tokenize-then-emit#✓fully proved

The stack embedding of the SAT tokenizer into the tokenize-then-emit machine for an emitter \(E\): the tokenizer's token stack \(T\) goes to \(E\)'s token stack, with token symbols translated by \(E\)'s bijection from token symbols to that stack's alphabet, and each other tokenizer stack goes to its own copy among the tokenizer stacks of the combined machine, with symbols left unchanged.

def embT : SEmb (fun _ : Tokenizer.K => Sym) (Γ E) where
  e := eT E
  inj a b h := by cases a <;> cases b <;> first | rfl | exact absurd h (by simp [eT])
  ι k := match k with
    | .T => E.iT | .X => Equiv.refl Sym | .W => Equiv.refl Sym | .B => Equiv.refl Sym
    | .CC => Equiv.refl Sym | .LC => Equiv.refl Sym

Uses 7 · Used by 2

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Tokenizer stacks in the tokenize-then-emit machine · Alphabets of the tokenize-then-emit machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Stack embedding

Used byProgram of the tokenize-then-emit machine · Tokenize, then emit

DefinitionEmbedding the emitter's stacks into tokenize-then-emit#✓fully proved

The stack embedding of an emitter \(E\) into the tokenize-then-emit machine for \(E\): each stack of \(E\) goes to its own copy among the emitter stacks of the combined machine, which carries the same alphabet, and symbols are left unchanged.

def embE : SEmb E.Γ (Γ E) where
  e := .inr
  inj := Sum.inr_injective
  ι _ := Equiv.refl _

Uses 5 · Used by 2

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Alphabets of the tokenize-then-emit machine · Stacks of the SAT tokenizer · Stack embedding

Used byProgram of the tokenize-then-emit machine · Tokenize, then emit

DefinitionRenaming the tokenizer's labels#✓fully proved

For an emitter \(E\), the tokenizer's accepting label goes to the start label of \(E\), its rejecting label goes to the label of the combined machine that writes the output \(E\) fixes for undecodable input, and every other tokenizer label goes to its own copy among the combined machine's labels.

def φT (l : Tokenizer.Lab) : L E :=
  if l = .acc then .inr (.inl E.start) else if l = .rej then .inr (.inr false) else .inl l

Uses 3 · Used by 2

Statement usesEmitter · Labels of the tokenize-then-emit machine · Labels of the SAT tokenizer

Used byProgram of the tokenize-then-emit machine · Tokenize, then emit

DefinitionEmitter labels in the tokenize-then-emit machine#✓fully proved

The map from the labels of an emitter \(E\) to the labels of the tokenize-then-emit machine for \(E\) that sends \(E\)'s exit label to the machine's exit label, and every other label of \(E\) to its own copy among the emitter labels.

def φE (l : E.L) : L E := if l = E.done then fin E else .inr (.inl l)

Uses 4 · Used by 2

Statement usesEmitter · Labels of the tokenize-then-emit machine · Exit label of the tokenize-then-emit machine · Labels of the SAT tokenizer

Used byProgram of the tokenize-then-emit machine · Tokenize, then emit

DefinitionProgram of the tokenize-then-emit machine#✓fully proved

For an emitter \(E\), the combined machine acts as follows. At a label of the SAT tokenizer it runs the tokenizer's statement for that label, with the tokenizer's token stack replaced by the token stack of \(E\) (token symbols identified with those of \(E\)), its other stacks kept as copies, and its labels renamed: acceptance goes to the start label of \(E\), rejection goes to the step that writes the undecodable-input output, and every other label goes to its own copy. At a label of \(E\) it runs the statement of \(E\) on the stacks of \(E\), with the exit label of \(E\) renamed to the exit label of the combined machine and every other label of \(E\) kept. At the label for undecodable input it pushes, in one step, the fixed output that \(E\) assigns to undecodable input, as output symbols of \(E\), onto the output stack of \(E\) (so that the stack then reads that output from the top) and goes to the exit label. At the exit label the machine halts.

def prog : L E → TM2.Stmt (Γ E) (L E) Bool
  | .inl l => mapS (embT E) (φT E) (Tokenizer.prog l)
  | .inr (.inl l) => mapS (embE E) (φE E) (E.prog l)
  | .inr (.inr false) =>
      emit (Γ := Γ E) (.inr E.cO) ((E.noOut.map E.eO.symm).reverse) (fin E)
  | .inr (.inr true) => .halt

Uses 15 · Used by 3

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Labels of the tokenize-then-emit machine · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · Exit label of the tokenize-then-emit machine · Alphabets of the tokenize-then-emit machine · Emitter labels in the tokenize-then-emit machine · Renaming the tokenizer's labels · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Translating a statement along a stack embedding · Pushing a constant list

Used byThe tokenize-then-emit machine as a host component · Emitter reductions out of SAT are polynomial-time · Tokenize, then emit

DefinitionStart label of the tokenize-then-emit machine#✓fully proved

For an emitter \(E\), the combined machine starts at the start label of the SAT tokenizer.

def start : L E := .inl Tokenizer.start

Uses 4 · Used by 2

Statement usesEmitter · Labels of the tokenize-then-emit machine · Labels of the SAT tokenizer · Start label of the SAT tokenizer

Used byEmitter reductions out of SAT are polynomial-time · Tokenize, then emit

DefinitionInitial stacks of the tokenize-then-emit machine#✓fully proved

For a bit string \(x\), the initial stack contents of the tokenize-then-emit machine for an emitter \(E\): the tokenizer's input stack \(X\) holds the bits of \(x\) in order, each written as a bit symbol, and every other stack is empty.

def init (x : List Bool) : ∀ k, List (Γ E k) := update (fun _ => []) (.inl .X) (x.map Sym.bit)

Uses 5 · Used by 2

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Alphabets of the tokenize-then-emit machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer

Used byEmitter reductions out of SAT are polynomial-time · Tokenize, then emit

DefinitionInitial stacks of the tokenizer#✓fully proved

For a bit string \(x\), the SAT tokenizer's initial stacks hold \(x\), as bit symbols, on the formula-bit stack \(X\) and leave every other stack empty.

def tokS (x : List Bool) : ∀ _ : Tokenizer.K, List Sym := update (fun _ => []) .X (x.map Sym.bit)

Uses 2 · Used by 1

Statement usesStack alphabet of the SAT verifier · Stacks of the SAT tokenizer

Used byTokenize, then emit

TheoremTokenize, then emit#✓fully proved

Let \(E\) be an emitter with step bound \(B\), and let \(x\) be a bit string. The tokenize-then-emit machine for \(E\), started at its start label with internal state false, with \(x\) as bit symbols on the tokenizer's input stack and every other stack empty, reaches its exit label, with some internal state, in at most \(2|x| + 3 + B(|x|)\) steps, and the output stack of \(E\) then holds the output on \(x\), written in the output symbols of \(E\).

theorem run (x : List Bool) :
    ∃ v S', RunLe (prog E) (2 * x.length + 3 + E.B x.length) ⟨some (start E), false, init E x⟩
      ⟨some (fin E), v, S'⟩ ∧ S' (.inr E.cO) = (out E x).map E.eO.symm

Uses 42 · Used by 1

Statement usesEmitter · Stacks of the tokenize-then-emit machine · Labels of the tokenize-then-emit machine · Exit label of the tokenize-then-emit machine · Initial stacks of the tokenize-then-emit machine · Output of an emitter on a bit string · Program of the tokenize-then-emit machine · Start label of the tokenize-then-emit machine · Alphabets of the tokenize-then-emit machine · Stacks of the SAT tokenizer · Runs within a step budget

Proof usesTokenizer stacks in the tokenize-then-emit machine · Embedding the emitter's stacks into tokenize-then-emit · Embedding the tokenizer's stacks into tokenize-then-emit · Initial stacks of the tokenizer · Emitter labels in the tokenize-then-emit machine · Renaming the tokenizer's labels · Stack alphabet of the SAT verifier · Labels of the SAT tokenizer · The tokenizer program · Rejecting run · Accepting run of the SAT tokenizer · Start label of the SAT tokenizer · Occurrence table of a formula and a witness · Table stack of an entry list · Token sequence of a CNF formula · Token count is bounded by the encoding length · Decoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · Occurrence list of a CNF formula · CNF formula · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Pushing a constant list · Pushing a list of symbols onto one stack

Used byEmitter reductions out of SAT are polynomial-time

DefinitionList of the tokenizer's stacks#✓fully proved

The list of the SAT tokenizer's six stacks in the order: the formula-bit stack \(X\), the witness-bit stack \(W\), the token stack \(T\), the table stack \(B\), the clause counter \(CC\) and the literal counter \(LC\).

def tokKs : List Tokenizer.K := [.X, .W, .T, .B, .CC, .LC]

Uses 1 · Used by 1

Statement usesStacks of the SAT tokenizer

Used byThe tokenize-then-emit machine as a host component

DefinitionThe tokenize-then-emit machine as a host component#✓fully proved

Given an emitter \(E\) with finitely many stacks, finite stack alphabets and finitely many labels, and a list of \(E\)'s stacks that contains every stack exactly once, this is the reduction-host component whose stacks, alphabets, labels and program are those of the tokenize-then-emit machine for \(E\), with its stacks listed as the SAT tokenizer's six stacks followed by the given list of \(E\)'s stacks.

Cslib.Complexity.Karp.TokThen.comp · 18 lines

def comp [Fintype E.K] [∀ k, Fintype (E.Γ k)] [Fintype E.L] (eks : List E.K) (hnd : eks.Nodup)
    (hmem : ∀ k, k ∈ eks) : Host.Comp where
  K := K E
  Γ := Γ E
  finΓ := fun k => match k with
    | .inl _ => SatVerifier.Sym.instFintype
    | .inr k => inferInstanceAs (Fintype (E.Γ k))
  L := L E
  prog := prog E
  ks := tokKs.map .inl ++ eks.map .inr
  ks_nodup := by
    refine List.nodup_append.2 ⟨(by decide : tokKs.Nodup).map Sum.inl_injective,
      hnd.map Sum.inr_injective, ?_⟩
    simp
  mem_ks := fun k => by
    rcases k with k | k
    · exact List.mem_append_left _ (List.mem_map_of_mem (mem_tokKs k))
    · exact List.mem_append_right _ (List.mem_map_of_mem (hmem k))

Uses 10 · Used by 1

Statement usesComponent machine · Emitter · Stacks of the tokenize-then-emit machine · Labels of the tokenize-then-emit machine · Program of the tokenize-then-emit machine · List of the tokenizer's stacks · Alphabets of the tokenize-then-emit machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer

Used byEmitter reductions out of SAT are polynomial-time

TheoremEmitter reductions out of SAT are polynomial-time#✓fully proved

Let \(E\) be an emitter with finitely many stacks, finite stack alphabets and finitely many labels, given together with a list of its stacks that contains every stack exactly once. Write \(B\) for the step bound of \(E\), \(g\) for its output map and \(o\) for its output on undecodable inputs, and let \(p\) be a polynomial with natural-number coefficients such that \(2n + 3 + B(n) \le p(n)\) for every \(n\). Then the map sending a bit string \(x\) to \(g(\varphi)\) when \(x\) is the binary code of a CNF formula \(\varphi\) (its clause count in unary followed by the encoded clauses), and to \(o\) otherwise, is polynomial-time computable for the canonical bit-string encoding of lists of booleans.

theorem isPolyTime_out [Fintype E.K] [∀ k, Fintype (E.Γ k)] [Fintype E.L] (eks : List E.K)
    (hnd : eks.Nodup) (hmem : ∀ k, k ∈ eks) (p : Polynomial ℕ)
    (hp : ∀ n, 2 * n + 3 + E.B n ≤ p.eval n) :
    MetaMathlibExt.ComplexityTheory.IsPolyTime (out E)

Uses 26 · Used by 4

Statement usesEmitter · Output of an emitter on a bit string · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Proof usesComponent machine · Reduction host, canonical form · Stacks of the tokenize-then-emit machine · Labels of the tokenize-then-emit machine · The tokenize-then-emit machine as a host component · Exit label of the tokenize-then-emit machine · Initial stacks of the tokenize-then-emit machine · Program of the tokenize-then-emit machine · Tokenize, then emit · Start label of the tokenize-then-emit machine · Alphabets of the tokenize-then-emit machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Exact-length runs of a TM2 machine · Runs within a step budget

Used byThe SAT-to-3-COLOR reduction is polynomial-time · SAT ≤ CLIQUE is polynomial-time · SAT ≤ HAMPATH is polynomial-time · The SAT-to-3SAT reduction is polynomial-time

TheoremTransitivity of polynomial-time many-one reductions#✓fully proved

For decision problems \(L_1\), \(L_2\) and \(L_3\), if \(L_1\) has a polynomial-time many-one reduction to \(L_2\) and \(L_2\) has one to \(L_3\), then \(L_1\) has a polynomial-time many-one reduction to \(L_3\).

theorem polyManyOneRed_trans {L₁ L₂ L₃ : DecisionProblem} (h₁ : PolyManyOneRed L₁ L₂)
    (h₂ : PolyManyOneRed L₂ L₃) : PolyManyOneRed L₁ L₃

Uses 12 · Used by 1

Statement usesPolynomial-time many-one reduction · Decision problems

Proof usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions · Polynomial-time functions are closed under composition

Used byNP-hardness transfers along reductions

TheoremNP-hardness transfers along reductions#✓fully proved

Let \(L\) and \(L'\) be decision problems. If every decision problem in NP has a polynomial-time many-one reduction to \(L\), and \(L\) has a polynomial-time many-one reduction to \(L'\), then every decision problem in NP has a polynomial-time many-one reduction to \(L'\).

theorem npHard_of_polyManyOneRed {L L' : DecisionProblem}
    (hL : ∀ A : DecisionProblem, A ∈ NP → PolyManyOneRed A L) (h : PolyManyOneRed L L') :
    ∀ A : DecisionProblem, A ∈ NP → PolyManyOneRed A L'

Uses 5 · Used by 8

Statement usesPolynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesTransitivity of polynomial-time many-one reductions

Used by3-COLOR is NP-hard · CLIQUE is NP-hard · INDEPENDENT-SET is NP-hard · VERTEX-COVER (exact size k) is NP-hard · PARTITION is NP-complete · SUBSET-SUM is NP-hard · HAMPATH is NP-hard · 3SAT is NP-hard

AbbreviationThe SAT-to-3SAT emitter#✓fully proved

The emitter whose stacks, stack alphabets, labels, program, start label and exit label are those of the 3SAT emitter machine, with that machine's token stack as its token stack and its bit-valued output stack as its output stack. Its output on a CNF formula \(\varphi\) is the binary encoding of the SAT-to-3SAT translation of \(\varphi\), its output on a bit string that encodes no CNF formula is the empty bit string, and its step bound is \(B(n) = 8(n+1)^2\): started at its start label with the reversed token sequence of \(\varphi\) on the token stack and every other stack empty, it reaches its exit label within \(B(n)\) steps, where \(n\) is the number of tokens of \(\varphi\), with the output for \(\varphi\) on the output stack.

Cslib.Complexity.Karp.emit3 · 21 lines

abbrev emit3 : Emitter where
  K := Emit3.K
  Γ := Emit3.Γ
  L := Emit3.Lab
  prog := Emit3.prog
  start := Emit3.start
  done := .done
  start_ne_done := by decide
  prog_done := rfl
  cT := .T
  cO := .O
  cT_ne_cO := by decide
  iT := Equiv.refl _
  eO := Equiv.refl _
  g φ := encodeCNF (to3 φ)
  noOut := []
  B n := 8 * (n + 1) ^ 2
  B_mono a b h := by dsimp only; gcongr
  run φ v St hT hO h0 := by
    obtain ⟨v', S', r, h⟩ := Emit3.run φ [] v St (by simpa using hT) hO h0
    exact ⟨v', S', r, by simpa using h⟩

Uses 13 · Used by 1

Statement usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · The SAT-to-3SAT emitter machine · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Start label of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Emitter · The SAT-to-3SAT translation · Stack alphabet of the SAT verifier · Token sequence of a CNF formula · Length-prefixed binary code of a CNF formula · CNF formula · Runs within a step budget

Used byThe SAT-to-3SAT reduction is polynomial-time

DefinitionThe stacks of the 3SAT emitter#✓fully proved

The list of all six stacks of the SAT-to-3SAT emitter machine, each listed once, in the order: token stack, output stack, fresh-variable counter, two scratch counters, output clause counter.

def emit3Ks : List Emit3.K := [.T, .O, .U, .Z, .W, .C]

Uses 1 · Used by 1

Statement usesStacks of the 3SAT emitter

Used byThe SAT-to-3SAT reduction is polynomial-time

TheoremThe SAT-to-3SAT reduction is polynomial-time#✓fully proved

The map on bit strings that sends the binary encoding of a CNF formula \(\varphi\) to the binary encoding of the SAT-to-3SAT translation of \(\varphi\), and sends every bit string that encodes no CNF formula to the empty bit string, is computable in polynomial time.

theorem isPolyTime_reduce3 : IsPolyTime reduce3

Uses 23 · Used by 1

Statement usesThe SAT-to-3SAT reduction on bit strings · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Proof usesStacks of the 3SAT emitter · Control labels of the SAT-to-3SAT emitter · Stack alphabets of the SAT-to-3SAT emitter · Emitter · Emitter reductions out of SAT are polynomial-time · Output of an emitter on a bit string · The SAT-to-3SAT emitter · The stacks of the 3SAT emitter · The SAT-to-3SAT translation · Stack alphabet of the SAT verifier · Decoding a complete length-prefixed CNF formula · Length-prefixed binary code of a CNF formula · CNF formula

Used bySAT reduces to 3SAT

TheoremSAT reduces to 3SAT#✓fully proved

The decision problem SAT, which accepts exactly the bit strings that encode a satisfiable CNF formula, has a polynomial-time many-one reduction to the decision problem 3SAT, which accepts exactly the bit strings that encode a satisfiable CNF formula with at most three literals per clause.

theorem satDec_polyManyOneRed_sat3Dec : PolyManyOneRed satDec sat3Dec

Uses 15 · Used by 1

Statement usesThe 3SAT decision problem · Polynomial-time many-one reduction · SAT as a decision problem

Proof usesThe SAT-to-3SAT reduction is polynomial-time · The SAT-to-3SAT reduction on bit strings · Correctness of the SAT-to-3SAT reduction on bit strings · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions

Used by3SAT is NP-hard

Theorem3SAT is NP-hard#✓fully proved

Every decision problem in NP has a polynomial-time many-one reduction to the decision problem 3SAT, which accepts exactly the bit strings that encode a satisfiable CNF formula with at most three literals per clause.

theorem sat3Dec_npHard : ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L sat3Dec

Uses 9 · Used by 1

Statement usesThe 3SAT decision problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesEvery NP problem reduces to binary-index CNF-SAT · NP-hardness transfers along reductions · SAT reduces to 3SAT · SAT as a decision problem

Used by3SAT is NP-complete

Theorem3SAT is NP-complete#✓fully proved

The decision problem 3SAT, which accepts exactly the bit strings that encode a satisfiable CNF formula with at most three literals per clause, is in NP, and every decision problem in NP has a polynomial-time many-one reduction to 3SAT.

theorem sat3Dec_npComplete :
    sat3Dec ∈ NP ∧ ∀ L : DecisionProblem, L ∈ NP → PolyManyOneRed L sat3Dec

Uses 7

Statement usesThe 3SAT decision problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof uses3SAT is NP-hard · 3SAT is in NP

109 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.