The Partial Minimum Circuit Size Problem (MCSP*)

The Partial Minimum Circuit Size Problem (MCSP* or PartialMCSP) asks, given the truth table of a partial Boolean function $f^* : \{0, 1\}^n \to \{0, 1, *\}$ on arity = n inputs and a size threshold s, whether there exists a total Boolean function $f : \{0, 1\}^n \to \{0, 1\}$ that extends $f^*$ (agreeing with $f^*$ on every input where $f^*(x) \ne *$) and has a circuit of size at most s [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2; Hirahara2022, ECCC TR22-119, Definition 8.4, p. 30].

In PartialMCSP.Instance, the truth table has $2^n$ entries in Option Bool, where some b requires the circuit to output b and none represents the "don't care" symbol * (also written ? in [Hirahara2022, ECCC TR22-119, Definition 8.4]).

Cslib.PartialMCSP uses the standard De Morgan all-gates size measure Circuit.size (complexityOn interpretation x.definedInputs (single x.completion)), matching Cslib.MCSP and Cslib.SuccinctMCSP. We also define Cslib.PartialMCSP.BinaryGate using the AND/OR-only gate count c.program.cost binaryCost from [Ilango2020FOCS, Section II.B and Section III.B, p. 427; ECCC TR20-183, Section 2.2] (where NOT and constant gates are free), and prove the threshold-$n-1$ bridge theorems relating the two measures using the binary-cost support bounds in Complexity.Computability.Circuit.Boolean.BinaryCost:

• Every yes-instance of PartialMCSP is a yes-instance of PartialMCSP.BinaryGate (PartialMCSP.mem_binaryGate_of_mem).
• When all n input coordinates are essential for the partial function, no circuit with fewer than n - 1 binary gates can agree with it (PartialMCSP.not_mem_binaryGate_of_threshold_lt), and at threshold n - 1 any all-gates circuit agreeing with it must have size n - 1, binary cost n - 1, and consist solely of binary AND/OR gates (PartialMCSP.isBinary_of_mem_of_threshold_le).

String encodings of PartialMCSP.Instance, membership in NP, and the polynomial-time many-one reduction from MCSP to PartialMCSP are in Complexity.Computability.MCSP.PartialNP.

Main definitions

• Cslib.PartialMCSP.Instance: an instance of partial-function MCSP (arity, table of length $2^{\text{arity}}$ over Option Bool, and threshold).
• Cslib.PartialMCSP.Instance.AgreesWith: a total Boolean function extends the partial truth table.
• Cslib.PartialMCSP: yes-instances under the all-gates De Morgan circuit size measure.
• Cslib.PartialMCSP.BinaryGate: yes-instances under Ilango's AND/OR-only gate measure (binaryCost).
• Cslib.PartialMCSP.Instance.ofTotal, Cslib.PartialMCSP.Instance.toSuccinct, Cslib.PartialMCSP.Instance.restrictTable: embeddings into PartialMCSP from MCSP, from PartialMCSP into SuccinctMCSP, and by restricting a total truth table to a subset of inputs.

Main results

• Cslib.PartialMCSP.mem_iff_exists_circuit, Cslib.PartialMCSP.mem_iff_exists_total_extension: characterizations of PartialMCSP via circuits and via total function extensions.
• Cslib.PartialMCSP.mem_binaryGate_of_mem, Cslib.PartialMCSP.not_mem_binaryGate_of_threshold_lt, Cslib.PartialMCSP.isBinary_of_mem_of_threshold_le, Cslib.PartialMCSP.mem_iff_mem_binaryGate_of_all_isBinary: bridge theorems between PartialMCSP and PartialMCSP.BinaryGate.
• Cslib.PartialMCSP.ofTotal_mem_iff, Cslib.PartialMCSP.toSuccinct_mem_iff, Cslib.PartialMCSP.restrictTable_mem_iff: exact compatibility with MCSP and SuccinctMCSP.

References

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

structure Cslib.PartialMCSP.Instance : Type

