Partial MCSP (MCSP*) is in NP

We define standard string encodings for instances of the Partial Minimum Circuit Size Problem (Cslib.PartialMCSP.Instance) and prove that PartialMCSP belongs to NP under both encodings:

• Cslib.PartialMCSP.enc: encodes the $2^n$-entry truth table over Option Bool using encList (encOption encBool) followed by the threshold in unary (encUnary), matching [Hirahara2022, ECCC TR22-119, Definition 8.4, p. 30].
• Cslib.PartialMCSP.encBinary: encodes the $2^n$-entry truth table over Option Bool using encList (encOption encBool) followed by the threshold in binary (encNat), matching Cslib.MCSP.encInstance and [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2].

A certificate for PartialMCSP is a circuit with at most MCSP.budget n s gates, in the format of Cslib.Circuits.Boolean.readCertificate, since any partial truth table on n variables can be extended to a total Boolean function x.completion of complexity at most $2^n (2 n + 3) + 1$ (complexity_le_two_pow_mul_add_one). The verifier evaluates the decoded circuit on every input $y \in \{0, 1\}^n$ and checks that whenever the partial truth table specifies some b at y, the circuit outputs b.

We also prove that the embedding PartialMCSP.Instance.ofTotal : MCSP.Instance → PartialMCSP.Instance is computable in polynomial time (computableInPolyTime_ofTotal_encBinary), giving a polynomial-time many-one reduction from MCSP to PartialMCSP (polyTimeReducible_MCSP_PartialMCSP_encBinary).

Main definitions

• Cslib.PartialMCSP.toRaw: raw data of an instance as a truth table list and a threshold.
• Cslib.PartialMCSP.enc: encoding of PartialMCSP.Instance with unary threshold.
• Cslib.PartialMCSP.encBinary: encoding of PartialMCSP.Instance with binary threshold.
• Cslib.PartialMCSP.tableEntry: lookup of an input bitstring in a partial truth-table list.
• Cslib.PartialMCSP.verifier, Cslib.PartialMCSP.tableVerifier: the NP verifiers.

Main results

• Cslib.PartialMCSP.mem_of_verifier_eq_true, Cslib.PartialMCSP.exists_verifier_append: soundness and padded completeness of PartialMCSP.verifier.
• Cslib.PartialMCSP.isVerifier, Cslib.PartialMCSP.isVerifier_encBinary: verifier correctness.
• Cslib.PartialMCSP.computableInPolyTime_tableEntry: table entry lookup is polynomial-time.
• Cslib.PartialMCSP.computableInPolyTime_id_enc_encBinary: re-encoding from unary (enc) to binary (encBinary) threshold is polynomial-time.
• Cslib.PartialMCSP.computableInPolyTime_verifier, Cslib.PartialMCSP.computableInPolyTime_verifier_encBinary: plain polynomial-time certificates for the verifiers.
• Cslib.PartialMCSP.mem_NP, Cslib.PartialMCSP.mem_NP_encBinary: PartialMCSP ∈ NP.
• Cslib.PartialMCSP.computableInPolyTime_ofTotal_encBinary, Cslib.PartialMCSP.polyTimeReducible_MCSP_PartialMCSP_encBinary: polynomial-time reduction from MCSP to PartialMCSP.

References

• R. Ilango, Constant Depth Formula and Partial Function Versions of MCSP are Hard
• S. Hirahara, NP-Hardness of Learning Programs and Partial MCSP

def Cslib.PartialMCSP.toRaw : Instance ↪ List (Option Bool) × ℕ

The raw data of a partial MCSP instance as a truth table list and a threshold.

theorem Cslib.PartialMCSP.toRaw_apply (x : Instance) : toRaw x = (List.ofFn x.table, x.threshold)

def Cslib.PartialMCSP.enc : Instance ↪ List Bool

Instances of PartialMCSP encoded by the framed list of Option Bool truth-table entries followed by the threshold in unary [Hirahara2022, ECCC TR22-119, Definition 8.4, p. 30].

theorem Cslib.PartialMCSP.enc_apply (x : Instance) : enc x = (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encUnary) (List.ofFn x.table, x.threshold)

def Cslib.PartialMCSP.encBinary : Instance ↪ List Bool

Instances of PartialMCSP encoded by the framed list of Option Bool truth-table entries followed by the threshold in binary [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2].

theorem Cslib.PartialMCSP.encBinary_apply (x : Instance) : encBinary x = (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encNat) (List.ofFn x.table, x.threshold)

def Cslib.PartialMCSP.tableEntry (table : List (Option Bool)) (y : List Bool) : Option Bool

