Structural consequences of the NP-hardness of MCSP

If the Minimum Circuit Size Problem (Cslib.MCSP) is NP-hard under polynomial-time many-one reductions (Cslib.Complexity.NPHard), several structural collapses and class separations follow Murray and Williams:

1. Collapse of NEXP to EXP under EXP ⊆ P/poly (Cslib.Complexity.NEXP_subset_EXP_of_MCSP_npHard_of_EXP_subset_PPoly, Cslib.Complexity.EXP_eq_NEXP_of_MCSP_npHard_of_EXP_subset_PPoly, Murray and Williams, Section 4.1, Theorem 4.1, p. 13): Murray and Williams state Theorem 4.1 as:

   "If every sparse language in NP has a polynomial-time reduction to MCSP, then EXP ⊂ P/poly ⟹ EXP = NEXP."

   The Lean theorems here assume full NPHard MCSP.encInstance MCSP (which implies the hypothesis for every language in NP, and in particular every tally/sparse language in NP), so they formalize the full-NPHard specialization of Theorem 4.1. For any problem A ∈ NEXP, its exponentially padded version ntm.padded c lies in NP, and the NP-hardness reduction R (applied only to ntm.padded c) maps padded instances z (enc a) of length 2 ^ poly(|enc a|) to MCSP instances R (z (enc a)). Reading the (R (z (enc a))).table bit at position y defines a problem in EXP on pairs (enc a, y), hence in P/poly when EXP ⊆ P/poly. Hardwiring enc a into the P/poly circuits bounds the circuit complexity of (R (z (enc a))).function by a fixed polynomial s_bound |enc a| on arity m_bound |enc a|. Consequently, membership of R (z (enc a)) in MCSP depends only on the capped threshold min (s_bound |enc a|) (R (z (enc a))).threshold, and brute-force enumeration of all circuit certificates of that size (Cslib.MCSP.boundedMCSPSearch) takes time 2 ^ poly(|enc a|) and decides A in EXP.

2. Separation EXP ⊈ NP ∩ P/poly and EXP ≠ ZPP (Cslib.Complexity.not_EXP_subset_NP_inter_PPolyOn_of_MCSP_npHard, Cslib.Complexity.EXP_ne_NP_inter_PPolyOn_of_MCSP_npHard, Cslib.Complexity.not_EXP_subset_RP_of_MCSP_npHard, Cslib.Complexity.not_EXP_subset_ZPP_of_MCSP_npHard, Cslib.Complexity.EXP_ne_ZPP_of_MCSP_npHard, Murray and Williams, Section 1, Theorem 1.6, p. 5): Murray and Williams state Theorem 1.6 as:

   "If MCSP is NP-hard under polynomial-time reductions, then EXP ≠ NP ∩ P/poly. Consequently, EXP ≠ ZPP."

   Combining Theorem 4.1 with NEXP ⊈ NP (Cslib.Complexity.not_NEXP_subset_NP, proved in Complexity.Computability.Complexity.Classes.Hierarchy.Nondeterministic by double-exponential padding from the deterministic time hierarchy) shows that EXP ⊆ NP ∩ P/poly (equivalently EXP = NP ∩ P/poly, since NP ∩ P/poly ⊆ NP ⊆ EXP) is impossible if MCSP is NP-hard. As an immediate corollary via ZPP ⊆ RP ⊆ NP ∩ P/poly (RP_subset_NP, RP_subset_PPolyOn), NP-hardness of MCSP under arbitrary polynomial-time many-one reductions implies EXP ⊈ RP and EXP ≠ ZPP.

3. Karp–Lipton collapse from MCSP ∈ P/poly (Cslib.Complexity.NP_subset_PPolyOn_of_MCSP_npHard_of_mem_PPolyOn, Cslib.Complexity.PH_eq_SigmaP_two_of_MCSP_npHard_of_mem_PPolyOn): If MCSP is both NP-hard and in P/poly, then NP ⊆ P/poly and the polynomial hierarchy collapses to Σ₂.

Main definitions

• Cslib.MCSP.boundedMCSPSearch: brute-force circuit search up to a unary gate budget S and unary certificate-enumeration budget K.

Main results