An instance of the Partial Minimum Circuit Size Problem (MCSP*): the truth table of a partial Boolean function on arity inputs (none for * / don't-care, some b for a required output b) and a circuit-size threshold [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2; Hirahara2022, ECCC TR22-119, Definition 8.4, p. 30].

• arity : ℕ

  The number of input variables of the partial Boolean function.

• table : Fin (2 ^ self.arity) → Option Bool

  The truth table of the partial Boolean function, indexed via BitString.equivFin.

• threshold : ℕ

  The maximum number of gates allowed.

def Cslib.PartialMCSP.Instance.partialFunction (x : Instance) (y : BitString x.arity) : Option Bool

The partial Boolean function represented by an instance.

@[simp]

theorem Cslib.PartialMCSP.Instance.partialFunction_apply (x : Instance) (y : BitString x.arity) : x.partialFunction y = x.table ((BitString.equivFin x.arity) y)

def Cslib.PartialMCSP.Instance.definedInputs (x : Instance) : Set (BitString x.arity)

The set of inputs on which the partial Boolean function is defined (not *).

def Cslib.PartialMCSP.Instance.definedFinset (x : Instance) : Finset (BitString x.arity)

The finite set of inputs on which the partial Boolean function is defined.

@[simp]

theorem Cslib.PartialMCSP.Instance.coe_definedFinset (x : Instance) : ↑x.definedFinset = x.definedInputs

def Cslib.PartialMCSP.Instance.completion (x : Instance) (y : BitString x.arity) : Bool

The canonical total completion of x.partialFunction that maps undefined (*) entries to false. On x.definedInputs, a circuit agrees with x if and only if it agrees with x.completion.

def Cslib.PartialMCSP.Instance.AgreesWith (x : Instance) (f : BooleanFunction x.arity) : Prop

A total Boolean function f agrees with (extends) the partial truth table of x when f y = b for every input y where x.partialFunction y = some b [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2].

theorem Cslib.PartialMCSP.Instance.agreesWith_iff_table {x : Instance} {f : BooleanFunction x.arity} : x.AgreesWith f ↔ ∀ (i : Fin (2 ^ x.arity)) (b : Bool), x.table i = some b → f ((BitString.equivFin x.arity).symm i) = b

Agreement stated directly in terms of the table indices Fin (2 ^ x.arity).

theorem Cslib.PartialMCSP.Instance.agreesWith_iff_eqOn_completion {x : Instance} {f : BooleanFunction x.arity} : x.AgreesWith f ↔ Set.EqOn f x.completion x.definedInputs

A total function agrees with x iff it equals x.completion on x.definedInputs.

theorem Cslib.PartialMCSP.Instance.agreesWith_completion (x : Instance) : x.AgreesWith x.completion

The canonical completion x.completion agrees with x.

theorem Cslib.PartialMCSP.Instance.computesOn_definedInputs_iff {x : Instance} {c : Circuits.Circuit Circuits.Boolean.signature x.arity 1} : c.ComputesOn Circuits.Boolean.interpretation x.definedInputs (Circuits.single x.completion) ↔ x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0

A one-output circuit computes single x.completion on x.definedInputs if and only if its output 0 agrees with x.

def Cslib.PartialMCSP : Set PartialMCSP.Instance

The Partial Minimum Circuit Size Problem (MCSP*) [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2; Hirahara2022, ECCC TR22-119, Definition 8.4, p. 30]: the partial-function instances that can be computed on their defined inputs by a De Morgan circuit with at most threshold gates.

def Cslib.PartialMCSP.BinaryGate : Set Instance

The Partial Minimum Circuit Size Problem under the binary-gate cost measure [Ilango2020FOCS, Section II.B and Section III.B, p. 427; ECCC TR20-183, Section 2.2]: the partial-function instances for which some De Morgan circuit using at most threshold binary (AND/OR) gates agrees with the partial truth table.

theorem Cslib.PartialMCSP.mem_iff {x : Instance} : x ∈ PartialMCSP ↔ Circuits.complexityOn Circuits.Boolean.interpretation x.definedInputs (Circuits.single x.completion) ≤ x.threshold

theorem Cslib.PartialMCSP.mem_iff_exists_circuit {x : Instance} : x ∈ PartialMCSP ↔ ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), c.size ≤ x.threshold ∧ ∀ (y : BitString x.arity) (b : Bool), x.partialFunction y = some b → c.eval Circuits.Boolean.interpretation y 0 = b