The entry of a partial truth-table list at the input with bits y (none if out of bounds).

theorem Cslib.PartialMCSP.tableEntry_ofFn (x : Instance) (y : BitString x.arity) : tableEntry (List.ofFn x.table) (List.ofFn y) = x.partialFunction y

The verifier reads the partial function of an instance from its truth table.

def Cslib.PartialMCSP.verifier (p : Instance × List Bool) : Bool

The verifier for PartialMCSP: the certificate must describe a circuit on n inputs with at most MCSP.budget n s gates (readCertificate) whose output agrees with the partial truth table on all defined entries among the 2 ^ n inputs.

Correctness

theorem Cslib.PartialMCSP.mem_of_verifier_eq_true {x : Instance} {w : List Bool} (hw : verifier (x, w) = true) : x ∈ PartialMCSP

Soundness of the verifier. An instance with an accepted certificate, of any length, is in PartialMCSP.

theorem Cslib.PartialMCSP.exists_verifier_append {x : Instance} (hx : x ∈ PartialMCSP) : ∃ (u : List Bool), u.length = Circuits.Boolean.certLength x.arity (MCSP.budget x.arity x.threshold) ∧ ∀ (extra : List Bool), verifier (x, u ++ extra) = true

Completeness of the verifier. Every instance in PartialMCSP has a certificate of length certLength x.arity (MCSP.budget x.arity x.threshold) that is accepted whatever bits follow it.

theorem Cslib.PartialMCSP.isVerifier : Complexity.IsVerifier enc MCSP.certPolynomial verifier PartialMCSP

PartialMCSP.verifier verifies PartialMCSP under enc (unary threshold).

theorem Cslib.PartialMCSP.isVerifier_encBinary : Complexity.IsVerifier encBinary MCSP.certPolynomial verifier PartialMCSP

PartialMCSP.verifier verifies PartialMCSP under encBinary (binary threshold).

Polynomial time

def Cslib.PartialMCSP.tableVerifier (r : (List (Option Bool) × ℕ) × List Bool) : Bool

The verifier on a raw partial truth-table list, a threshold, and a certificate, with the number of inputs read from the length of the table.

theorem Cslib.PartialMCSP.verifier_eq_tableVerifier (p : Instance × List Bool) : verifier p = tableVerifier ((List.ofFn p.1.table, p.1.threshold), p.2)

theorem Cslib.PartialMCSP.computableInPolyTime_tableEntry : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (Option Bool) × List Bool) => tableEntry p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)

Looking up an entry in a partial truth table is computable in polynomial time.

theorem Cslib.PartialMCSP.computableInPolyTime_tableVerifier : Turing.MultiTapeTM.ComputableInPolyTime tableVerifier (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifier on raw data is computable in polynomial time.

theorem Cslib.PartialMCSP.computableInPolyTime_verifier_encBinary : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encBinary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The PartialMCSP verifier is computable in polynomial time under encBinary.

theorem Cslib.PartialMCSP.computableInPolyTime_id_enc_encBinary : Turing.MultiTapeTM.ComputableInPolyTime id enc encBinary

Re-encoding a PartialMCSP.Instance from unary threshold encoding (enc) to binary threshold encoding (encBinary) is computable in polynomial time.

theorem Cslib.PartialMCSP.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The PartialMCSP verifier is computable in polynomial time under enc (unary threshold).

theorem Cslib.PartialMCSP.mem_NP : PartialMCSP ∈ Complexity.NP enc

PartialMCSP is in NP under PartialMCSP.enc (framed Option Bool truth table and unary threshold) [Hirahara2022, ECCC TR22-119, Definition 8.4, p. 30].

theorem Cslib.PartialMCSP.mem_NP_encBinary : PartialMCSP ∈ Complexity.NP encBinary

PartialMCSP is in NP under PartialMCSP.encBinary (framed Option Bool truth table and binary threshold) [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2].

Polynomial-time reduction from MCSP to PartialMCSP

theorem Cslib.PartialMCSP.computableInPolyTime_ofTotal_encBinary : Turing.MultiTapeTM.ComputableInPolyTime Instance.ofTotal MCSP.encInstance encBinary

Embedding a total MCSP.Instance as a PartialMCSP.Instance with no * entries is computable in polynomial time.

theorem Cslib.PartialMCSP.polyTimeReducible_MCSP_PartialMCSP_encBinary : Complexity.PolyTimeReducible MCSP.encInstance encBinary MCSP PartialMCSP

MCSP reduces to PartialMCSP in polynomial time via Instance.ofTotal.