Cook-Levin for dense CNF-SAT on the canonical classes

19 fully proved

An encoding whose output alphabet contains a chosen accept symbol

DefinitionEffective alphabets with an adjoined accept symbol#✓fully proved

For a finite multi-stack Turing machine \(M\), a symbol \(a\) of its output-stack alphabet and a stack \(k\), this is the finite set of symbols that some statement of \(M\) can push on stack \(k\) (together with the whole input alphabet when \(k\) is the input stack), with \(a\) added when \(k\) is the output stack.

noncomputable def symSetX (M : FinTM2) (acc : M.Γ M.k₁) (k : M.K) : Finset (M.Γ k) :=
  symSet M k ∪ (if h : M.k₁ = k then {cast (congrArg M.Γ h) acc} else ∅)

Uses 1 · Used by 2

Statement usesPushable and input symbols of a stack

Used byTableau encoding with a chosen accept symbol · The chosen accept symbol is encodable

DefinitionTableau encoding with a chosen accept symbol#✓fully proved

Given a finite multi-stack Turing machine \(M\) and a symbol \(a\) of its output-stack alphabet, this is the encoding of \(M\) that numbers the stacks and the pairs (optional label, state) through their finite enumerations, and whose effective alphabet on each stack \(k\) is the set of symbols some statement of \(M\) can push on \(k\) (plus the whole input alphabet if \(k\) is the input stack), with \(a\) added if \(k\) is the output stack. A symbol in that set has code one more than its position in it; any other symbol has code \(0\).

Cslib.Complexity.CookLevin.Hardness.encX · 23 lines

noncomputable def encX (M : FinTM2) (acc : M.Γ M.k₁) : Enc M :=
  letI := M.kFin; letI := M.ΛFin; letI := M.σFin
  { KK := Fintype.card M.K
    kc := fun k => Fintype.equivFin M.K k
    kd := fun n => if h : n < Fintype.card M.K then (Fintype.equivFin M.K).symm ⟨n, h⟩ else M.k₀
    kc_lt := fun k => (Fintype.equivFin M.K k).2
    kd_kc := fun k => by simp
    kc_kd := fun n hn => by simp [hn]
    A0 := Fintype.card (Option M.Λ × M.σ)
    lc := fun x => Fintype.equivFin _ x
    ld := fun c => if h : c < Fintype.card (Option M.Λ × M.σ) then
      (Fintype.equivFin _).symm ⟨c, h⟩ else (none, M.initialState)
    lc_lt := fun x => (Fintype.equivFin _ x).2
    ld_lc := fun x => by rw [dite_eq_left (Fintype.equivFin _ x).2]; simp
    lc_ld := fun c hc => by rw [dite_eq_left hc]; simp
    sz := fun k => (symSetX M acc k).card
    dec := fun k i => ((symSetX M acc k).equivFin.symm i).1
    enc := fun k x => if h : x ∈ symSetX M acc k then (symSetX M acc k).equivFin ⟨x, h⟩ + 1 else 0
    enc_dec := fun k i => by simp
    push_mem := fun l k x h => ⟨(symSetX M acc k).equivFin
      ⟨x, Finset.mem_union_left _ (push_mem_symSet M l k x h)⟩, by simp⟩
    input_mem := fun x => ⟨(symSetX M acc M.k₀).equivFin
      ⟨x, Finset.mem_union_left _ (input_mem_symSet M x)⟩, by simp⟩ }

Uses 5 · Used by 2

Statement usesEffective alphabets with an adjoined accept symbol · Encoding data for a finite TM2 machine · Symbols a statement tree can push · Finite set of pushable symbols · Pushable and input symbols of a stack

Used byThe chosen accept symbol is encodable · Tableau encoding of the verifier

TheoremThe chosen accept symbol is encodable#✓fully proved

Let \(M\) be a finite multi-stack Turing machine and let \(a\) be a symbol of its output-stack alphabet. In the tableau encoding of \(M\) with \(a\) adjoined to the output alphabet, some index of the effective output-stack alphabet decodes to \(a\).

This discharges, for every machine, the accept-symbol hypothesis of the correctness theorem for the assembled formula.

theorem encX_acc (M : FinTM2) (acc : M.Γ M.k₁) : ∃ i, (encX M acc).dec M.k₁ i = acc

Uses 4 · Used by 1

Statement usesTableau encoding with a chosen accept symbol · Encoding data for a finite TM2 machine

Proof usesEffective alphabets with an adjoined accept symbol · Pushable and input symbols of a stack

Used byCorrectness of the reduction

The verifier's machine and the reduction's parameters

DefinitionAccept symbol of the verifier#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, whose output alphabet is identified with the Booleans. The accept symbol is the output symbol of \(V\) that corresponds to \(\mathrm{true}\).

