The SAT verifier machine to SAT is in NP

DefinitionThe SAT verifier machine#✓fully proved

For a flag \(\mathit{cap}\), the host machine is the finite multi-stack Turing machine whose stacks are the host stacks, with the input stack as input (its alphabet is that of the pair encoding: tagged formula bits, a separator and tagged witness bits), the output stack (alphabet the booleans) as output, the host alphabets on all stacks, the host labels as labels, the first phase-0 label as start label, a boolean internal state initially false, and the host program with flag \(\mathit{cap}\) as program.

def tm (cap : Bool) : FinTM2 where
  K := HK
  k₀ := .inp
  k₁ := .out
  Γ := HΓ
  Λ := HLab
  main := .ph .m1
  σ := Bool
  initialState := false
  m := hprog cap

Uses 10 · Used by 4

Statement usesLabels of the 3SAT clause-length filter · Driver labels of the clause check · Labels of the lookup machine · Stacks of the SAT verifier host · Labels of the SAT verifier host · Host labels as a sum type · Stack alphabets of the SAT verifier host · Phase-0 labels of the SAT verifier host · Program of the SAT verifier host · Labels of the SAT tokenizer

Used byInitial configuration of the SAT verifier machine · Step bound of the SAT verifier machine · Explicit step bound of the SAT verifier machine · The TM2 SAT verifier

TheoremPhase 0 of the SAT verifier host#✓fully proved

