Ladner's theorem

If P ≠ NP, some problem in NP is neither in P nor NP-complete Arora and Barak, Theorem 3.3. The problem is Ladner's language Cslib.Complexity.Ladner.SATH: satisfiable formulas φ whose encoding has length m, padded with m ^ H m ones, where the exponent H m is the least index below log₂ (log₂ m) of a machine agreeing with the language on the words with indices below m (Complexity.Computability.Complexity.Classes.Ladner.Basic). It is in NP (Cslib.Complexity.Ladner.SATH_mem_NP), because H is polynomial-time (Complexity.Computability.Complexity.Classes.Ladner.PolyTime). Two holes are blown in SAT:

• If SATH is in P, a machine deciding it within a polynomial time bound has indices whose clocks exceed that bound, and from some point on H is at most such an index (Cslib.Complexity.Ladner.exists_H_le_of_mem_P). With H bounded, padding is a polynomial-time reduction from SAT to SATH, so SAT is in P (Cslib.Complexity.Ladner.SAT_mem_P_of_SATH_mem_P).
• If SATH is not in P, then H tends to infinity: if H took a value i infinitely often, the machine with index i would agree with SATH everywhere within polynomial time (Cslib.Complexity.Ladner.SATH_mem_P_of_frequently_H_eq). A polynomial-time reduction from SAT to SATH then maps every large formula either to a word outside SATH or to a padded formula strictly shorter than itself, because the padding grows faster than any polynomial. Iterating the reduction as many times as the formula is long leaves a formula of bounded length, decided by a finite table, so SAT is in P (Cslib.Complexity.Ladner.SAT_mem_P_of_reducible_of_tendsto).

An NP-complete problem in P gives P = NP for every encoding (Cslib.Complexity.NPComplete.P_eq_NP_of_mem_P), since P is closed under polynomial-time reductions (Cslib.Complexity.PolyTimeReducible.mem_P). Since SAT is NP-complete (Cslib.Complexity.CookLevin.SAT_npComplete), SAT ∈ P gives P = NP (Cslib.Complexity.Ladner.P_eq_NP_of_SAT_mem_P). The unconditional forms are Cslib.Complexity.Ladner.P_eq_NP_of_SATH_mem_P and Cslib.Complexity.Ladner.P_eq_NP_of_NPComplete_SATH; the theorem keeps P ≠ NP as an explicit hypothesis (Cslib.Complexity.Ladner.exists_NP_not_P_not_NPComplete).

Main definitions

• Cslib.Complexity.Ladner.padBounded: the padding reduction from SAT to SATH along a bounded exponent.
• Cslib.Complexity.Ladner.shrink, Cslib.Complexity.Ladner.selfReduce: the self-reduction of SAT along a reduction to SATH.
• Cslib.Complexity.Ladner.smallSAT: the finite table of the short satisfiable formulas.

Main results

• Cslib.Complexity.Ladner.P_eq_NP_of_SAT_mem_P: if SAT ∈ P, then P = NP for every encoding.
• Cslib.Complexity.Ladner.exists_H_le_of_mem_P: if SATH ∈ P, H is bounded.
• Cslib.Complexity.Ladner.reducible_of_H_le: if H is bounded, SAT reduces to SATH.
• Cslib.Complexity.Ladner.SATH_mem_P_of_frequently_H_eq, Cslib.Complexity.Ladner.tendsto_H_of_notMem_P: if H takes a value infinitely often, SATH ∈ P; so if SATH ∉ P, H tends to infinity.
• Cslib.Complexity.Ladner.SAT_mem_P_of_reducible_of_tendsto: if SAT reduces to SATH and H tends to infinity, then SAT ∈ P.
• Unconditionally, SATH is in NP (Cslib.Complexity.Ladner.SATH_mem_NP), in P only if SAT is (Cslib.Complexity.Ladner.SAT_mem_P_of_SATH_mem_P), NP-hard only if SAT ∈ P (Cslib.Complexity.Ladner.SAT_mem_P_of_NPHard_SATH), and in P or NP-complete only if P = NP (Cslib.Complexity.Ladner.P_eq_NP_of_SATH_mem_P, Cslib.Complexity.Ladner.P_eq_NP_of_NPComplete_SATH).
• Cslib.Complexity.Ladner.exists_NP_not_P_not_NPComplete: Ladner's theorem, under the hypothesis P ≠ NP.

