Succinct MCSP is in NP

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

• Cslib.SuccinctMCSP.enc: encodes the arity in unary (encUnary), the canonical list of input-output samples using encList (encPair encBits encBool), and the threshold in unary (encUnary). This is equivalent up to field order and list framing (t is implicit in encList) to the encoding ⟨1^n, 1^s, 1^t, (x_1, b_1), …, (x_t, b_t)⟩ of [OliveiraPichSanthanam2019, Section 4.1, proof of Theorem 1.4], and the two are computable from each other in polynomial time.
• Cslib.SuccinctMCSP.encBinary: encodes the arity in unary, the canonical list of samples, and the threshold in binary (encNat).

Any consistent sample set samples on n variables is satisfied by the sparse DNF indicator function sampleFunction samples of circuit complexity at most samples.card * (2 * n + 3) + 1 (complexity_sampleFunction_le). A certificate for SuccinctMCSP can therefore be capped at MCSP.sampleBudget n samples.card s = min s (samples.card * (2 * n + 3) + 1) gates, which is polynomial in the encoded instance length even when samples.card ≪ 2 ^ n and the threshold s is given in binary. The verifier instantiates MCSP.checkCertificateOn with the listed samples.

Main definitions

• Cslib.SuccinctMCSP.sampleFunction: indicator function of the positive samples.
• Cslib.SuccinctMCSP.enumSamples, Cslib.SuccinctMCSP.rawSamples: canonical duplicate-free enumeration of an instance's samples.
• Cslib.SuccinctMCSP.toRaw: embedding of SuccinctMCSP.Instance into raw data.
• Cslib.SuccinctMCSP.enc, Cslib.SuccinctMCSP.encBinary: unary- and binary-threshold encodings.
• Cslib.SuccinctMCSP.ofFunctionEncLength: the exact bit length of SuccinctMCSP.enc (SuccinctMCSP.Instance.ofFunction f S s).
• Cslib.SuccinctMCSP.rawVerifier, Cslib.SuccinctMCSP.verifier: the NP verifiers.

Main results

• Cslib.SuccinctMCSP.complexity_sampleFunction_le: sparse synthesis bound in the number of samples.
• Cslib.SuccinctMCSP.mem_iff_exists_circuit_le_sampleBudget: SuccinctMCSP membership with gate count capped at MCSP.sampleBudget.
• Cslib.SuccinctMCSP.rawSamples_ofFunction, Cslib.SuccinctMCSP.length_enc_ofFunction: canonical sample enumeration and encoded length of Instance.ofFunction.
• Cslib.SuccinctMCSP.mem_of_verifier_eq_true, Cslib.SuccinctMCSP.exists_verifier_append: soundness and padded completeness of SuccinctMCSP.verifier.
• Cslib.SuccinctMCSP.isVerifier, Cslib.SuccinctMCSP.isVerifier_encBinary: verifier correctness.
• Cslib.SuccinctMCSP.computableInPolyTime_rawVerifier, Cslib.SuccinctMCSP.computableInPolyTime_id_enc_encBinary, Cslib.SuccinctMCSP.computableInPolyTime_verifier, Cslib.SuccinctMCSP.computableInPolyTime_verifier_encBinary: polynomial-time certificates for the verifiers and unary-to-binary threshold re-encoding.
• Cslib.SuccinctMCSP.mem_NP, Cslib.SuccinctMCSP.mem_NP_encBinary: SuccinctMCSP ∈ NP.

References

• I. C. Oliveira, J. Pich, R. Santhanam, Hardness magnification near state-of-the-art lower bounds

Sample-set complexity bound and gate budget

def Cslib.SuccinctMCSP.sampleFunction {n : ℕ} (samples : Finset (BitString n × Bool)) : BooleanFunction n

The Boolean function on n inputs that returns true on the positive samples in samples and false elsewhere.

theorem Cslib.SuccinctMCSP.complexity_sampleFunction_le {n : ℕ} (samples : Finset (BitString n × Bool)) : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (sampleFunction samples)) ≤ samples.card * (2 * n + 3) + 1

Restricting the constant true function to the positive inputs in samples shows that sampleFunction samples has circuit complexity at most samples.card * (2 * n + 3) + 1.

theorem Cslib.SuccinctMCSP.sampleFunction_agrees {x : Instance} (hcons : ∀ (y : BitString x.arity), ¬((y, true) ∈ x.samples ∧ (y, false) ∈ x.samples)) {p : BitString x.arity × Bool} (hp : p ∈ x.samples) : sampleFunction x.samples p.1 = p.2

When x has no contradictory samples, sampleFunction x.samples agrees with every sample in x.samples.

theorem Cslib.SuccinctMCSP.mem_iff_exists_circuit_le_sampleBudget {x : Instance} : x ∈ SuccinctMCSP ↔ ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), c.size ≤ MCSP.sampleBudget x.arity x.samples.card x.threshold ∧ ∀ p ∈ x.samples, c.eval Circuits.Boolean.interpretation p.1 0 = p.2

An instance is in SuccinctMCSP if and only if it is satisfied by a circuit of size at most MCSP.sampleBudget x.arity x.samples.card x.threshold.

Canonical sample enumeration and instance encodings

def Cslib.SuccinctMCSP.enumSamples (n : ℕ) : List (BitString n × Bool)

All possible input-output pairs on n variables, enumerated in the order of BitString.enum n with output false before true.

@[simp]