Let \(c\) be a flag, \(x\) and \(w\) bit strings of lengths \(m\) and \(n\), \(v\) an internal state, and \(S\) host stacks whose input stack holds the pair encoding \(x \# w\) and whose other stacks are all empty. Then there are an internal state \(v'\) and host stacks \(S'\) such that the host program with flag \(c\) runs in exactly \(2m + 2n + 5\) steps from the configuration at the phase-0 label \(m_1\) with internal state \(v\) and stacks \(S\) to the configuration at the start label of the tokenizer with internal state \(v'\) and stacks \(S'\), the stack \(X\) of \(S'\) holds the bits of \(x\) in order and the stack \(W\) holds the bits of \(w\) in order, each as a name-bit symbol, and every other stack of \(S'\) is empty.

theorem phase0_run (x w : List Bool) (v : Bool) (S : ∀ k, List (HΓ k))
    (hinp : S .inp = Cslib.Complexity.DenseSAT.Verifier.pairEncode (x, w))
    (h0 : ∀ k, k ≠ .inp → S k = []) :
    ∃ v' S', Run (hprog cap) (2 * x.length + 2 * w.length + 5) ⟨some (.ph .m1), v, S⟩
      ⟨some (.tok Tokenizer.start), v', S'⟩ ∧
      S' .X = x.map Sym.bit ∧ S' .W = w.map Sym.bit ∧ ∀ k, k ≠ .X → k ≠ .W → S' k = []

Uses 17 · Used by 1

Statement usesPair encoding \(w \# y\) · Stacks of the SAT verifier host · Labels of the SAT verifier host · Stack alphabets of the SAT verifier host · Phase-0 labels of the SAT verifier host · Program of the SAT verifier host · Stack alphabet of the SAT verifier · Labels of the SAT tokenizer · Start label of the SAT tokenizer · Exact-length runs of a TM2 machine

Proof usesWork alphabet of the dense-SAT verifier · Reading a witness bit in the SAT host · Reading a formula bit in the SAT host · Reading a symbol as a name bit · Flag bit of a machine state · A single step executes the statement at the current label · Running the bit-moving loop

Used byThe TM2 SAT verifier

TheoremThe tokenizer embeds in the SAT verifier host#✓fully proved

For every flag \(c\), the tokenizer program embeds in the host program with flag \(c\) along the stack embedding of the tokenizer into the host and the map of tokenizer labels into host labels, which sends the tokenizer's accepting label to the start label of the clause-length filter, its rejecting label to the cleanup label with answer false, and every other label \(\ell\) to the host label running the tokenizer at \(\ell\). That is, for every tokenizer label \(\ell\), either the tokenizer's statement at \(\ell\) is the halt statement, or the host program's statement at the image of \(\ell\) is the tokenizer's statement at \(\ell\) translated along this embedding and label map.

theorem embeds_tok : Embeds embT φT Tokenizer.prog (hprog cap)

Uses 35 · Used by 1

Statement usesStacks of the SAT verifier host · Labels of the SAT verifier host · Stack alphabets of the SAT verifier host · Stack embedding of the tokenizer into the host · Program of the SAT verifier host · Tokenizer labels in the host machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Embedding of a machine in a host

Proof usesStacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Start label of the filter · Driver labels of the clause check · Stacks of the clause check · The clause-check driver with a lookup sub-program · Labels of the lookup machine · Start label of the lookup machine · Phase-0 labels of the SAT verifier host · Reading a witness bit in the SAT host · Reading a formula bit in the SAT host · Stack embedding of the clause-check driver into the host · Stack embedding of the clause-length filter into the host · The embedded lookup program · Stacks emptied by the SAT verifier's cleanup · Driver labels in the SAT host · Filter exits in the SAT verifier host · Reading a symbol as a name bit · Start label of the SAT tokenizer · Translating a statement along a stack embedding · Flag bit of a machine state · Cleanup round · Bit-moving loop

Used byThe TM2 SAT verifier

TheoremThe embedded lookup meets the lookup contract#✓fully proved

The clause-check driver, with the embedded lookup program as its lookup sub-program and the lookup's start label as the label it calls, meets the driver's lookup contract with constants \(a = 8\) and \(b = 4\): from the lookup's start label, with a reversed name block \(q\) on the token stack \(T\) above a rest that does not begin with a name bit, the table stack of an entry list \(es\) on \(B\), and the stacks \(S\), \(A\), \(C\), \(V\) empty, it reaches the driver's return label within \(8m + 4\) steps, where \(m\) is the length of the table stack, with \(V\) holding the single bit of the live value of \(q\) in \(es\) and every other stack unchanged.

theorem lookupSpec : Check.LookupSpec lkH Lookup.start 8 4

Uses 27 · Used by 1

Statement usesThe lookup contract · Labels of the lookup machine · Start label of the lookup machine · The embedded lookup program

Proof usesDriver labels of the clause check · Stacks of the clause check · Clause-check statements · The clause-check driver · The clause-check driver with a lookup sub-program · Table entries · Stacks of the lookup machine · The lookup program · Correctness of the SAT-verifier lookup machine · Placement of the lookup's stacks in the clause-check driver · Stack embedding of the lookup into the clause-check driver · Lookup labels in the clause-check driver · Stack alphabet of the SAT verifier · Reading a symbol as a name bit · Live value of a name in a table · Table stack of an entry list · 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 · Runs within a step budget

Used byThe TM2 SAT verifier

TheoremThe cleanup stacks are distinct#✓fully proved

The list of stacks emptied by the cleanup of the SAT verifier host has no repeated entries.

theorem workKs_nodup : workKs.Nodup

Uses 2 · Used by 1

Statement usesStacks of the SAT verifier host · Stacks emptied by the SAT verifier's cleanup

Used byCleanup of the SAT host

TheoremCleanup of the SAT host#✓fully proved

Let \(m\) be a natural number and let \(S\) assign contents to the host stacks so that every stack has length at most \(m\) and the output stack is empty. Then for every flag \(c\), answer bit \(a\) and internal state \(v\), the host program with flag \(c\) goes in at most \(m + 1\) steps from the cleanup label with answer \(a\), internal state \(v\) and stacks \(S\) to the final label with answer \(a\), internal state false and every stack empty.

theorem clean_host (ans : Bool) (m : ℕ) (v : Bool) (S : ∀ k, List (HΓ k))
    (hl : ∀ k, (S k).length ≤ m) (ho : S .out = []) :
    RunLe (hprog cap) (m + 1) ⟨some (.clean ans), v, S⟩ ⟨some (.fin ans), false, fun _ => []⟩

Uses 9 · Used by 1

Statement usesStacks of the SAT verifier host · Labels of the SAT verifier host · Stack alphabets of the SAT verifier host · Program of the SAT verifier host · Runs within a step budget

Proof usesStacks emptied by the SAT verifier's cleanup · The cleanup stacks are distinct · Flag bit of a machine state · Cleanup empties its stacks

Used byCleanup phase of the SAT verifier host

TheoremName lengths in an occurrence table#✓fully proved

For every list \(n_0, \dots, n_{k-1}\) of natural numbers and every list \(w\) of bits, the names of the entries of the occurrence table of \(n_0, \dots, n_{k-1}\) and \(w\), in order, have the lengths of the binary codes of \(n_0, \dots, n_{k-1}\) (Mathlib's encoding of natural numbers as bit lists).

theorem entsOf_map_length (ns : List ℕ) :
    ∀ w : List Bool,
      (entsOf ns w).map (fun e => e.1.length) = ns.map fun n => (encodeNat n).length

Uses 2 · Used by 1

Statement usesTable entries · Occurrence table of a list of variables

Used byThe TM2 SAT verifier

DefinitionInitial stacks of the SAT verifier host#✓fully proved

For a word \(l\) over the input alphabet \(G\), the initial host stacks on \(l\) hold \(l\) on the input stack and leave every other stack empty.

def initS (l : List G) : ∀ k, List (HΓ k) := update (fun _ => []) HK.inp l

Uses 3 · Used by 2

Statement usesInput alphabet of the SAT verifier host · Stacks of the SAT verifier host · Stack alphabets of the SAT verifier host

Used byInitial configuration of the SAT verifier machine · The TM2 SAT verifier

DefinitionTokenizer stacks after phase 0#✓fully proved

For bit lists \(x\) and \(w\), these tokenizer stack contents put the bits of \(x\) on the formula stack \(X\) and the bits of \(w\) on the witness stack \(W\) (each bit as a bit symbol), and leave every other tokenizer stack (token, table and the two counters) empty.

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

Uses 2 · Used by 1

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

Used byThe TM2 SAT verifier

DefinitionDriver stacks after tokenization#✓fully proved

For a CNF formula \(\varphi\) and a witness \(w\), these are the contents of the clause-check driver's stacks once the tokenizer has accepted \(\varphi\): the token stack holds the token list of \(\varphi\) reversed, the table stack holds the table-stack encoding of the occurrence table of \(\varphi\) and \(w\), and every other stack is empty.

def chkS (φ : CNF) (w : List Bool) : ∀ _ : Check.K, List Sym
  | .T => (toks φ).reverse
  | .B => tblStk (ents φ w)
  | _ => []

Uses 6 · Used by 1

Statement usesStacks of the clause check · Stack alphabet of the SAT verifier · Occurrence table of a formula and a witness · Table stack of an entry list · Token sequence of a CNF formula · CNF formula

Used byThe TM2 SAT verifier

DefinitionStep budget before the cleanup#✓fully proved

For an input length \(N\), the number \((2N + 5) + (2N + 2) + (2N + 2) + (N(8N + 9) + 1)\).

It budgets the host steps before the cleanup: its four summands budget phase 0, the tokenizer, the clause-length filter and the clause-check driver.

def preSteps (N : ℕ) : ℕ := (2 * N + 5) + (2 * N + 2) + (2 * N + 2) + (N * (8 * N + 9) + 1)

Used by 2

Used byExplicit step bound of the SAT verifier machine · The TM2 SAT verifier

TheoremCleanup phase of the SAT verifier host#✓fully proved

Fix either value of the 3SAT flag, an answer bit \(b\), a natural number \(m\), an internal state \(v\), and host stacks \(S\) such that every stack of \(S\) has length at most \(m\) and the output stack of \(S\) is empty. Then for some \(n \le m + 2\), the host program runs in exactly \(n\) steps from the configuration at the cleanup label with answer \(b\), internal state \(v\) and stacks \(S\) to the halted configuration with internal state false, the one-symbol word \(b\) on the output stack and every other stack empty.

theorem finish (ans : Bool) (m : ℕ) (v : Bool) (S : ∀ k, List (HΓ k))
    (hl : ∀ k, (S k).length ≤ m) (ho : S .out = []) :
    ∃ n, n ≤ m + 2 ∧ Run (hprog cap) n ⟨some (.clean ans), v, S⟩
      ⟨none, false, update (fun _ => []) HK.out [ans]⟩

Uses 8 · Used by 1

Statement usesStacks of the SAT verifier host · Labels of the SAT verifier host · Stack alphabets of the SAT verifier host · Program of the SAT verifier host · Exact-length runs of a TM2 machine

Proof usesCleanup of the SAT host · A single step executes the statement at the current label · Runs within a step budget

Used byThe TM2 SAT verifier

DefinitionAnswer of the SAT host#✓fully proved

For a flag \(c\) and a pair \((x, w)\) of bit strings, the host's answer is false if \(x\) does not decode to a CNF formula. If \(x\) decodes to a formula \(\varphi\), give each variable \(n\) the value \(w_i\) (counting from \(0\)), where \(i\) is the first position of \(n\) in the list of variable occurrences of \(\varphi\) read clause by clause, and the value false if \(i \ge |w|\). Then the answer is true exactly when both (a) \(c\) is false or every clause of \(\varphi\) has at most three literals, and (b) every clause of \(\varphi\) contains a literal \((n, b)\) whose variable \(n\) has value \(b\).

def ans (p : List Bool × List Bool) : Bool :=
  ((decodeCNF p.1).map fun φ => (!cap || Karp.is3 φ) && checkSpec φ (ents φ p.2)).getD false

Uses 5 · Used by 5

Statement usesThree-literal clause test · Clause check against an occurrence table · Occurrence table of a formula and a witness · Decoding a complete length-prefixed CNF formula · CNF formula

Used byThe SAT host's answer is polynomial-time · The SAT verifier is polynomial-time · The TM2 SAT verifier · Answer of the SAT host with the three-literal filter · 3SAT is in NP

DefinitionExplicit step bound of the SAT verifier machine#✓fully proved

For a flag \(\mathit{cap}\) and an input length \(N\), let \(s(N) = (2N + 5) + (2N + 2) + (2N + 2) + (N(8N + 9) + 1)\) be the number of steps allowed before the cleanup, and let \(p\) be the per-step push budget of the host machine with that flag. The total step bound is \(s(N) + (N + p \cdot s(N)) + 2\).

When the cleanup starts, every stack has length at most \(N + p \cdot s(N)\); the cleanup and the output step then take at most that many steps plus \(2\).

noncomputable def totalSteps (N : ℕ) : ℕ :=
  preSteps N + (N + TM2Composition.pushBound (tm cap) * preSteps N) + 2

Uses 3 · Used by 1

Statement usesStep budget before the cleanup · The SAT verifier machine · Push bound of a finite multi-stack Turing machine

Used byThe TM2 SAT verifier

TheoremInitial configuration of the SAT verifier machine#✓fully proved

For every flag \(c\) and every word \(l\) over the input alphabet \(G\) of the host, the initial configuration of the SAT verifier machine with flag \(c\) on \(l\) (its start label, its initial internal state, \(l\) on the input stack and every other stack empty) is the configuration at the phase-0 label \(m_1\) with internal state false and the initial host stacks on \(l\).

theorem initList_tm (l : List G) : initList (tm cap) l = ⟨some (.ph .m1), false, initS l⟩

Uses 6 · Used by 1

Statement usesInput alphabet of the SAT verifier host · Labels of the SAT verifier host · Phase-0 labels of the SAT verifier host · Initial stacks of the SAT verifier host · The SAT verifier machine

Proof usesStacks of the SAT verifier host

Used byThe TM2 SAT verifier

DefinitionStep bound of the SAT verifier machine#✓fully proved

For a flag \(\mathit{cap}\), let \(p\) be the per-step push budget of the host machine with that flag (the sum over its labels of the number of push instructions in each label's statement). The step bound is the polynomial \((p + 1)(8X^2 + 15X + 10) + X + 2\) with natural-number coefficients, in the input length \(X\).

noncomputable def time : Polynomial ℕ :=
  Polynomial.C (TM2Composition.pushBound (tm cap) + 1) *
      (Polynomial.C 8 * Polynomial.X ^ 2 + Polynomial.C 15 * Polynomial.X + Polynomial.C 10) +
    Polynomial.X + Polynomial.C 2

Uses 2 · Used by 1

Statement usesThe SAT verifier machine · Push bound of a finite multi-stack Turing machine

Used byThe TM2 SAT verifier

DefinitionThe TM2 SAT verifier#✓fully proved

For a flag \(\mathit{cap}\), the host machine with that flag computes the host's answer in polynomial time. For every pair \((x, w)\) of bit lists, started on the input \(x \# w\) (the bits of \(x\), a separator, then the bits of \(w\)), it halts with the single bit \(\mathrm{ans}_{\mathit{cap}}(x, w)\) on its output stack and every other stack empty within \(T(n)\) steps, where \(n\) is the length of \(x \# w\) and \(T\) is the host's polynomial step bound. Here \(\mathrm{ans}_{\mathit{cap}}(x, w)\) is false unless \(x\) decodes to a CNF formula \(\varphi\); in that case it is true exactly when \(\varphi\) passes the clause check against the table built from \(w\) and, if \(\mathit{cap}\) is true, every clause of \(\varphi\) has at most three literals.

Cslib.Complexity.SatVerifier.Machine.verifier · 23 lines

noncomputable def verifier :
    TM2ComputableInPolyTime Cslib.Complexity.DenseSAT.Verifier.pairEncode (fun b : Bool => [b])
      (fun p => ans cap p) where
  tm := tm cap
  inputAlphabet := Equiv.refl G
  outputAlphabet := Equiv.refl Bool
  time := time cap
  outputsFun := fun p => by
    obtain ⟨x, w⟩ := p
    have h := host_run cap x w
    have hn := (Classical.choose_spec h).1
    have r := (Classical.choose_spec h).2
    unfold TM2OutputsInTime
    refine { steps := Classical.choose h, evals_in_steps := ?_, steps_le_m := ?_ }
    · change (flip bind (TM2.step (hprog cap)))^[_] (some (initList (tm cap) _)) =
        Option.map (haltList (tm cap)) (some _)
      erw [List.map_id, List.map_id, initList_tm, Option.map_some, haltList_tm]
      exact r
    · refine hn.trans (le_of_eq ?_)
      simp only [totalSteps, time, preSteps_eq, Polynomial.eval_add, Polynomial.eval_mul,
        Polynomial.eval_C,
        Polynomial.eval_pow, Polynomial.eval_X]
      ring

Uses 79 · Used by 1

Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Stacks of the 3SAT clause-length filter · Labels of the 3SAT clause-length filter · The clause-length filter program · Correctness of the clause-length filter · Filter stacks from two lists · Start label of the filter · Three-literal clause test · Driver labels of the clause check · Stacks of the clause check · The clause-check driver with a lookup sub-program · The clause check · Table entries · Labels of the lookup machine · Start label of the lookup machine · Input alphabet of the SAT verifier host · Stacks of the SAT verifier host · Labels of the SAT verifier host · Stack alphabets of the SAT verifier host · Phase-0 labels of the SAT verifier host · Answer of the SAT host · Driver stacks after tokenization · Placement of the filter's stacks in the host · Placement of the tokenizer's stacks in the host · Stack embedding of the clause-check driver into the host · Stack embedding of the clause-length filter into the host · Stack embedding of the tokenizer into the host · The tokenizer embeds in the SAT verifier host · Name lengths in an occurrence table · Cleanup phase of the SAT verifier host · Program of the SAT verifier host · Initial configuration of the SAT verifier machine · Initial stacks of the SAT verifier host · The embedded lookup program · The embedded lookup meets the lookup contract · Phase 0 of the SAT verifier host · Step budget before the cleanup · Step bound of the SAT verifier machine · The SAT verifier machine · Tokenizer stacks after phase 0 · Explicit step bound of the SAT verifier machine · Driver labels in the SAT host · Filter exits in the SAT verifier host · Tokenizer labels in the host machine · Stack alphabet of the SAT verifier · Stacks of the SAT tokenizer · Labels of the SAT tokenizer · The tokenizer program · Rejecting run · Accepting run of the SAT tokenizer · Start label of the SAT tokenizer · Clause check against an occurrence table · Tokens of a clause · Symbols of a table entry · Occurrence table of a formula and a witness · Occurrence table of a list of variables · Tokens of a literal · Closing marker of a table entry · 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 · CNF clause · Push bound of a finite multi-stack Turing machine · Number of push instructions in a TM2 statement · 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 · Runs within a step budget · A halted run stays halted

Used byThe SAT host's answer is polynomial-time

TheoremThe SAT host's answer is polynomial-time#✓fully proved

For each value of the flag \(\mathit{cap}\) (with or without the three-literal clause filter), the host's answer, as a function from pairs \((x, w)\) of bit strings to Booleans, is polynomial-time computable under the canonical bitstring encodings.

theorem isPolyTime_ans : ComplexityTheory.IsPolyTime fun p => ans cap p

Uses 15 · Used by 2

Statement usesAnswer of the SAT host · 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 usesPolynomial-time conversion to the verifier's pair encoding · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · The TM2 SAT verifier · Polynomial-time TM2-computable functions are closed under composition

Used byThe SAT verifier is polynomial-time · 3SAT is in NP

TheoremThe SAT verifier is polynomial-time#✓fully proved

The function that maps a pair \((x, w)\) of bit strings to the Boolean answer of the SAT verifier on \((x, w)\) (its return value, ignoring its declared time cost) is polynomial-time computable under the canonical bitstring encodings.

theorem isPolyTime_satVerifier :
    ComplexityTheory.IsPolyTime fun xw => (satVerifier xw).ret

Uses 18 · Used by 3

Statement usesThe SAT verifier · 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 usesThree-literal clause test · Answer of the SAT host · The SAT host's answer is polynomial-time · Clause check against an occurrence table · Occurrence table of a formula and a witness · The SAT verifier's answer through the occurrence table · Decoding a complete length-prefixed CNF formula · CNF formula

Used byPreimage of SAT under a polynomial-time map is in NP · SAT is in NP · Cook–Levin theorem

TheoremSAT is in NP#✓fully proved

The decision problem SAT, which accepts exactly the bit strings that encode a satisfiable CNF formula, belongs to the class NP.

Variable indices are binary-coded in the encoding of formulas.

theorem satDec_mem_NP : satDec ∈ ComplexityTheory.NP

Uses 6

Statement usesSAT as a decision problem · Complexity classes · Decision problems · The complexity class NP

Proof usesThe SAT verifier is polynomial-time · SAT is in NP if its verifier is polynomial-time

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.