The Minimum Circuit Size Problem

The Minimum Circuit Size Problem (MCSP) asks, given the truth table of a Boolean function f on n inputs and a number s, whether f has a circuit with at most s gates [KC00]. Its gap version GapMCSP[s₁, s₂] is the promise problem of telling, for each n, the truth tables of functions with circuits of at most s₁ n gates from those of functions that need more than s₂ n gates [OliveiraPichSanthanam2019, Definition 2.4].

The truth table of f lists its 2 ^ n values in the order of BitString.equivFin. Circuits are De Morgan circuits, and their size counts every AND, OR, NOT and constant gate, so the measure is cslib's complexity interpretation (single f); see Cslib.Computability.Circuit.Boolean.Basic. Only the semantics of the problems is defined here. An encoding of the instances of MCSP as strings, and the proof that MCSP is in NP for it, are in Complexity.Computability.MCSP.NP.

The yes-instances of MCSP on functions of n inputs at threshold s are the truth tables of cslib's computableFunctions n s, so there are as many of them as such functions (MCSP.ncard_setOf_mem).

Main definitions

• Cslib.MCSP.truthTable: truth tables of Boolean functions.
• Cslib.MCSP.Instance, Cslib.MCSP: the instances and the yes-instances of MCSP.
• Cslib.GapMCSP.yes, Cslib.GapMCSP.no: the two sides of GapMCSP[s₁, s₂].

Main results

• Cslib.MCSP.mem_iff_exists_circuit, Cslib.MCSP.mem_iff_mem_computableFunctions: the yes- instances of MCSP, as circuits and as computable functions.
• Cslib.MCSP.ncard_setOf_mem: the number of yes-instances of a given arity and threshold.
• Cslib.GapMCSP.disjoint_yes_no: the promise of GapMCSP[s₁, s₂] is consistent when s₁ ≤ s₂, and Cslib.GapMCSP.no_eq_compl_yes: GapMCSP[s, s] is MCSP at threshold s.

References

• V. Kabanets, J.-Y. Cai, Circuit minimization problem
• I. C. Oliveira, J. Pich, R. Santhanam, Hardness magnification near state-of-the-art lower bounds

def Cslib.MCSP.truthTable (n : ℕ) : BooleanFunction n ≃ BitString (2 ^ n)

The truth table of a Boolean function on n inputs: its values on the 2 ^ n inputs, in the order of BitString.equivFin.

@[simp]

theorem Cslib.MCSP.truthTable_apply {n : ℕ} (f : BooleanFunction n) (i : Fin (2 ^ n)) : (truthTable n) f i = f ((BitString.equivFin n).symm i)

@[simp]

theorem Cslib.MCSP.truthTable_symm_apply {n : ℕ} (T : BitString (2 ^ n)) (x : BitString n) : (truthTable n).symm T x = T ((BitString.equivFin n) x)

structure Cslib.MCSP.Instance : Type

An instance of the Minimum Circuit Size Problem: the truth table of a Boolean function on arity inputs, and a size threshold.

• arity : ℕ

  The number of inputs of the function.

• table : BitString (2 ^ self.arity)

  The truth table of the function.

• threshold : ℕ

  The number of gates allowed.

def Cslib.MCSP.Instance.function (x : Instance) : BooleanFunction x.arity

The Boolean function whose truth table an instance gives.

def Cslib.MCSP : Set MCSP.Instance

The Minimum Circuit Size Problem [KC00]: the instances whose function has a De Morgan circuit with at most threshold gates.

theorem Cslib.MCSP.mem_iff {x : Instance} : x ∈ MCSP ↔ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single x.function) ≤ x.threshold

@[simp]

theorem Cslib.MCSP.mk_truthTable_mem_iff {n s : ℕ} {f : BooleanFunction n} : { arity := n, table := (truthTable n) f, threshold := s } ∈ MCSP ↔ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single f) ≤ s

The truth table of f with threshold s is a yes-instance exactly when f has complexity at most s.