An instance is in PartialMCSP if and only if some De Morgan circuit of size at most x.threshold agrees with x.partialFunction on all defined inputs.

theorem Cslib.PartialMCSP.mem_iff_exists_circuit_table {x : Instance} : x ∈ PartialMCSP ↔ ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), c.size ≤ x.threshold ∧ ∀ (i : Fin (2 ^ x.arity)) (b : Bool), x.table i = some b → c.eval Circuits.Boolean.interpretation ((BitString.equivFin x.arity).symm i) 0 = b

Circuit characterization of PartialMCSP indexed by Fin (2 ^ x.arity).

theorem Cslib.PartialMCSP.mem_iff_exists_total_extension {x : Instance} : x ∈ PartialMCSP ↔ ∃ (f : BooleanFunction x.arity), x.AgreesWith f ∧ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single f) ≤ x.threshold

Total-extension characterization of PartialMCSP [Ilango2020FOCS, Section II.B; ECCC TR20-183, Section 2.2]: an instance is in PartialMCSP if and only if some total Boolean function f agrees with x on all non-* entries and has circuit complexity at most x.threshold.

theorem Cslib.PartialMCSP.mem_iff_exists_mem_computableFunctions {x : Instance} : x ∈ PartialMCSP ↔ ∃ f ∈ Circuits.Boolean.computableFunctions x.arity x.threshold, x.AgreesWith f

An instance is in PartialMCSP if and only if some function in computableFunctions x.arity x.threshold agrees with x.

theorem Cslib.PartialMCSP.mem_of_le {n s t : ℕ} {T : Fin (2 ^ n) → Option Bool} (h : { arity := n, table := T, threshold := s } ∈ PartialMCSP) (hst : s ≤ t) : { arity := n, table := T, threshold := t } ∈ PartialMCSP

Raising the threshold preserves membership in PartialMCSP.

theorem Cslib.PartialMCSP.mem_binaryGate_of_le {n s t : ℕ} {T : Fin (2 ^ n) → Option Bool} (h : { arity := n, table := T, threshold := s } ∈ BinaryGate) (hst : s ≤ t) : { arity := n, table := T, threshold := t } ∈ BinaryGate

Raising the threshold preserves membership in PartialMCSP.BinaryGate.

Bridge between all-gates PartialMCSP and binary-gate PartialMCSP.BinaryGate

theorem Cslib.PartialMCSP.mem_binaryGate_of_mem {x : Instance} (h : x ∈ PartialMCSP) : x ∈ BinaryGate

Every yes-instance under the all-gates measure is a yes-instance under the binary-gate measure, since c.program.cost binaryCost ≤ c.size.

def Cslib.PartialMCSP.Instance.EssentialAt (x : Instance) (i : Fin x.arity) : Prop

Coordinate i is essential for the partial Boolean function of x when some pair of inputs differing only at i are both defined in x and assigned opposite Boolean values.

theorem Cslib.PartialMCSP.Instance.EssentialAt.essentialAt_of_agreesWith {x : Instance} {i : Fin x.arity} {f : BooleanFunction x.arity} (hi : x.EssentialAt i) (hf : x.AgreesWith f) : Circuits.EssentialAt f i

If coordinate i is essential for x, then i is essential for every total Boolean function that agrees with x.

theorem Cslib.PartialMCSP.Instance.EssentialAt.mem_inputSupport {x : Instance} {i : Fin x.arity} {c : Circuits.Circuit Circuits.Boolean.signature x.arity 1} (hi : x.EssentialAt i) (hc : x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0) : i ∈ c.inputSupport

If coordinate i is essential for x, then i belongs to c.inputSupport for every circuit c whose output agrees with x.

theorem Cslib.PartialMCSP.Instance.inputSupport_eq_univ_of_forall_essentialAt {x : Instance} {c : Circuits.Circuit Circuits.Boolean.signature x.arity 1} (hess : ∀ (i : Fin x.arity), x.EssentialAt i) (hc : x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0) : c.inputSupport = Finset.univ