def vacc : V.tm.Γ V.tm.k₁ := V.outputAlphabet.symm true

Uses 2 · Used by 5

Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Tableau encoding of the verifier · Every NP problem reduces to binary-index CNF-SAT

DefinitionTableau encoding of the verifier#✓fully proved

For a polynomial-time Turing machine \(V\) that computes a Boolean function on pairs of bit strings, reading a pair \((a, y)\) as the bits of \(a\), a separator, then the bits of \(y\), and writing its answer as one bit, this is the tableau encoding of \(V\) whose effective output alphabet is enlarged by the accept symbol: the output symbol of \(V\) for true.

noncomputable def vE : Enc V.tm := encX V.tm (vacc V)

Uses 5 · Used by 4

Statement usesTableau encoding with a chosen accept symbol · Accept symbol of the verifier · Encoding data for a finite TM2 machine · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Every NP problem reduces to binary-index CNF-SAT

DefinitionBits as indices#✓fully proved

The bijection from \(\{0, 1\}\), the indices below the number \(2\) of Booleans, onto the Booleans that is inverse to the fixed enumeration of the Booleans.

noncomputable def veqv : Fin (Fintype.card Bool) ≃ Bool := (Fintype.equivFin Bool).symm

Used by 7

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Input-bit symbol of the verifier · Correctness of the reduction · Input of the verifier on a pair · The verifier's run settles on its output · Every NP problem reduces to binary-index CNF-SAT

DefinitionInput-bit symbol of the verifier#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, whose input alphabet is identified with the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\), and let \(\beta\) be the fixed bijection from \(\{0, 1\}\) onto the Booleans. For an index \(i \in \{0, 1\}\), this is the symbol of \(V\)'s input alphabet that corresponds to the left-tagged bit \(\mathrm{inl}(\beta(i))\).

noncomputable def vι (i : Fin (Fintype.card Bool)) : V.tm.Γ V.tm.k₀ :=
  V.inputAlphabet.symm (Sum.inl (veqv i))

Uses 3 · Used by 6

Statement usesBits as indices · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Input of the verifier on a pair · The verifier's run settles on its output · Every NP problem reduces to binary-index CNF-SAT

DefinitionSeparator symbol of the verifier#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, whose input alphabet is identified with the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\). This is the symbol of \(V\)'s input alphabet that corresponds to the separator \(\#\), the element \(\mathrm{inr}(\mathrm{none})\).

def vsep : V.tm.Γ V.tm.k₀ := V.inputAlphabet.symm (Sum.inr none)

Uses 2 · Used by 6

Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Input of the verifier on a pair · The verifier's run settles on its output · Every NP problem reduces to binary-index CNF-SAT

DefinitionCertificate symbol of the verifier#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, whose input alphabet is identified with the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\). For a bit \(g\), this is the symbol of \(V\)'s input alphabet that corresponds to the right-tagged bit \(\mathrm{inr}(\mathrm{some}\ g)\).

def vY (g : Bool) : V.tm.Γ V.tm.k₀ := V.inputAlphabet.symm (Sum.inr (some g))

Uses 2 · Used by 4

Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byCorrectness of the reduction · Input of the verifier on a pair · The verifier's run settles on its output · Certificate symbols of the verifier

DefinitionCertificate symbols of the verifier#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, whose input alphabet is identified with the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\). This is the list of the symbols of \(V\)'s input alphabet corresponding to the right-tagged bits \(\mathrm{inr}(\mathrm{some}\ g)\) for \(g = \mathrm{true}\) and \(g = \mathrm{false}\), each once, in the order of a fixed enumeration of the Booleans.

noncomputable def vYs : List (V.tm.Γ V.tm.k₀) := (Finset.univ : Finset Bool).toList.map (vY V)

Uses 3 · Used by 4

Statement usesCertificate symbol of the verifier · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Every NP problem reduces to binary-index CNF-SAT

DefinitionOffset of the verifier's time bound#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, with time polynomial \(t_V\). This is a natural number \(c \ge 1\), fixed by choice, such that for some exponent \(e\) we have \(t_V(j) \le (j + c)^e\) for every natural number \(j\).

noncomputable def vc : ℕ := Classical.choose (eval_le_pow V.time)

Uses 2 · Used by 4

Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Every NP problem reduces to binary-index CNF-SAT

DefinitionExponent of the verifier's time bound#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, with time polynomial \(t_V\), and let \(c \ge 1\) be the offset of its time bound, fixed by choice so that some exponent works. This is an exponent \(e\), fixed by choice, with \(t_V(j) \le (j + c)^e\) for every natural number \(j\).

noncomputable def ve : ℕ := Classical.choose (Classical.choose_spec (eval_le_pow V.time))