theorem Cslib.SuccinctMCSP.mem_enumSamples (n : ℕ) (p : BitString n × Bool) : p ∈ enumSamples n

@[simp]

theorem Cslib.SuccinctMCSP.length_enumSamples (n : ℕ) : (enumSamples n).length = 2 ^ n * 2

theorem Cslib.SuccinctMCSP.nodup_enumSamples (n : ℕ) : (enumSamples n).Nodup

def Cslib.SuccinctMCSP.rawSamples (x : Instance) : List (List Bool × Bool)

The samples of an instance x listed canonically in the order of enumSamples x.arity, with each input bitstring converted to List Bool via List.ofFn.

theorem Cslib.SuccinctMCSP.mem_rawSamples_iff {x : Instance} {p : List Bool × Bool} : p ∈ rawSamples x ↔ ∃ (y : BitString x.arity), (y, p.2) ∈ x.samples ∧ List.ofFn y = p.1

@[simp]

theorem Cslib.SuccinctMCSP.ofFn_mem_rawSamples_iff (x : Instance) (y : BitString x.arity) (b : Bool) : (List.ofFn y, b) ∈ rawSamples x ↔ (y, b) ∈ x.samples

@[simp]

theorem Cslib.SuccinctMCSP.length_rawSamples (x : Instance) : (rawSamples x).length = x.samples.card

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

Embedding a SuccinctMCSP.Instance into raw data ((arity, rawSamples), threshold).

theorem Cslib.SuccinctMCSP.toRaw_apply (x : Instance) : toRaw x = ((x.arity, rawSamples x), x.threshold)

def Cslib.SuccinctMCSP.enc : Instance ↪ List Bool

Instances of SuccinctMCSP encoded by the arity in unary, the framed list of samples, and the threshold in unary. This is equivalent up to field order and list framing (t is implicit in encList) to ⟨1^n, 1^s, 1^t, (x_1, b_1), …, (x_t, b_t)⟩ in [OliveiraPichSanthanam2019, Section 4.1, proof of Theorem 1.4], and both encodings are computable from each other in polynomial time.

theorem Cslib.SuccinctMCSP.enc_apply (x : Instance) : enc x = (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encUnary) (toRaw x)

def Cslib.SuccinctMCSP.encBinary : Instance ↪ List Bool

Instances of SuccinctMCSP encoded by the arity in unary, the framed list of samples, and the threshold in binary.

theorem Cslib.SuccinctMCSP.encBinary_apply (x : Instance) : encBinary x = (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encNat) (toRaw x)

theorem Cslib.SuccinctMCSP.rawSamples_ofFunction {n : ℕ} (f : BooleanFunction n) (S : Finset (BitString n)) (s : ℕ) : rawSamples (Instance.ofFunction f S s) = List.map (fun (y : Fin n → Bool) => (List.ofFn y, f y)) (List.filter (fun (x : BitString n) => decide (x ∈ S)) (BitString.enum n))

For Instance.ofFunction f S s, the canonical sample enumeration rawSamples visits the inputs of S in the order of BitString.enum n, paired with their values under f.

def Cslib.SuccinctMCSP.ofFunctionEncLength (n q s : ℕ) : ℕ

The exact bit length of SuccinctMCSP.enc (SuccinctMCSP.Instance.ofFunction f S s) when S.card = q: the framed unary arity n, the twice-framed list of q samples of length n + 1, and the unary threshold s.

theorem Cslib.SuccinctMCSP.ofFunctionEncLength_mono (n s : ℕ) : Monotone fun (q : ℕ) => ofFunctionEncLength n q s

SuccinctMCSP.ofFunctionEncLength is monotone in the number of samples q.

@[simp]

theorem Cslib.SuccinctMCSP.length_enc_ofFunction {n : ℕ} (f : BooleanFunction n) (S : Finset (BitString n)) (s : ℕ) : (enc (Instance.ofFunction f S s)).length = ofFunctionEncLength n S.card s

The encoded length of Instance.ofFunction f S s under SuccinctMCSP.enc depends only on the arity n, the sample count S.card, and the threshold s.

Verifier and correctness

def Cslib.SuccinctMCSP.rawVerifier (r : ((ℕ × List (List Bool × Bool)) × ℕ) × List Bool) : Bool

The verifier on raw data (((n, samples), s), w): instantiates MCSP.checkCertificateOn on the sample list samples at gate budget MCSP.sampleBudget n samples.length s.

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

The NP verifier for SuccinctMCSP.

theorem Cslib.SuccinctMCSP.verifier_eq (x : Instance) (w : List Bool) : verifier (x, w) = MCSP.checkCertificateOn (rawSamples x) Prod.fst (fun (p : List Bool × Bool) (out : Bool) => out == p.2) x.arity (MCSP.sampleBudget x.arity x.samples.card x.threshold) w

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

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

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

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

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

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

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

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

Polynomial time

theorem Cslib.SuccinctMCSP.computableInPolyTime_rawVerifier : Turing.MultiTapeTM.ComputableInPolyTime rawVerifier (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The raw verifier for SuccinctMCSP is computable in polynomial time.

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

The SuccinctMCSP verifier is computable in polynomial time under encBinary.

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

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

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

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

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

SuccinctMCSP is in NP under SuccinctMCSP.enc (unary arity, framed sample list, and unary threshold) [OliveiraPichSanthanam2019, Section 4.1, proof of Theorem 1.4].

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

SuccinctMCSP is in NP under SuccinctMCSP.encBinary (unary arity, framed sample list, and binary threshold).