The succinct Cook–Levin theorem: the statement

MIPRE.SAT.SuccinctCookLevin is blueprint thm:succinct-sat — the paper's prop:standard-succinct-sat (answer_reduction.tex, sec:cook-levin) — in the vocabulary of the ambient model: a polynomial-time algorithm that, on a decider 𝒟, an index n, a time bound T, a question length Q, a description-length bound σ and questions x, y, outputs a circuit C on 3m + 3 inputs which succinctly describes a 3SAT formula C.formula3 m on 2^m variables (def:succinct-formulas: C(i₁, i₂, i₃, o₁, o₂, o₃) = 1 iff x_{i₁}^{o₁} ∨ x_{i₂}^{o₂} ∨ x_{i₃}^{o₃} is a clause), such that

1. for all a, b ∈ {0,1}^{2T}, the formula has a satisfying assignment extending a and b on its first 4T variables iff a and b are the two-bit tape encodings (tapeBits: 0 ↦ 00, 1 ↦ 01, blank ↦ 10) of strings of length at most T on which 𝒟 accepts (n, x, y, ·, ·) within cost T (Decider.AcceptsWithin);
2. m = O(log T + log σ) and 2^m ≥ 4T;
3. C has at most s(n, T, Q, σ) = poly(log n, log T, Q, σ) gates;
4. the algorithm runs in polynomial time (PolyTimeFun, whose bound is a polynomial in the size of the input, itself at most poly(log n, log T, Q, σ) under the validity hypotheses);
5. m and s are polynomial-time computable from the parameters.

"Within T steps" is cost at most T in the ambient model, the reading of every time bound of the pipeline (Decider.TimeBoundAt). An instance of this structure is the theorem; its inhabitation is planning/succinct-cook-levin.md. The validity hypotheses Valid are the paper's: max{Q, 2⌈log n⌉} ≤ T, |𝒟| ≤ σ, |x|, |y| ≤ Q.

Succinctly described 3SAT formulas

def MIPRE.SAT.clauseInput (m : ℕ) (c : Clause3 (Fin (2 ^ m))) : List Bool

The input bits presenting a clause to a describer on 3m + 3 inputs: the three m-bit indices, then the three signs.

Equations

• MIPRE.SAT.clauseInput m c = MIPRE.SAT.bitsOfNat m ↑c.l₁.var ++ MIPRE.SAT.bitsOfNat m ↑c.l₂.var ++ MIPRE.SAT.bitsOfNat m ↑c.l₃.var ++ [c.l₁.pos, c.l₂.pos, c.l₃.pos]

@[simp]

theorem MIPRE.SAT.length_clauseInput (m : ℕ) (c : Clause3 (Fin (2 ^ m))) : (clauseInput m c).length = 3 * m + 3

def MIPRE.SAT.Circuit.formula3 (C : Circuit) (m : ℕ) : Cnf3 (Fin (2 ^ m))

The 3SAT formula on 2^m variables that C succinctly describes: the clauses C accepts (def:succinct-formulas).

Equations

• C.formula3 m = {c : MIPRE.SAT.Clause3 (Fin (2 ^ m)) | C.evalBits (MIPRE.SAT.clauseInput m c) = true}

Tape encodings of answers

def MIPRE.SAT.cellBits : Option Bool → Bool × Bool

The two-bit encoding of a tape cell: 0 ↦ 00, 1 ↦ 01, blank ↦ 10 (the boundary symbol of the tableau is 11).

Equations

• MIPRE.SAT.cellBits (some false) = (false, false)
• MIPRE.SAT.cellBits (some true) = (false, true)
• MIPRE.SAT.cellBits none = (true, false)

def MIPRE.SAT.tapeBits (s : Cost.BitStr) (p : ℕ) : Bool

The bits of a tape holding s followed by blanks: position p is bit p % 2 of cell p / 2.

Equations

• MIPRE.SAT.tapeBits s p = if p % 2 = 0 then (MIPRE.SAT.cellBits s[p / 2]?).1 else (MIPRE.SAT.cellBits s[p / 2]?).2

Deciders accepting within a cost

def MIPRE.Decider.AcceptsWithin (D : Decider) (n : ℕ) (x y a b : Cost.BitStr) (T : ℕ) : Prop

𝒟 accepts (n, x, y, a, b) within cost T.

Equations

• D.AcceptsWithin n x y a b T = ∃ t ≤ T, D.prog.Runs (MIPRE.Cost.encode (n, x, y, a, b)) (MIPRE.Cost.encode true) t

theorem MIPRE.Decider.AcceptsWithin.accepts {D : Decider} {n : ℕ} {x y a b : Cost.BitStr} {T : ℕ} (h : D.AcceptsWithin n x y a b T) : D.Accepts n x y a b

