Documentation

Complexity.Computability.Complexity.Classes.PH.KarpLipton

The Karp–Lipton theorem #

If SAT has circuits of polynomial size, the polynomial hierarchy collapses to its second level Karp and Lipton, Arora and Barak, Theorem 6.19. The hypothesis is that some language L ∈ P/poly contains exactly the encodings encCNF φ of the satisfiable formulas; it follows from NP ⊆ P/poly, for problems with any encoding of their instances.

The proof shows Π₂ ⊆ Σ₂ (Cslib.Complexity.PiP_two_subset_SigmaP_two_of_SAT). Let a ∈ A ↔ ∀ u, ∃ v, V (a, u ++ v). The pairs (a, u) for which some v is accepted form a problem in NP by the witness API (Cslib.Complexity.mem_NP_setOf_exists_append), which the Cook–Levin reduction f maps to SAT. A Σ₂ verifier guesses circuits for SAT on all the lengths the self-reduction (Cslib.Complexity.SAT.search) of a formula f (a, u) asks about, then checks, for every u, that the self-reduction answered by the guessed circuits finds a satisfying assignment of f (a, u). A satisfying assignment proves (a, u) in the problem whatever circuits were guessed, and correct circuits always find one when there is one. Since Π₂ ⊆ Σ₂ holds for every encoding of instances, the hierarchy collapses to Σ₂ (Cslib.Complexity.PH_eq_SigmaP_of_PiP_subset_SigmaP).

The guessed circuits are listed in an advice string (Cslib.Circuits.Boolean.familyAdvice, Cslib.Circuits.Boolean.PPoly.exists_evalAdvice): the circuits C 0, …, C N, each in the certificate format of Cslib.Circuits.Boolean.readCertificate, padded to a common length. The circuit for an input x is read from the block at position x.length and evaluated on x (Cslib.Circuits.Boolean.evalAdvice), in polynomial time.

The same advice-string mechanism eliminates alternating quantifiers nonuniformly: if M ∈ P/poly, replacing M by an advice string listing its circuits up to length 2 |x| + 1 + p |x| turns the existential quantifier over w of length p |x| in frame x ++ w ∈ M into a language in NP, and hardwiring the advice string (Cslib.Circuits.Boolean.PPoly.of_advice) shows that the existential projection remains in P/poly when NP ⊆ P/poly (Cslib.Complexity.mem_PPoly_of_exists_frame_append). Together with closure of P/poly under complement (Cslib.Circuits.Boolean.PPolyOn.compl) and P ⊆ P/poly (Cslib.Circuits.Boolean.P_subset_PPolyOn), induction on k gives Σₖ ⊆ P/poly, Πₖ ⊆ P/poly, and PH ⊆ P/poly (Cslib.Complexity.SigmaP_subset_PPolyOn_of_NP_subset_PPoly, Cslib.Complexity.PiP_subset_PPolyOn_of_NP_subset_PPoly, Cslib.Complexity.PH_subset_PPolyOn_of_NP_subset_PPoly) Karp and Lipton, Section 3, Arora and Barak, Section 6.4. Furthermore, P/poly preimages are closed under polynomial-time many-one reductions (Cslib.Complexity.PolyTimeReducible.mem_PPolyOn), so NP encBits ⊆ PPolyOn encBits is equivalent to SAT ∈ PPolyOn encCNF (Cslib.Complexity.NP_subset_PPolyOn_iff_SAT).

Main results #

References #

The Karp–Lipton verifier #

Π₂ ⊆ Σ₂ #

source
theorem Cslib.Complexity.PiP_two_subset_SigmaP_two_of_SAT {α : Type} (hSAT : SAT ∈ Circuits.Boolean.PPolyOn encCNF) (enc : α ↪ List Bool) :
PiP 2 enc ⊆ SigmaP 2 enc

Karp–Lipton, Π₂ ⊆ Σ₂. If some language in P/poly contains exactly the encodings of the satisfiable formulas, then Π₂ ⊆ Σ₂, for every encoding of instances.

source
theorem Cslib.Complexity.PiP_two_eq_SigmaP_two_of_SAT {α : Type} (hSAT : SAT ∈ Circuits.Boolean.PPolyOn encCNF) (enc : α ↪ List Bool) :
PiP 2 enc = SigmaP 2 enc

Karp–Lipton, Π₂ = Σ₂. If some language in P/poly contains exactly the encodings of the satisfiable formulas, then Π₂ = Σ₂, for every encoding of instances.

The collapse #

source
theorem Cslib.Complexity.PH_eq_SigmaP_two_of_SAT {α : Type} {enc : α ↪ List Bool} (hSAT : SAT ∈ Circuits.Boolean.PPolyOn encCNF) :
PH enc = SigmaP 2 enc

The Karp–Lipton theorem. If some language in P/poly contains exactly the encodings of the satisfiable formulas, then the polynomial hierarchy collapses to its second level: PH = Σ₂, for every encoding of instances.

source
theorem Cslib.Complexity.PH_eq_SigmaP_two_of_NP_subset_PPoly {α : Type} {enc : α ↪ List Bool} (h : ∀ {β : Type} (encB : β ↪ List Bool), NP encB ⊆ Circuits.Boolean.PPolyOn encB) :
PH enc = SigmaP 2 enc

The Karp–Lipton theorem, NP ⊆ P/poly ⇒ PH = Σ₂. If every problem in NP, with any encoding of its instances, is the preimage of a language in P/poly, then PH = Σ₂, for every encoding of instances.