theorem Cslib.MCSP.mk_truthTable_mem_iff_mem {n s : ℕ} {f : BooleanFunction n} : { arity := n, table := (truthTable n) f, threshold := s } ∈ MCSP ↔ f ∈ Circuits.Boolean.computableFunctions n s

The truth table of f with threshold s is a yes-instance exactly when f is computable with at most s gates.

theorem Cslib.MCSP.mem_iff_exists_circuit {x : Instance} : x ∈ MCSP ↔ ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), c.Computes Circuits.Boolean.interpretation (Circuits.single x.function) ∧ c.size ≤ x.threshold

An instance is a yes-instance exactly when some circuit with at most threshold gates computes its function.

theorem Cslib.MCSP.mem_iff_mem_computableFunctions {x : Instance} : x ∈ MCSP ↔ x.function ∈ Circuits.Boolean.computableFunctions x.arity x.threshold

The yes-instances are the truth tables of the functions computable within the threshold.

theorem Cslib.MCSP.mem_of_le {n s t : ℕ} {T : BitString (2 ^ n)} (h : { arity := n, table := T, threshold := s } ∈ MCSP) (hst : s ≤ t) : { arity := n, table := T, threshold := t } ∈ MCSP

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

theorem Cslib.MCSP.ncard_setOf_mem (n s : ℕ) : {T : BitString (2 ^ n) | { arity := n, table := T, threshold := s } ∈ MCSP}.ncard = (Circuits.Boolean.computableFunctions n s).card

There are as many yes-instances of arity n and threshold s as functions on n inputs computable with at most s gates.

def Cslib.GapMCSP.yes (s₁ : ℕ → ℕ) (n : ℕ) : Set (BitString (2 ^ n))

The yes-instances of GapMCSP[s₁, s₂] on functions of n inputs: the truth tables of functions with circuits of at most s₁ n gates [OliveiraPichSanthanam2019, Definition 2.4].

def Cslib.GapMCSP.no (s₂ : ℕ → ℕ) (n : ℕ) : Set (BitString (2 ^ n))

The no-instances of GapMCSP[s₁, s₂] on functions of n inputs: the truth tables of functions that need more than s₂ n gates [OliveiraPichSanthanam2019, Definition 2.4].

theorem Cslib.GapMCSP.mem_yes_iff {s₁ : ℕ → ℕ} {n : ℕ} {T : BitString (2 ^ n)} : T ∈ yes s₁ n ↔ { arity := n, table := T, threshold := s₁ n } ∈ MCSP

The yes-instances of GapMCSP[s₁, s₂] are those of MCSP at threshold s₁ n.

theorem Cslib.GapMCSP.no_eq_compl_yes (s₂ : ℕ → ℕ) (n : ℕ) : no s₂ n = (yes s₂ n)ᶜ

The no-instances of GapMCSP[s₁, s₂] are the truth tables that are not yes-instances of MCSP at threshold s₂ n.

theorem Cslib.GapMCSP.disjoint_yes_no {s₁ s₂ : ℕ → ℕ} {n : ℕ} (h : s₁ n ≤ s₂ n) : Disjoint (yes s₁ n) (no s₂ n)

The promise of GapMCSP[s₁, s₂] is consistent: when s₁ n ≤ s₂ n, no truth table is both a yes-instance and a no-instance.

theorem Cslib.GapMCSP.yes_mono {s₁ : ℕ → ℕ} {n : ℕ} {s₁' : ℕ → ℕ} (h : s₁ n ≤ s₁' n) : yes s₁ n ⊆ yes s₁' n

Raising the yes-threshold adds yes-instances.

theorem Cslib.GapMCSP.no_anti {s₂ : ℕ → ℕ} {n : ℕ} {s₂' : ℕ → ℕ} (h : s₂ n ≤ s₂' n) : no s₂' n ⊆ no s₂ n

Raising the no-threshold removes no-instances.