When all x.arity input coordinates are essential for x, every circuit agreeing with x has full input support c.inputSupport = Finset.univ.

theorem Cslib.PartialMCSP.Instance.arity_le_one_add_cost_binaryCost {x : Instance} {c : Circuits.Circuit Circuits.Boolean.signature x.arity 1} (hess : ∀ (i : Fin x.arity), x.EssentialAt i) (hc : x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0) : x.arity ≤ 1 + c.program.cost Circuits.Boolean.binaryCost

When all x.arity input coordinates are essential for x, every circuit agreeing with x uses at least x.arity - 1 binary (AND/OR) gates (x.arity ≤ 1 + c.program.cost binaryCost).

theorem Cslib.PartialMCSP.not_mem_binaryGate_of_threshold_lt {x : Instance} (hess : ∀ (i : Fin x.arity), x.EssentialAt i) (ht : x.threshold + 1 < x.arity) : x ∉ BinaryGate

When all x.arity coordinates are essential for x and x.threshold + 1 < x.arity (i.e. x.threshold < x.arity - 1), x is a no-instance even under the binary-gate measure.

theorem Cslib.PartialMCSP.not_mem_of_threshold_lt {x : Instance} (hess : ∀ (i : Fin x.arity), x.EssentialAt i) (ht : x.threshold + 1 < x.arity) : x ∉ PartialMCSP

When all x.arity coordinates are essential for x and x.threshold + 1 < x.arity, x is a no-instance of PartialMCSP.

theorem Cslib.PartialMCSP.isBinary_of_mem_of_threshold_le {x : Instance} {c : Circuits.Circuit Circuits.Boolean.signature x.arity 1} (hess : ∀ (i : Fin x.arity), x.EssentialAt i) (hc : x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0) (hsize : c.size ≤ x.threshold) (ht : x.threshold + 1 ≤ x.arity) : c.program.cost Circuits.Boolean.binaryCost = x.arity - 1 ∧ c.size = x.arity - 1 ∧ ∀ (k : Fin c.size), Circuits.Boolean.Op.IsBinary (c.program.lines k).op

Threshold-n - 1 rigidity. When all x.arity coordinates are essential for x and x.threshold + 1 ≤ x.arity, any all-gates circuit c of size at most x.threshold agreeing with x has c.program.cost binaryCost = x.arity - 1, c.size = x.arity - 1, and consists exclusively of binary AND and OR gates (no NOT or constant gates).

theorem Cslib.PartialMCSP.mem_of_exists_all_isBinary {x : Instance} (h : ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), (∀ (k : Fin c.size), Circuits.Boolean.Op.IsBinary (c.program.lines k).op) ∧ c.program.cost Circuits.Boolean.binaryCost ≤ x.threshold ∧ x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0) : x ∈ PartialMCSP

Any circuit whose gates are all binary AND/OR gates has c.size = c.program.cost binaryCost, so a binary-gate witness without NOT or constant gates is immediately an all-gates witness of the same size.

theorem Cslib.PartialMCSP.mem_iff_exists_all_isBinary_of_threshold_eq_arity_sub_one {x : Instance} (hess : ∀ (i : Fin x.arity), x.EssentialAt i) (hpos : 1 ≤ x.arity) (ht : x.threshold = x.arity - 1) : x ∈ PartialMCSP ↔ ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), c.size = x.arity - 1 ∧ (∀ (k : Fin c.size), Circuits.Boolean.Op.IsBinary (c.program.lines k).op) ∧ x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0

When all x.arity coordinates are essential for x, 1 ≤ x.arity, and x.threshold = x.arity - 1, x ∈ PartialMCSP if and only if there is a circuit of size x.arity - 1 whose gates are all binary AND/OR gates that agrees with x.