• Cslib.MCSP.computableInPolyTime_boundedMCSPSearch, Cslib.MCSP.boundedMCSPSearch_eq_true_iff, Cslib.MCSP.boundedMCSPSearch_ofFn_eq_true_iff: polynomial-time complexity and correctness of bounded circuit search.
• Cslib.Complexity.NEXP_subset_EXP_of_MCSP_npHard_of_EXP_subset_PPoly, Cslib.Complexity.EXP_eq_NEXP_of_MCSP_npHard_of_EXP_subset_PPoly: full-NPHard specialization of Murray–Williams Theorem 4.1 (EXP ⊆ P/poly ⟹ EXP = NEXP).
• Cslib.Complexity.not_EXP_subset_NP_inter_PPolyOn_of_MCSP_npHard, Cslib.Complexity.EXP_ne_NP_inter_PPolyOn_of_MCSP_npHard: Murray–Williams Theorem 1.6 (EXP ≠ NP ∩ P/poly from NP-hardness of MCSP).
• Cslib.Complexity.not_EXP_subset_RP_of_MCSP_npHard, Cslib.Complexity.EXP_ne_RP_of_MCSP_npHard, Cslib.Complexity.not_EXP_subset_ZPP_of_MCSP_npHard, Cslib.Complexity.EXP_ne_ZPP_of_MCSP_npHard: corollaries EXP ⊈ RP and EXP ≠ ZPP from NP-hardness of MCSP.
• Cslib.Complexity.NP_subset_PPolyOn_of_MCSP_npHard_of_mem_PPolyOn, Cslib.Complexity.PH_eq_SigmaP_two_of_MCSP_npHard_of_mem_PPolyOn: if MCSP is NP-hard and in P/poly, then NP ⊆ P/poly and PH = Σ₂.

References

• C. D. Murray, R. R. Williams, On the (non) NP-hardness of computing circuit complexity

Pair decoding and lifting EXP ⊆ P/poly to pairs of bitstrings

Bounded brute-force certificate search for MCSP

def Cslib.MCSP.boundedMCSPSearch (T : List Bool) (S K : ℕ) : Bool

Check whether a truth table T (of arity m = Nat.log 2 T.length) has a circuit of size at most S by enumerating all certificates of length min (certLength m S) (Nat.log 2 K). Because the certificate length is capped at Nat.log 2 K, at most K + 1 certificates are enumerated, so the search runs in time polynomial in T.length, S, and K when S and K are given in unary.

theorem Cslib.MCSP.computableInPolyTime_boundedMCSPSearch {γ : Type} {encIn : γ ↪ List Bool} {T : γ → List Bool} {S K : γ → ℕ} (hT : Turing.MultiTapeTM.ComputableInPolyTime T encIn Turing.MultiTapeTM.encBits) (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn Turing.MultiTapeTM.encUnary) (hK : Turing.MultiTapeTM.ComputableInPolyTime K encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => boundedMCSPSearch (T a) (S a) (K a)) encIn Turing.MultiTapeTM.encBool

boundedMCSPSearch is computable in polynomial time when the truth table T is given as bits and the gate budget S and enumeration budget K are given in unary.

theorem Cslib.MCSP.boundedMCSPSearch_eq_true_iff {m S K : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) (hK : Circuits.Boolean.certLength m S ≤ Nat.log 2 K) : boundedMCSPSearch T S K = true ↔ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (tableFunction m T)) ≤ S

When T has length 2 ^ m and the enumeration budget satisfies certLength m S ≤ Nat.log 2 K, boundedMCSPSearch T S K returns true if and only if the Boolean function represented by T has circuit complexity at most S.

theorem Cslib.MCSP.boundedMCSPSearch_ofFn_eq_true_iff (x : Instance) {S K : ℕ} (hK : Circuits.Boolean.certLength x.arity S ≤ Nat.log 2 K) : boundedMCSPSearch (List.ofFn x.table) S K = true ↔ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single x.function) ≤ S

On the truth table List.ofFn x.table of an MCSP.Instance x, when certLength x.arity S ≤ Nat.log 2 K, boundedMCSPSearch decides whether x.function has circuit complexity at most S.

Murray–Williams Theorem 4.1, Theorem 1.6, and Karp–Lipton consequences

theorem Cslib.Complexity.NEXP_subset_EXP_of_MCSP_npHard_of_EXP_subset_PPoly (hHard : NPHard MCSP.encInstance MCSP) (hEXP : EXP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) {α : Type} (enc : α ↪ List Bool) : NEXP enc ⊆ EXP enc

Murray–Williams Theorem 4.1 (NEXP ⊆ EXP, full-NPHard specialization) Murray and Williams, Section 4.1, Theorem 4.1, p. 13:

"If every sparse language in NP has a polynomial-time reduction to MCSP, then EXP ⊂ P/poly ⟹ EXP = NEXP."

This theorem assumes full NPHard MCSP.encInstance MCSP (which implies the hypothesis for every language in NP, and in particular every tally/sparse language in NP; the proof applies hHard only to the unary-padded language ntm.padded c), and shows that if EXP encBits ⊆ PPolyOn encBits then NEXP enc ⊆ EXP enc for every encoding enc of instances.

theorem Cslib.Complexity.EXP_eq_NEXP_of_MCSP_npHard_of_EXP_subset_PPoly (hHard : NPHard MCSP.encInstance MCSP) (hEXP : EXP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) {α : Type} (enc : α ↪ List Bool) : EXP enc = NEXP enc

Murray–Williams Theorem 4.1 (EXP = NEXP, full-NPHard specialization) Murray and Williams, Section 4.1, Theorem 4.1, p. 13:

