Succinct MCSP

Succinct MCSP asks, given samples (x₁, b₁), …, (x_t, b_t) of a Boolean function on n inputs and a threshold s, whether some circuit with at most s gates takes the value bᵢ at xᵢ for every i [OliveiraPichSanthanam2019, proof of Theorem 1.4]. Its instances list samples instead of a whole truth table, so they may be much shorter than the 2 ^ n bits of an instance of MCSP. Contradictory samples are allowed; they make a no-instance.

When the samples are the values of f on a set S of inputs (Instance.ofFunction), the question is whether f has complexity at most s on S, cslib's complexityOn interpretation S (single f) (ofFunction_mem_iff). Taking every input as a sample gives MCSP (ofFunction_univ_mem_iff). Sholomov's bound for partial functions gives a Shannon window here too: on 2 p inputs, every instance of at most 2 ^ p consistent samples is a yes-instance at every threshold of at least (1 + ε) 2 ^ p / p, for large p (eventually_ofFunction_mem).

Main definitions

• Cslib.SuccinctMCSP.Instance, Cslib.SuccinctMCSP: the instances and yes-instances.

Main results

• Cslib.SuccinctMCSP.ofFunction_mem_iff: samples of a function, as complexity on a support.
• Cslib.SuccinctMCSP.ofFunction_univ_mem_iff: all samples of a function, as MCSP.
• Cslib.SuccinctMCSP.eventually_ofFunction_mem: few samples always have small circuits.

References

• I. C. Oliveira, J. Pich, R. Santhanam, Hardness magnification near state-of-the-art lower bounds
• L. A. Sholomov, On the realization of incompletely defined Boolean functions by circuits of functional elements

structure Cslib.SuccinctMCSP.Instance : Type

An instance of Succinct MCSP: samples of a Boolean function on arity inputs, each an input and the value required there, and a size threshold.

• arity : ℕ

  The number of inputs of the function.

• samples : Finset (BitString self.arity × Bool)

  The samples: an input and the required value at it.

• threshold : ℕ

  The number of gates allowed.

def Cslib.SuccinctMCSP.Instance.ofFunction {n : ℕ} (f : BooleanFunction n) (S : Finset (BitString n)) (s : ℕ) : Instance

The instance whose samples are the values of f on the inputs in S, with threshold s.

def Cslib.SuccinctMCSP : Set SuccinctMCSP.Instance

Succinct MCSP [OPS19]: the instances some De Morgan circuit with at most threshold gates satisfies, taking the value b at x for every sample (x, b).

theorem Cslib.SuccinctMCSP.mem_iff_exists_mem_computableFunctions {x : Instance} : x ∈ SuccinctMCSP ↔ ∃ g ∈ Circuits.Boolean.computableFunctions x.arity x.threshold, ∀ p ∈ x.samples, g p.1 = p.2

The yes-instances are those satisfied by some function computable within the threshold.

theorem Cslib.SuccinctMCSP.ofFunction_mem_iff {n s : ℕ} {f : BooleanFunction n} {S : Finset (BitString n)} : Instance.ofFunction f S s ∈ SuccinctMCSP ↔ Circuits.complexityOn Circuits.Boolean.interpretation (↑S) (Circuits.single f) ≤ s

Samples of f on S are a yes-instance exactly when f has complexity at most s on S.

theorem Cslib.SuccinctMCSP.ofFunction_univ_mem_iff {n s : ℕ} {f : BooleanFunction n} : Instance.ofFunction f Finset.univ s ∈ SuccinctMCSP ↔ { arity := n, table := (MCSP.truthTable n) f, threshold := s } ∈ MCSP

With every input as a sample, Succinct MCSP is MCSP.

theorem Cslib.SuccinctMCSP.mk_mem_of_le {n s : ℕ} {samples : Finset (BitString n × Bool)} {t : ℕ} (h : { arity := n, samples := samples, threshold := s } ∈ SuccinctMCSP) (hst : s ≤ t) : { arity := n, samples := samples, threshold := t } ∈ SuccinctMCSP

Raising the threshold keeps a yes-instance a yes-instance.

theorem Cslib.SuccinctMCSP.mk_mem_of_subset {n s : ℕ} {samples samples' : Finset (BitString n × Bool)} (h : { arity := n, samples := samples, threshold := s } ∈ SuccinctMCSP) (hsub : samples' ⊆ samples) : { arity := n, samples := samples', threshold := s } ∈ SuccinctMCSP

Dropping samples keeps a yes-instance a yes-instance.

theorem Cslib.SuccinctMCSP.not_mem_of_mem_samples {x : Instance} {y : BitString x.arity} (htrue : (y, true) ∈ x.samples) (hfalse : (y, false) ∈ x.samples) : x ∉ SuccinctMCSP

Contradictory samples make a no-instance.

theorem Cslib.SuccinctMCSP.eventually_ofFunction_mem (ε : ℝ) (hε : 0 < ε) : ∃ (p₀ : ℕ), ∀ p ≥ p₀, ∀ (f : BooleanFunction (2 * p)) (S : Finset (BitString (2 * p))), S.card ≤ 2 ^ p → ∀ (s : ℕ), (1 + ε) * 2 ^ p / ↑p ≤ ↑s → Instance.ofFunction f S s ∈ SuccinctMCSP

Few samples have small circuits [Sho69]. For every ε > 0 and all large p, every instance of at most 2 ^ p samples of a function on 2 p inputs is a yes-instance at every threshold of at least (1 + ε) 2 ^ p / p.