Ladner's language in polynomial time and in NP

The exponent function Cslib.Complexity.Ladner.H of Ladner's language is computable in polynomial time on unary numbers (Cslib.Complexity.Ladner.computableInPolyTime_H), and Ladner's language is in NP (Cslib.Complexity.Ladner.SATH_mem_NP), with a verifier that reads the padded formula and evaluates it under the assignment the certificate describes.

The table of the values H m, m < n, is built by iterating one step n times. The step (Cslib.Complexity.Ladner.hstepB, equal to Cslib.Complexity.Ladner.Hstep) searches the first log₂ (log₂ n) machine indices; for each, it runs the machine on each of the n words with indices below n with the universal function, for at most n steps, and compares the answer with membership in the padded language along the table. A word with index below n has length at most log₂ n, so membership is decided by decoding the padded formula and trying the n words with indices below n as certificates (Cslib.Complexity.Ladner.bruteSAT_iff). Every intermediate value is polynomial in n, and the polynomial-time calculus certifies the composite.

The certificate rests on general tools: a total decoder for formulas (Cslib.Complexity.cnfDecoder, built from Turing.MultiTapeTM.Decoder.nat and Turing.MultiTapeTM.Decoder.bool), capped powers on unary numbers (Cslib.Complexity.Ladner.computableInPolyTime_capPow), the universal function with its number of steps in unary (Turing.MultiTapeTM.Universal.computableInPolyTime_universal), and the words by index (Cslib.Complexity.Ladner.computableInPolyTime_word). Decoding machine descriptions and coding their input bits use the shared polynomial-time rules in Complexity.Computability.Machines.Turing.MultiTape.Universal.PolyTime.

Main definitions

• Cslib.Complexity.Ladner.capPow: powers capped at a bound.
• Cslib.Complexity.Ladner.padCheckAt, Cslib.Complexity.Ladner.padCheck: the formula padded in a word, if any.
• Cslib.Complexity.Ladner.bruteSAT: satisfiability by trying the words with small indices.
• Cslib.Complexity.Ladner.hstepB: the step of the exponent function as a search.
• Cslib.Complexity.Ladner.verifier: the verifier of Ladner's language.

Main results

• Cslib.Complexity.Ladner.computableInPolyTime_capPow: capped powers in unary.
• Cslib.Complexity.Ladner.mem_padSAT_iff: membership in a padded language through padCheck.
• Cslib.Complexity.Ladner.computableInPolyTime_padCheck: padCheck is polynomial-time for a polynomial-time exponent function.
• Cslib.Complexity.Ladner.hstepB_eq: the search computes the step.
• Cslib.Complexity.Ladner.computableInPolyTime_H: H is polynomial-time.
• Cslib.Complexity.Ladner.SATH_mem_NP: Ladner's language is in NP.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Decoding formulas

def Cslib.Complexity.Ladner.decodeCNF (w : List Bool) : Logic.PL.CNF ℕ

The formula decoded from a word.

@[simp]

theorem Cslib.Complexity.Ladner.decodeCNF_encCNF (φ : Logic.PL.CNF ℕ) : decodeCNF (encCNF φ) = φ

theorem Cslib.Complexity.Ladner.computableInPolyTime_decodeCNF : Turing.MultiTapeTM.ComputableInPolyTime decodeCNF Turing.MultiTapeTM.encBits encCNF

Capped powers

def Cslib.Complexity.Ladner.capPow (b e c : ℕ) : ℕ

The power b ^ e, capped at c.

theorem Cslib.Complexity.Ladner.computableInPolyTime_capPow {α : Type} {input : α ↪ List Bool} {base exp cap : α → ℕ} (hbase : Turing.MultiTapeTM.ComputableInPolyTime base input Turing.MultiTapeTM.encUnary) (hexp : Turing.MultiTapeTM.ComputableInPolyTime exp input Turing.MultiTapeTM.encUnary) (hcap : Turing.MultiTapeTM.ComputableInPolyTime cap input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => capPow (base x) (exp x) (cap x)) input Turing.MultiTapeTM.encUnary

Words by index

theorem Cslib.Complexity.Ladner.computableInPolyTime_word : Turing.MultiTapeTM.ComputableInPolyTime word Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits

The word with a given index is polynomial-time in the index in unary.

Reading a padded formula

def Cslib.Complexity.Ladner.padCheckAt (y : List Bool) (h : ℕ) : Option (Logic.PL.CNF ℕ)

The formula φ such that y is encCNF φ padded with (encCNF φ).length ^ h ones, if there is one.

theorem Cslib.Complexity.Ladner.padCheckAt_eq_some_iff {y : List Bool} {h : ℕ} {φ : Logic.PL.CNF ℕ} : padCheckAt y h = some φ ↔ y = pad (encCNF φ) ((encCNF φ).length ^ h)

def Cslib.Complexity.Ladner.padCheck (e : ℕ → ℕ) (y : List Bool) : Option (Logic.PL.CNF ℕ)

The formula padded in y along the exponent function e, if any.

theorem Cslib.Complexity.Ladner.padCheck_eq_some_iff {e : ℕ → ℕ} {y : List Bool} {φ : Logic.PL.CNF ℕ} : padCheck e y = some φ ↔ y = pad (encCNF φ) ((encCNF φ).length ^ e (encCNF φ).length)