"If every sparse language in NP has a polynomial-time reduction to MCSP, then EXP ⊂ P/poly ⟹ EXP = NEXP."

This theorem assumes full NPHard MCSP.encInstance MCSP (the full-NPHard specialization of Theorem 4.1) and shows that if EXP encBits ⊆ PPolyOn encBits then EXP enc = NEXP enc for every encoding enc of instances.

theorem Cslib.Complexity.not_EXP_subset_NP_inter_PPolyOn_of_MCSP_npHard (hHard : NPHard MCSP.encInstance MCSP) : ¬EXP Turing.MultiTapeTM.encBits ⊆ NP Turing.MultiTapeTM.encBits ∩ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits

Murray–Williams Theorem 1.6 (EXP ⊈ NP ∩ P/poly) Murray and Williams, Section 1, Theorem 1.6, p. 5:

"If MCSP is NP-hard under polynomial-time reductions, then EXP ≠ NP ∩ P/poly. Consequently, EXP ≠ ZPP."

Since NP ∩ P/poly ⊆ NP ⊆ EXP, EXP ≠ NP ∩ P/poly is equivalent to ¬ (EXP encBits ⊆ NP encBits ∩ PPolyOn encBits).

theorem Cslib.Complexity.EXP_ne_NP_inter_PPolyOn_of_MCSP_npHard (hHard : NPHard MCSP.encInstance MCSP) : EXP Turing.MultiTapeTM.encBits ≠ NP Turing.MultiTapeTM.encBits ∩ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits

Murray–Williams Theorem 1.6 (EXP ≠ NP ∩ P/poly) Murray and Williams, Section 1, Theorem 1.6, p. 5:

"If MCSP is NP-hard under polynomial-time reductions, then EXP ≠ NP ∩ P/poly. Consequently, EXP ≠ ZPP."

theorem Cslib.Complexity.not_EXP_subset_RP_of_MCSP_npHard (hHard : NPHard MCSP.encInstance MCSP) : ¬EXP Turing.MultiTapeTM.encBits ⊆ RP Turing.MultiTapeTM.encBits

Corollary of Murray–Williams Theorem 1.6 (not_EXP_subset_NP_inter_PPolyOn_of_MCSP_npHard) Murray and Williams, Section 1, Theorem 1.6, p. 5: if MCSP is NP-hard under arbitrary polynomial-time many-one reductions, then EXP ⊈ RP, via RP ⊆ NP (RP_subset_NP) and RP ⊆ BPP ⊆ P/poly (RP_subset_PPolyOn).

theorem Cslib.Complexity.EXP_ne_RP_of_MCSP_npHard (hHard : NPHard MCSP.encInstance MCSP) : EXP Turing.MultiTapeTM.encBits ≠ RP Turing.MultiTapeTM.encBits

If MCSP is NP-hard, then EXP ≠ RP.

theorem Cslib.Complexity.not_EXP_subset_ZPP_of_MCSP_npHard (hHard : NPHard MCSP.encInstance MCSP) : ¬EXP Turing.MultiTapeTM.encBits ⊆ ZPP Turing.MultiTapeTM.encBits

Murray–Williams Theorem 1.6 (EXP ⊈ ZPP) Murray and Williams, Section 1, Theorem 1.6, p. 5: if MCSP is NP-hard, then EXP ⊈ ZPP.

theorem Cslib.Complexity.EXP_ne_ZPP_of_MCSP_npHard (hHard : NPHard MCSP.encInstance MCSP) : EXP Turing.MultiTapeTM.encBits ≠ ZPP Turing.MultiTapeTM.encBits

Murray–Williams Theorem 1.6 (EXP ≠ ZPP) Murray and Williams, Section 1, Theorem 1.6, p. 5:

"If MCSP is NP-hard under polynomial-time reductions, then EXP ≠ NP ∩ P/poly. Consequently, EXP ≠ ZPP."

theorem Cslib.Complexity.NP_subset_PPolyOn_of_MCSP_npHard_of_mem_PPolyOn (hHard : NPHard MCSP.encInstance MCSP) (hPPoly : MCSP ∈ Circuits.Boolean.PPolyOn MCSP.encInstance) {α : Type} (enc : α ↪ List Bool) : NP enc ⊆ Circuits.Boolean.PPolyOn enc

If MCSP is NP-hard and lies in P/poly, then NP enc ⊆ PPolyOn enc for every encoding enc of instances.

theorem Cslib.Complexity.PH_eq_SigmaP_two_of_MCSP_npHard_of_mem_PPolyOn (hHard : NPHard MCSP.encInstance MCSP) (hPPoly : MCSP ∈ Circuits.Boolean.PPolyOn MCSP.encInstance) {α : Type} (enc : α ↪ List Bool) : PH enc = SigmaP 2 enc

If MCSP is NP-hard and lies in P/poly, then the polynomial hierarchy collapses to its second level: PH enc = SigmaP 2 enc for every encoding enc of instances.