The theorem

@[reducible, inline]

abbrev MIPRE.SAT.DescInput : Type

The input of the describer: ((𝒟, n, T, Q, σ), x, y).

Equations

• MIPRE.SAT.DescInput = ((MIPRE.Cost.Prog × ℕ × ℕ × ℕ × ℕ) × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

structure MIPRE.SAT.Valid (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : Prop

The validity hypotheses of the paper's proposition: max{Q, 2⌈log n⌉} ≤ T, |𝒟| ≤ σ and |x|, |y| ≤ Q.

• q_le : Q ≤ T
• logn_le : 2 * n.size ≤ T
• size_le : Cost.esize D ≤ σ
• x_le : List.length x ≤ Q
• y_le : List.length y ≤ Q

def MIPRE.SAT.ExtendsAnswers {m T : ℕ} (h : 4 * T ≤ 2 ^ m) (φ : Cnf3 (Fin (2 ^ m))) (a b : Fin (2 * T) → Bool) : Prop

A satisfying assignment of a formula on 2^m ≥ 4T variables extending the answer blocks a, b ∈ {0,1}^{2T} on the first 4T variables.

Equations

• MIPRE.SAT.ExtendsAnswers h φ a b = ∃ (w : Fin (2 ^ m) → Bool), (∀ (j : Fin (2 * T)), w ⟨↑j, ⋯⟩ = a j) ∧ (∀ (j : Fin (2 * T)), w ⟨2 * T + ↑j, ⋯⟩ = b j) ∧ φ.Sat w

def MIPRE.SAT.EncodesAccepted (D : Decider) (n : ℕ) (x y : Cost.BitStr) (T : ℕ) (a b : Fin (2 * T) → Bool) : Prop

a is the tape encoding of a string of length at most T on which, together with the string encoded by b, the decider accepts within cost T: the right-hand side of item 1.

Equations

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

structure MIPRE.SAT.SuccinctCookLevin : Type

Explicit succinct Cook–Levin (blueprint thm:succinct-sat; prop:standard-succinct-sat). An instance of this structure is the theorem.

• m : ℕ → ℕ → ℕ

  The variable-count exponent m(T, σ).

• s : ℕ → ℕ → ℕ → ℕ → ℕ

  The gate bound s(n, T, Q, σ).

• describe : Cost.PolyTimeFun DescInput Circuit

  The algorithm: the describer circuit from ((𝒟, n, T, Q, σ), x, y), in polynomial time (item 4).

• mProg : Cost.PolyTimeFun (ℕ × ℕ) ℕ

  Item 5: m in polynomial time from (T, σ).

• mProg_eq (T σ : ℕ) : self.mProg.toFun (T, σ) = self.m T σ
• sProg : Cost.PolyTimeFun (ℕ × ℕ × ℕ × ℕ) ℕ

  Item 5: s in polynomial time from (n, T, Q, σ).

• sProg_eq (n T Q σ : ℕ) : self.sProg.toFun (n, T, Q, σ) = self.s n T Q σ
• m_le : ∃ (c : ℕ), ∀ (T σ : ℕ), self.m T σ ≤ c * (T.size + σ.size + 1)

  Item 2: m = O(log T + log σ).

• four_mul_le (T σ : ℕ) : 4 * T ≤ 2 ^ self.m T σ

  Item 2: 2^m ≥ 4T.

• s_le : ∃ (P : Polynomial ℕ), ∀ (n T Q σ : ℕ), self.s n T Q σ ≤ Polynomial.eval (n.size + T.size + Q + σ) P

  Item 3: s = poly(log n, log T, Q, σ).

• inputs_eq (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : (self.describe.toFun ((D, n, T, Q, σ), x, y)).inputs = 3 * self.m T σ + 3

  The describer has 3m + 3 inputs.

• wellFormed (inp : DescInput) : (self.describe.toFun inp).WellFormed

  The describer is a well-formed circuit (fan-out at most two, terminal output).

• size_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D n T Q σ x y → (self.describe.toFun ((D, n, T, Q, σ), x, y)).size ≤ self.s n T Q σ

  Item 3: at most s gates on valid inputs.

• accepts_iff (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) : Valid D.prog n T Q σ x y → ∀ (a b : Fin (2 * T) → Bool), ExtendsAnswers ⋯ ((self.describe.toFun ((D.prog, n, T, Q, σ), x, y)).formula3 (self.m T σ)) a b ↔ EncodesAccepted D n x y T a b

  Item 1: the described formula has a satisfying assignment extending a, b on its first 4T variables iff a, b encode strings of length at most T that 𝒟 accepts within cost T.