theorem Cslib.PartialMCSP.mem_iff_mem_binaryGate_of_all_isBinary {x : Instance} (h : x ∈ BinaryGate → ∃ (c : Circuits.Circuit Circuits.Boolean.signature x.arity 1), (∀ (k : Fin c.size), Circuits.Boolean.Op.IsBinary (c.program.lines k).op) ∧ c.program.cost Circuits.Boolean.binaryCost ≤ x.threshold ∧ x.AgreesWith fun (y : BitString x.arity) => c.eval Circuits.Boolean.interpretation y 0) : x ∈ PartialMCSP ↔ x ∈ BinaryGate

If every binary-gate circuit for x of cost at most x.threshold can be replaced by a NOT-free, constant-free circuit of no greater binary cost (for example, in monotone reductions such as [Ilango2020FOCS, Theorem I.3; ECCC TR20-183, Theorem 3] where yes-instances have read-once monotone formulas of size n - 1 and no-instances require at least n binary gates), then x ∈ PartialMCSP ↔ x ∈ BinaryGate.

Embeddings from MCSP and into SuccinctMCSP

def Cslib.PartialMCSP.Instance.ofTotal (x : MCSP.Instance) : Instance

View a total MCSP.Instance as a PartialMCSP.Instance with no * (none) entries.

@[simp]

theorem Cslib.PartialMCSP.Instance.partialFunction_ofTotal (x : MCSP.Instance) (y : BitString x.arity) : (ofTotal x).partialFunction y = some (x.function y)

@[simp]

theorem Cslib.PartialMCSP.Instance.definedInputs_ofTotal (x : MCSP.Instance) : (ofTotal x).definedInputs = Set.univ

@[simp]

theorem Cslib.PartialMCSP.Instance.completion_ofTotal (x : MCSP.Instance) : (ofTotal x).completion = x.function

@[simp]

theorem Cslib.PartialMCSP.ofTotal_mem_iff (x : MCSP.Instance) : Instance.ofTotal x ∈ PartialMCSP ↔ x ∈ MCSP

A total instance belongs to PartialMCSP if and only if it belongs to MCSP.

def Cslib.PartialMCSP.Instance.toSuccinct (x : Instance) : SuccinctMCSP.Instance

View a PartialMCSP.Instance as a SuccinctMCSP.Instance whose samples are the defined entries of its truth table.

@[simp]

theorem Cslib.PartialMCSP.toSuccinct_mem_iff (x : Instance) : x.toSuccinct ∈ SuccinctMCSP ↔ x ∈ PartialMCSP

A partial truth table is in PartialMCSP if and only if its set of defined samples is in SuccinctMCSP.

def Cslib.PartialMCSP.Instance.restrictTable {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) : Instance

Restrict a total truth table T : BitString (2 ^ n) to a subset S : Finset (BitString n) of defined inputs at threshold s, setting all entries outside S to none (*).

@[simp]

theorem Cslib.PartialMCSP.Instance.arity_restrictTable {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) : (restrictTable T S s).arity = n

@[simp]

theorem Cslib.PartialMCSP.Instance.threshold_restrictTable {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) : (restrictTable T S s).threshold = s

@[simp]

theorem Cslib.PartialMCSP.Instance.partialFunction_restrictTable {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) (y : BitString n) : (restrictTable T S s).partialFunction y = if y ∈ S then some (T ((BitString.equivFin n) y)) else none

@[simp]

theorem Cslib.PartialMCSP.Instance.definedFinset_restrictTable {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) : (restrictTable T S s).definedFinset = S

@[simp]

theorem Cslib.PartialMCSP.Instance.toSuccinct_restrictTable {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) : (restrictTable T S s).toSuccinct = SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s

Viewing Instance.restrictTable T S s as a SuccinctMCSP.Instance via Instance.toSuccinct yields SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s.

@[simp]

theorem Cslib.PartialMCSP.restrictTable_mem_iff {n : ℕ} (T : BitString (2 ^ n)) (S : Finset (BitString n)) (s : ℕ) : Instance.restrictTable T S s ∈ PartialMCSP ↔ SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s ∈ SuccinctMCSP

The partial truth table Instance.restrictTable T S s is in PartialMCSP if and only if SuccinctMCSP.Instance.ofFunction ((MCSP.truthTable n).symm T) S s is in SuccinctMCSP.