Uses 2 · Used by 4

Statement usesWork alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Every NP problem reduces to binary-index CNF-SAT

TheoremInput of the verifier on a pair#✓fully proved

Let \(V\) be a polynomial-time machine computing a function of pairs of bit lists from their pair encoding, whose input alphabet is identified with the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\), and let \(\beta\) be the fixed bijection from \(\{0, 1\}\) onto the Booleans. For bit lists \(a\) and \(y\), translating the pair encoding \(a \# y\) symbol by symbol into \(V\)'s input alphabet gives the input-bit symbols of the indices \(\beta^{-1}(b)\) for the bits \(b\) of \(a\) in order, then the separator symbol, then the certificate symbols of the bits of \(y\) in order.

theorem v_input (a y : List Bool) :
    List.map V.inputAlphabet.invFun (Verifier.pairEncode (a, y)) =
      (a.map veqv.invFun).map (vι V) ++ [vsep V] ++ y.map (vY V)

Uses 6 · Used by 1

Statement usesCertificate symbol of the verifier · Bits as indices · Separator symbol of the verifier · Input-bit symbol of the verifier · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byThe verifier's run settles on its output

TheoremThe verifier's run settles on its output#✓fully proved

Let \(V\) be a machine that computes a function \(f_v\) of pairs of bit lists from their pair encoding, within \(t_V(n)\) steps on an encoding of length \(n\) for a polynomial \(t_V\) with natural-number coefficients, with input alphabet identified with the pair alphabet \(\mathrm{Bool} \oplus \mathrm{Option}\ \mathrm{Bool}\) and output alphabet identified with the Booleans. Let \(a\), \(y\) be bit lists of lengths \(|a|\), \(|y|\), and \(T\) a natural number with \(t_V(|a| + 1 + |y|) \le T\). Start \(V\) in its initial configuration with its input stack holding the symbols for the left-tagged bits \(\mathrm{inl}(b)\) of \(a\), then the separator \(\mathrm{inr}(\mathrm{none})\), then the symbols for the right-tagged bits \(\mathrm{inr}(\mathrm{some}\ b)\) of \(y\), and run it for \(T\) steps, a halted configuration staying unchanged. The result is the halted configuration, in the initial internal state, whose output stack holds exactly the one output symbol for \(f_v(a, y)\) and whose other stacks are empty.

theorem v_run (a y : List Bool) {T : ℕ} (hT : V.time.eval (a.length + 1 + y.length) ≤ T) :
    runI V.tm (initList V.tm ((a.map veqv.invFun).map (vι V) ++ [vsep V] ++ y.map (vY V))) T =
      haltList V.tm [V.outputAlphabet.symm (fv (a, y))]

Uses 9 · Used by 1

Statement usesCertificate symbol of the verifier · Bits as indices · Separator symbol of the verifier · Input-bit symbol of the verifier · Idle-extended run · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Proof usesInput of the verifier on a pair · The idle-extended run stays at the halting configuration

Used byCorrectness of the reduction

DefinitionThe Cook–Levin reduction#✓fully proved

Let \(V\) be a polynomial-time Turing machine that computes a Boolean function on pairs of bit strings, reading a pair \((a, y)\) as the bits of \(a\), a separator, then the bits of \(y\), and writing its answer as one bit; let \(t\) be its time bound and fix constants \(c \ge 1\) and \(e\) with \(t(j) \le (j + c)^e\) for all \(j\). For a polynomial \(p\) with natural-number coefficients, the reduction sends a bit string \(a\) of length \(n\) to the dense bit encoding of the tableau formula \(\Phi\) of \(V\), built with the encoding of \(V\) whose output alphabet contains the output symbol \(\mathrm{acc}\) for true, for the input prefix \(x\) made of the bits of \(a\) followed by the separator, the certificate symbols of \(V\) (one per bit) as the allowed symbols after \(x\), the accept symbol \(\mathrm{acc}\), width \(m = n + 1 + p(n)\) and \(T = (m + c)^e\) steps.

noncomputable def red (p : Polynomial ℕ) : List Bool → List Bool :=
  fR (vE V) (fun l : List Bool => l) veqv (vYs V) (vacc V) (vι V) (vsep V) p (vc V) (ve V)

Uses 11 · Used by 4

Statement usesTableau encoding of the verifier · Certificate symbols of the verifier · Accept symbol of the verifier · Offset of the verifier's time bound · Exponent of the verifier's time bound · Bits as indices · Separator symbol of the verifier · Input-bit symbol of the verifier · The Cook–Levin reduction function · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Used byEvery NP problem reduces to dense CNF-SAT · The Cook–Levin reduction is polynomial-time · Correctness of the reduction · Every NP problem reduces to binary-index CNF-SAT

TheoremCorrectness of the reduction#✓fully proved

Let \(V\) be a polynomial-time Turing machine that computes a Boolean function \(f\) on pairs of bit strings, reading a pair \((a, y)\) as the bits of \(a\), a separator, then the bits of \(y\), and writing its answer as one bit. Let \(p\) be a polynomial with natural-number coefficients, \(R\) a relation on bit strings with \(R(a, y)\) iff \(f(a, y)\) is true, and \(L'\) a predicate on bit strings such that \(L'(a)\) holds iff some bit string \(y\) of length at most \(p(|a|)\) satisfies \(R(a, y)\). Then for every bit string \(a\), \(L'(a)\) holds iff the image of \(a\) under the reduction built from \(V\) and \(p\) is in CNF-SAT.

theorem v_correct {R : List Bool → List Bool → Prop} {p : Polynomial ℕ} {L' : List Bool → Prop}
    (hfv : ∀ q : List Bool × List Bool, R q.1 q.2 ↔ fv q = true)
    (hL : ∀ a, L' a ↔ ∃ y : List Bool, y.length ≤ p.eval a.length ∧ R a y) (a : List Bool) :
    L' a ↔ SAT (red V p a)

Uses 28 · Used by 2

Statement usesThe Cook–Levin reduction · Dense CNF-SAT · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\)

Proof usesThe formula emitted by the host · Correctness of the assembled formula · The chosen accept symbol is encodable · Tableau encoding of the verifier · Certificate symbol of the verifier · Certificate symbols of the verifier · The verifier's run settles on its output · Accept symbol of the verifier · Offset of the verifier's time bound · Exponent of the verifier's time bound · Bits as indices · Separator symbol of the verifier · Input-bit symbol of the verifier · The precomputed time bound · Total length bound · Accepting configuration · Acceptance of a halting configuration · Idle-extended run · Dense CNF formula · Satisfaction of a dense CNF formula · Dense decoding of CNF formulas · Decoding inverts the dense encoding · Dense encoding of a CNF formula · Evaluation of a natural-number polynomial is monotone

Used byEvery NP problem reduces to dense CNF-SAT · Every NP problem reduces to binary-index CNF-SAT

TheoremThe Cook–Levin reduction is polynomial-time#✓fully proved

Let \(V\) be a polynomial-time Turing machine that computes a Boolean function on pairs of bit strings, reading a pair \((a, y)\) as the bits of \(a\), a separator, then the bits of \(y\), and writing its answer as one bit. For every polynomial \(p\) with natural-number coefficients, the reduction built from \(V\) and \(p\) is polynomial-time computable with respect to the canonical bit-string encodings.

theorem isPolyTime_red (p : Polynomial ℕ) : IsPolyTime (red V p)

Uses 25 · Used by 2

Statement usesThe Cook–Levin reduction · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · 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 usesTableau encoding of the verifier · Certificate symbols of the verifier · Accept symbol of the verifier · Offset of the verifier's time bound · Exponent of the verifier's time bound · Bits as indices · Separator symbol of the verifier · Input-bit symbol of the verifier · The Cook–Levin reduction function · The reduction machine as a polynomial-time computation · Polynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Polynomial-time TM2-computable functions are closed under composition

Used byEvery NP problem reduces to dense CNF-SAT · Every NP problem reduces to binary-index CNF-SAT

Hardness and completeness

TheoremEvery NP problem reduces to dense CNF-SAT#✓fully proved

Every decision problem \(L\) in NP has a polynomial-time many-one reduction to dense CNF-SAT: a polynomial-time computable map \(f\) on bit strings such that, for every bit string \(x\), \(L\) accepts \(x\) exactly when dense CNF-SAT accepts \(f(x)\).

theorem denseSatDec_npHard (L : DecisionProblem) (hL : L ∈ NP) :
    Cslib.CookLevin.PolyManyOneRed L denseSatDec

Uses 22 · Used by 1

Statement usesDense CNF-SAT as a decision problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesThe Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Correctness of the reduction · Dense CNF-SAT · Canonical bit-list decoder · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · 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 · The composite polynomial-time TM2 computation

Used byCook-Levin for dense CNF-SAT

TheoremCook-Levin for dense CNF-SAT#✓fully proved

Dense CNF-SAT is NP-complete: it lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to dense CNF-SAT.

theorem denseSatDec_npComplete :
    denseSatDec ∈ NP ∧
      ∀ L : DecisionProblem, L ∈ NP → Cslib.CookLevin.PolyManyOneRed L denseSatDec

Uses 7

Statement usesDense CNF-SAT as a decision problem · Polynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP

Proof usesEvery NP problem reduces to dense CNF-SAT · Dense CNF-SAT is in NP

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.