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.Circuits.Boolean.truthTableLanguage: the truth tables of a property, as a language.
• Cslib.MCSP.Instance, Cslib.MCSP: the instances and the yes-instances of MCSP.
• Cslib.GapMCSP: GapMCSP[s₁, s₂] as a PromiseProblem (List Bool), with sides Cslib.GapMCSP.yesSet and Cslib.GapMCSP.noSet.

Main results

• Cslib.Circuits.Boolean.ofFn_mem_truthTableLanguage: membership of an ofFn-vector in truthTableLanguage.
• 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.ofFn_mem_yesSet_iff_mem_MCSP, Cslib.GapMCSP.slice_yesSet_eq_true_iff, Cslib.GapMCSP.ofFn_mem_noSet_iff_notMem_MCSP: characterization of truth tables of length 2^n in the yes and no sets.
• Cslib.GapMCSP.disjoint_yesSet_noSet: the promise of GapMCSP[s₁, s₂] is consistent when s₁ n ≤ s₂ n for all n.

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.Circuits.Boolean.truthTableLanguage (C : (n : ℕ) → Set (BooleanFunction n)) : Language Bool

The truth tables of a property, as a language [RR97]: a word of length 2 ^ n belongs to it when it is the truth table of a function in C n. Words whose length is not a power of two do not belong to it.

theorem Cslib.Circuits.Boolean.ofFn_mem_truthTableLanguage {C : (n : ℕ) → Set (BooleanFunction n)} {n : ℕ} {T : BitString (2 ^ n)} : List.ofFn T ∈ truthTableLanguage C ↔ (MCSP.truthTable n).symm T ∈ C n

A 2 ^ n-bit string T, viewed as a list via List.ofFn, belongs to truthTableLanguage C if and only if its corresponding Boolean function lies in C n.

def Cslib.GapMCSP.yesSet (s₁ : ℕ → ℕ) : Language Bool

The yes-instances of GapMCSP[s₁, s₂] across all lengths [OliveiraPichSanthanam2019, Definition 2.4]: the truth tables of Boolean functions with circuit complexity at most s₁ n.

def Cslib.GapMCSP.noSet (s₂ : ℕ → ℕ) : Language Bool

The no-instances of GapMCSP[s₁, s₂] across all lengths [OliveiraPichSanthanam2019, Definition 2.4]: the truth tables of Boolean functions with circuit complexity greater than s₂ n.

@[simp]

theorem Cslib.GapMCSP.ofFn_mem_yesSet_iff {s₁ : ℕ → ℕ} {n : ℕ} {T : BitString (2 ^ n)} : List.ofFn T ∈ yesSet s₁ ↔ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((MCSP.truthTable n).symm T)) ≤ s₁ n

A 2 ^ n-bit string T, viewed as a list via List.ofFn, belongs to yesSet s₁ if and only if its circuit complexity is at most s₁ n.

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

A 2 ^ n-bit string T, viewed as a list via List.ofFn, belongs to yesSet s₁ if and only if ⟨n, T, s₁ n⟩ ∈ MCSP.

theorem Cslib.GapMCSP.slice_yesSet_eq_true_iff {s₁ : ℕ → ℕ} {n : ℕ} {T : BitString (2 ^ n)} : (yesSet s₁).slice (2 ^ n) T = true ↔ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((MCSP.truthTable n).symm T)) ≤ s₁ n

The 2 ^ n-bit slice of yesSet s₁ evaluates to true on T if and only if its circuit complexity is at most s₁ n.

@[simp]

theorem Cslib.GapMCSP.ofFn_mem_noSet_iff {s₂ : ℕ → ℕ} {n : ℕ} {T : BitString (2 ^ n)} : List.ofFn T ∈ noSet s₂ ↔ s₂ n < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((MCSP.truthTable n).symm T))

A 2 ^ n-bit string T, viewed as a list via List.ofFn, belongs to noSet s₂ if and only if its circuit complexity is strictly greater than s₂ n.

theorem Cslib.GapMCSP.ofFn_mem_noSet_iff_notMem_MCSP {s₂ : ℕ → ℕ} {n : ℕ} {T : BitString (2 ^ n)} : List.ofFn T ∈ noSet s₂ ↔ { arity := n, table := T, threshold := s₂ n } ∉ MCSP

A 2 ^ n-bit string T, viewed as a list via List.ofFn, belongs to noSet s₂ if and only if ⟨n, T, s₂ n⟩ ∉ MCSP.

theorem Cslib.GapMCSP.disjoint_yesSet_noSet {s₁ s₂ : ℕ → ℕ} (h : ∀ (n : ℕ), s₁ n ≤ s₂ n) : Disjoint (yesSet s₁) (noSet s₂)

When s₁ n ≤ s₂ n for all n, no truth table is both a yes-instance and a no-instance.

theorem Cslib.GapMCSP.yesSet_mono {s₁ s₁' : ℕ → ℕ} (h : ∀ (n : ℕ), s₁ n ≤ s₁' n) : yesSet s₁ ≤ yesSet s₁'

Raising the yes-threshold adds yes-instances.

theorem Cslib.GapMCSP.noSet_anti {s₂ s₂' : ℕ → ℕ} (h : ∀ (n : ℕ), s₂ n ≤ s₂' n) : noSet s₂' ≤ noSet s₂

Raising the no-threshold removes no-instances.

def Cslib.GapMCSP (s₁ s₂ : ℕ → ℕ) (h : ∀ (n : ℕ), s₁ n ≤ s₂ n) : Complexity.PromiseProblem (List Bool)

GapMCSP[s₁, s₂] [OliveiraPichSanthanam2019, Definition 2.4]: the promise problem whose yes-instances are truth tables of functions with circuits of at most s₁ n gates and whose no-instances are truth tables of functions that need more than s₂ n gates, when s₁ n ≤ s₂ n for all n. Following OPS19, the hypothesis ∀ n, s₁ n ≤ s₂ n is bundled to guarantee disjointness of the promise problem by construction.

@[simp]

theorem Cslib.GapMCSP.yes_eq {s₁ s₂ : ℕ → ℕ} (h : ∀ (n : ℕ), s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ h).yes = yesSet s₁

@[simp]

theorem Cslib.GapMCSP.no_eq {s₁ s₂ : ℕ → ℕ} (h : ∀ (n : ℕ), s₁ n ≤ s₂ n) : (GapMCSP s₁ s₂ h).no = noSet s₂