References

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

theorem Cslib.Complexity.Ladner.P_eq_NP_of_SAT_mem_P (h : SAT ∈ P encCNF) {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

If SAT is in P, then P = NP for every encoding of instances.

theorem Cslib.Complexity.Ladner.SAT_notMem_P {α : Type} {enc : α ↪ List Bool} (h : P enc ≠ NP enc) : SAT ∉ P encCNF

P ≠ NP, for any encoding, puts SAT outside P.

A machine deciding Ladner's language bounds the exponent

theorem Cslib.Complexity.Ladner.universal_desc_of_halted {k : ℕ} {State : Type} [Fintype State] (eS : State ↪ ℕ) (tm : Turing.MultiTapeTM k Bool State) {f : List Bool → Bool} {t : List Bool → ℕ} (h : ∀ (x : List Bool), (Turing.MultiTapeTM.runFrom (tm.initCfg x) (t x)).Halted ∧ (Turing.MultiTapeTM.runFrom (tm.initCfg x) (t x)).output = [f x]) {x : List Bool} {T : ℕ} (hT : t x ≤ T) : Turing.MultiTapeTM.Universal.universal (Turing.MultiTapeTM.Universal.desc eS Turing.MultiTapeTM.Universal.eBit tm, List.map (⇑Turing.MultiTapeTM.Universal.eBit) x, T) = ([Turing.MultiTapeTM.Universal.eBit (f x)], true)

A finite binary machine halting within time t x with output [f x], simulated by the universal function on its description for at least t x steps, halts with output [eBit (f x)].

theorem Cslib.Complexity.Ladner.exists_H_le_of_mem_P (h : SATH ∈ P Turing.MultiTapeTM.encBits) : ∃ (C : ℕ), ∀ (n : ℕ), H n ≤ C

If SATH is in P, then H is bounded: some index of a machine deciding SATH has a clock exceeding its polynomial time bound, and from some point on H is at most that index.

The first hole: padding along a bounded exponent

noncomputable def Cslib.Complexity.Ladner.padBounded (C : ℕ) (φ : Logic.PL.CNF ℕ) : List Bool

The padding of φ along H, computed with powers capped at (m + 1) ^ C for the length m of the encoded formula.

theorem Cslib.Complexity.Ladner.reducible_of_H_le {C : ℕ} (hC : ∀ (n : ℕ), H n ≤ C) : PolyTimeReducible encCNF Turing.MultiTapeTM.encBits SAT SATH

If H is bounded, padding reduces SAT to SATH in polynomial time.

theorem Cslib.Complexity.Ladner.SAT_mem_P_of_SATH_mem_P (h : SATH ∈ P Turing.MultiTapeTM.encBits) : SAT ∈ P encCNF

If SATH is in P, so is SAT.

A frequent value of the exponent

theorem Cslib.Complexity.Ladner.agrees_of_frequently_H_eq {i : ℕ} (h : ∃ᶠ (n : ℕ) in Filter.atTop, H n = i) (w : List Bool) : ∃ (b : Bool), runIndexed i w (clock i w.length) = ([Turing.MultiTapeTM.Universal.eBit b], true) ∧ (b = true ↔ w ∈ SATH)

If H takes the value i infinitely often, the machine with index i agrees with SATH on every word within its clock.

theorem Cslib.Complexity.Ladner.SATH_mem_P_of_frequently_H_eq {i : ℕ} (h : ∃ᶠ (n : ℕ) in Filter.atTop, H n = i) : SATH ∈ P Turing.MultiTapeTM.encBits

If H takes a value infinitely often, SATH is in P, decided by running the machine with that index within its polynomial clock.

theorem Cslib.Complexity.Ladner.tendsto_H_of_notMem_P (h : SATH ∉ P Turing.MultiTapeTM.encBits) : Filter.Tendsto H Filter.atTop Filter.atTop

If SATH is not in P, then H tends to infinity.

The second hole: an unbounded exponent

def Cslib.Complexity.Ladner.falseCNF : Logic.PL.CNF ℕ

The unsatisfiable formula with one empty clause.

theorem Cslib.Complexity.Ladner.falseCNF_notMem_SAT : falseCNF ∉ SAT

noncomputable def Cslib.Complexity.Ladner.shrink (R : Logic.PL.CNF ℕ → List Bool) (N : ℕ) (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

One round of the self-reduction of SAT along a map R into words: a formula shorter than N is kept, and otherwise replaced by the formula padded along H in R φ, or by falseCNF if R φ is not such a padded word.

theorem Cslib.Complexity.Ladner.shrink_mem_SAT_iff {R : Logic.PL.CNF ℕ → List Bool} (hR : ∀ (φ : Logic.PL.CNF ℕ), φ ∈ SAT ↔ R φ ∈ SATH) (N : ℕ) (φ : Logic.PL.CNF ℕ) : shrink R N φ ∈ SAT ↔ φ ∈ SAT

Along a reduction from SAT to SATH, a round of the self-reduction preserves satisfiability.

noncomputable def Cslib.Complexity.Ladner.selfReduce (R : Logic.PL.CNF ℕ → List Bool) (N : ℕ) (φ : Logic.PL.CNF ℕ) : Logic.PL.CNF ℕ

The self-reduction: as many rounds as the encoded formula is long.

noncomputable def Cslib.Complexity.Ladner.smallSAT (N : ℕ) : List (List Bool)

The satisfiable formulas whose encodings are shorter than N, as their encodings.

theorem Cslib.Complexity.Ladner.mem_smallSAT {N : ℕ} {φ : Logic.PL.CNF ℕ} (h : (encCNF φ).length < N) : encCNF φ ∈ smallSAT N ↔ φ ∈ SAT

theorem Cslib.Complexity.Ladner.SAT_mem_P_of_reducible_of_tendsto (hR : PolyTimeReducible encCNF Turing.MultiTapeTM.encBits SAT SATH) (hH : Filter.Tendsto H Filter.atTop Filter.atTop) : SAT ∈ P encCNF

The second hole. If SAT reduces to SATH in polynomial time and H tends to infinity, then SAT is in P: the self-reduction leaves a formula of bounded length, decided by a finite table.

theorem Cslib.Complexity.Ladner.SAT_mem_P_of_NPHard_SATH (h : NPHard Turing.MultiTapeTM.encBits SATH) : SAT ∈ P encCNF

If SATH is NP-hard, then SAT is in P: either SATH is in P, and the first hole applies, or H tends to infinity, and the second hole applies to the reduction of SAT.

Ladner's theorem

theorem Cslib.Complexity.Ladner.P_eq_NP_of_SATH_mem_P (h : SATH ∈ P Turing.MultiTapeTM.encBits) {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

If Ladner's language is in P, then P = NP.

theorem Cslib.Complexity.Ladner.P_eq_NP_of_NPComplete_SATH (h : NPComplete Turing.MultiTapeTM.encBits SATH) {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

If Ladner's language is NP-complete, then P = NP.

theorem Cslib.Complexity.Ladner.SATH_notMem_P {α : Type} {enc : α ↪ List Bool} (h : P enc ≠ NP enc) : SATH ∉ P Turing.MultiTapeTM.encBits

If P ≠ NP, Ladner's language is not in P.

theorem Cslib.Complexity.Ladner.not_NPComplete_SATH {α : Type} {enc : α ↪ List Bool} (h : P enc ≠ NP enc) : ¬NPComplete Turing.MultiTapeTM.encBits SATH

If P ≠ NP, Ladner's language is not NP-complete.

theorem Cslib.Complexity.Ladner.exists_NP_not_P_not_NPComplete {α : Type} {enc : α ↪ List Bool} (h : P enc ≠ NP enc) : ∃ L ∈ NP Turing.MultiTapeTM.encBits, L ∉ P Turing.MultiTapeTM.encBits ∧ ¬NPComplete Turing.MultiTapeTM.encBits L

Ladner's theorem. If P ≠ NP (for some encoding of instances), some problem in NP is neither in P nor NP-complete: Ladner's language SATH Arora and Barak, Theorem 3.3.