Nonuniform quantifier elimination and PH ⊆ P/poly #

source
theorem Cslib.Complexity.PolyTimeReducible.mem_PPolyOn {α : Type} {enc : α ↪ List Bool} {β : Type} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hAB : PolyTimeReducible enc encB A B) (hB : B ∈ Circuits.Boolean.PPolyOn encB) :
A ∈ Circuits.Boolean.PPolyOn enc

Preimages of P/poly are closed under polynomial-time reductions. If A reduces to B in polynomial time and B is the preimage under encB of a language in P/poly, then A is the preimage under enc of a language in P/poly: evaluating the circuits for B up to the polynomial output-length bound of the reduction from an advice string is polynomial-time, and hardwiring the advice string (PPoly.of_advice) gives circuits of polynomial size.

source
theorem Cslib.Complexity.mem_PPoly_of_exists_frame_append (hNP : NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) {M : Language Bool} (hM : M ∈ Circuits.Boolean.PPoly) (p : Polynomial ℕ) :
{x : List Bool | ∃ (w : List Bool), w.length = Polynomial.eval x.length p ∧ Turing.MultiTapeTM.frame x ++ w ∈ M} ∈ Circuits.Boolean.PPoly

Nonuniform quantifier elimination. If every language in NP over Bool is in P/poly and M is in P/poly, then the language of words x for which frame x ++ w ∈ M for some w of length p |x| is in P/poly: replacing M by an advice string listing its circuits up to length 2 |x| + 1 + p |x| turns the existential quantifier over w into a language in NP, and hardwiring the advice string (Cslib.Circuits.Boolean.PPoly.of_advice) gives circuits of polynomial size Karp and Lipton, Section 3.

source
theorem Cslib.Complexity.PPolyOn.exists_of_computableInPolyTime_length {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) {N : α → ℕ} (hN : Turing.MultiTapeTM.ComputableInPolyTime N enc Turing.MultiTapeTM.encUnary) {P : α → List Bool → Prop} (hP : {p : α × List Bool | P p.1 p.2} ∈ Circuits.Boolean.PPolyOn (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) :
{a : α | ∃ (u : List Bool), u.length = N a ∧ P a u} ∈ Circuits.Boolean.PPolyOn enc

Nonuniform existential quantifier elimination in PPolyOn. Under NP ⊆ P/poly, if a relation P : α → List Bool → Prop is in PPolyOn (encPair enc encBits) and the witness length N : α → ℕ is computable in polynomial time in unary, then {a | ∃ u, u.length = N a ∧ P a u} is in PPolyOn enc.

source
theorem Cslib.Complexity.PPolyOn.forall_of_computableInPolyTime_length {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) {N : α → ℕ} (hN : Turing.MultiTapeTM.ComputableInPolyTime N enc Turing.MultiTapeTM.encUnary) {P : α → List Bool → Prop} (hP : {p : α × List Bool | P p.1 p.2} ∈ Circuits.Boolean.PPolyOn (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits)) :
{a : α | ∀ (u : List Bool), u.length = N a → P a u} ∈ Circuits.Boolean.PPolyOn enc

Nonuniform universal quantifier elimination in PPolyOn. Under NP ⊆ P/poly, if a relation P : α → List Bool → Prop is in PPolyOn (encPair enc encBits) and the bound N : α → ℕ is computable in polynomial time in unary, then {a | ∀ u, u.length = N a → P a u} is in PPolyOn enc.

source
theorem Cslib.Complexity.SigmaP_subset_PPolyOn_of_NP_subset_PPoly {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) (k : ℕ) :
SigmaP k enc ⊆ Circuits.Boolean.PPolyOn enc

Karp–Lipton, NP ⊆ P/poly ⇒ Σₖ ⊆ P/poly. If NP ⊆ P/poly over bitstrings, then every level Σₖ of the polynomial hierarchy, with any encoding of its instances, is in P/poly Karp and Lipton, Section 3, Arora and Barak, Section 6.4.

source
theorem Cslib.Complexity.PiP_subset_PPolyOn_of_NP_subset_PPoly {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) (k : ℕ) :
PiP k enc ⊆ Circuits.Boolean.PPolyOn enc

Karp–Lipton, NP ⊆ P/poly ⇒ Πₖ ⊆ P/poly. If NP ⊆ P/poly over bitstrings, then every level Πₖ of the polynomial hierarchy, with any encoding of its instances, is in P/poly.

source
theorem Cslib.Complexity.PH_subset_PPolyOn_of_NP_subset_PPoly {α : Type} {enc : α ↪ List Bool} (hNP : NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) :
PH enc ⊆ Circuits.Boolean.PPolyOn enc

Karp–Lipton, NP ⊆ P/poly ⇒ PH ⊆ P/poly. If NP ⊆ P/poly over bitstrings, then the entire polynomial hierarchy, with any encoding of its instances, is in P/poly Karp and Lipton, Section 3, Arora and Barak, Section 6.4.

source
theorem Cslib.Complexity.NP_subset_PPolyOn_iff_SAT :
NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits ↔ SAT ∈ Circuits.Boolean.PPolyOn encCNF

Equivalence of NP ⊆ P/poly over bitstrings and SAT ∈ P/poly. Having polynomial-size circuits for every problem in NP encBits is equivalent to SAT having circuits of polynomial size.