theorem Cslib.Complexity.Ladner.mem_padSAT_iff {e : ℕ → ℕ} {y : List Bool} : y ∈ padSAT e ↔ ∃ (φ : Logic.PL.CNF ℕ), padCheck e y = some φ ∧ φ ∈ SAT

Membership in a padded language through padCheck.

theorem Cslib.Complexity.Ladner.computableInPolyTime_unpad : Turing.MultiTapeTM.ComputableInPolyTime unpad Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encUnary)

Splitting a padded word is polynomial-time.

theorem Cslib.Complexity.Ladner.computableInPolyTime_padCheck {α : Type} {input : α ↪ List Bool} {e : α → ℕ → ℕ} {y : α → List Bool} (he : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : α × ℕ) => e p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) (hy : Turing.MultiTapeTM.ComputableInPolyTime y input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => padCheck (e x) (y x)) input (Turing.MultiTapeTM.encOption encCNF)

Reading the formula padded along a computed exponent function is polynomial-time. The exponent function may capture the input.

Satisfiability of short formulas

def Cslib.Complexity.Ladner.bruteSAT (n : ℕ) (φ : Logic.PL.CNF ℕ) : Bool

Whether one of the words with indices below n is a satisfying certificate for φ.

theorem Cslib.Complexity.Ladner.bruteSAT_iff {n : ℕ} {φ : Logic.PL.CNF ℕ} (h : 2 ^ ((encCNF φ).length + 1) ≤ n + 1) : bruteSAT n φ = true ↔ φ ∈ SAT

Short formulas are decided by trying the words with small indices: every certificate of the length of the encoded formula has a smaller index than n.

theorem Cslib.Complexity.Ladner.computableInPolyTime_bruteSAT {α : Type} {input : α ↪ List Bool} {n : α → ℕ} {φ : α → Logic.PL.CNF ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n input Turing.MultiTapeTM.encUnary) (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input encCNF) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => bruteSAT (n x) (φ x)) input Turing.MultiTapeTM.encBool

The step of the exponent function

def Cslib.Complexity.Ladner.memB (T : List ℕ) (y : List Bool) : Bool

Membership in the padded language along the table T, decided by bruteSAT with the words with indices below the length of T.

theorem Cslib.Complexity.Ladner.memB_word_iff {T : List ℕ} {j : ℕ} (hj : j < T.length) : memB T (word j) = true ↔ word j ∈ padSAT fun (m : ℕ) => T.getD m 0

def Cslib.Complexity.Ladner.agreesB (T : List ℕ) (i j : ℕ) : Bool

The test of Cslib.Complexity.Ladner.Agrees along the table T, as a Boolean.

theorem Cslib.Complexity.Ladner.agreesB_iff {T : List ℕ} {i j : ℕ} (hj : j < T.length) : agreesB T i j = true ↔ Agrees (fun (m : ℕ) => T.getD m 0) T.length i j

def Cslib.Complexity.Ladner.hstepB (T : List ℕ) : ℕ

The step of the exponent function as a search over machine indices and words.

theorem Cslib.Complexity.Ladner.hstepB_eq (T : List ℕ) : hstepB T = Hstep T

The search computes the step.

theorem Cslib.Complexity.Ladner.computableInPolyTime_runIndexed {α : Type} {input : α ↪ List Bool} {i : α → ℕ} {w : α → List Bool} {t : α → ℕ} (hi : Turing.MultiTapeTM.ComputableInPolyTime i input Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w input Turing.MultiTapeTM.encBits) (ht : Turing.MultiTapeTM.ComputableInPolyTime t input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => runIndexed (i x) (w x) (t x)) input Turing.MultiTapeTM.Universal.eOut

The run of an indexed machine, with the number of steps in unary, is polynomial-time.

The exponent function

theorem Cslib.Complexity.Ladner.Htable_eq_iterate (n : ℕ) : Htable n = (fun (T : List ℕ) => T ++ [hstepB T])^[n] []

theorem Cslib.Complexity.Ladner.computableInPolyTime_Htable : Turing.MultiTapeTM.ComputableInPolyTime Htable Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)

The tables of H are polynomial-time in their length, in unary.

theorem Cslib.Complexity.Ladner.computableInPolyTime_H : Turing.MultiTapeTM.ComputableInPolyTime H Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

H is polynomial-time on unary numbers.

Ladner's language is in NP

noncomputable def Cslib.Complexity.Ladner.verifier (x : List Bool × List Bool) : Bool

The verifier of Ladner's language: read the padded formula and evaluate it under the assignment the certificate describes.

theorem Cslib.Complexity.Ladner.assignment_append_replicate (φ : Logic.PL.CNF ℕ) (w : List Bool) (k : ℕ) : SAT.assignment φ (w ++ List.replicate k false) = SAT.assignment φ w

Padding a certificate with false does not change the assignment it describes.

theorem Cslib.Complexity.Ladner.isVerifier : IsVerifier Turing.MultiTapeTM.encBits Polynomial.X verifier SATH

Cslib.Complexity.Ladner.verifier verifies Ladner's language with certificates as long as the word.

theorem Cslib.Complexity.Ladner.SATH_mem_NP : SATH ∈ NP Turing.MultiTapeTM.encBits

Ladner's language is in NP, with the verifier evaluating the padded formula.