MCSP is in NP

An instance of the Minimum Circuit Size Problem (Cslib.MCSP) is encoded by the 2 ^ n bits of its truth table followed by the threshold in binary (Cslib.MCSP.encInstance); the length of the table determines n. The problem is in NP for this encoding (Cslib.MCSP.mem_NP) Kabanets and Cai: a certificate is a circuit with at most as many gates as the threshold, in the format of Cslib.Circuits.Boolean.readCertificate, and the verifier checks that it is a circuit and evaluates it on all 2 ^ n inputs. The threshold may be exponentially larger than the table; certificates are capped at the truth-table bound 2 ^ n (2 n + 3) + 1, which every function on n inputs meets (Cslib.Circuits.Boolean.complexity_le_two_pow_mul_add_one), so they stay polynomially long in the length of the table.

Main definitions

• Cslib.MCSP.encInstance: the encoding of instances.
• Cslib.MCSP.sampleBudget, Cslib.MCSP.budget: certificate gate budgets for t samples and for a full 2 ^ n-entry truth table.
• Cslib.MCSP.validCertificate, Cslib.MCSP.evalCertificate, Cslib.MCSP.checkCertificateOn, Cslib.MCSP.checkCertificate: certificate well-formedness, evaluation, and generic parameterized verifiers over a list of tests and over all 2 ^ m inputs.
• Cslib.MCSP.tableFunction: the Boolean function read from a truth-table list.
• Cslib.MCSP.verifier: the verifier.
• Cslib.MCSP.tableVerifier: the verifier on the bits of a truth table and a threshold.

Main results

• Cslib.MCSP.exists_circuit_of_checkCertificateOn, Cslib.MCSP.exists_checkCertificateOn_append, Cslib.MCSP.exists_circuit_of_checkCertificate, Cslib.MCSP.exists_checkCertificate_append, Cslib.MCSP.exists_circuit_of_validCertificate, Cslib.MCSP.exists_validCertificate_of_circuit: soundness and completeness of the generic verifiers and of validCertificate / evalCertificate.
• Cslib.MCSP.mem_of_verifier_eq_true, Cslib.MCSP.exists_verifier_append: the verifier accepts some certificate exactly for the instances in MCSP, certificates of a fixed length suffice, and bits after them are ignored.
• Cslib.MCSP.complexity_le_of_tableVerifier, Cslib.MCSP.exists_tableVerifier_append: soundness and completeness of tableVerifier on truth-table lists of length 2 ^ m.
• Cslib.MCSP.isVerifier: the verifier is correct.
• Cslib.MCSP.computableInPolyTime_tableValue: truth table lookup is polynomial-time.
• Cslib.MCSP.computableInPolyTime_validCertificate, Cslib.MCSP.computableInPolyTime_evalCertificate, Cslib.MCSP.computableInPolyTime_checkCertificateOn, Cslib.MCSP.computableInPolyTime_checkCertificate: certificate well-formedness, evaluation, and generic verification are polynomial-time.
• Cslib.MCSP.computableInPolyTime_verifier, Cslib.MCSP.computableInPolyTime_tableVerifier: the verifiers are polynomial-time.
• Cslib.MCSP.mem_NP: MCSP is in NP.

References

• V. Kabanets, J.-Y. Cai, Circuit minimization problem

def Cslib.MCSP.encInstance : Instance ↪ List Bool

Instances of MCSP encoded by the bits of the truth table, then the threshold in binary.

theorem Cslib.MCSP.encInstance_apply (x : Instance) : encInstance x = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat) (List.ofFn x.table, x.threshold)

def Cslib.MCSP.sampleBudget (n t s : ℕ) : ℕ

The number of gates a certificate for t samples on n inputs may describe: the threshold s, capped at the sample-set bound t * (2 * n + 3) + 1.

@[simp]

theorem Cslib.MCSP.sampleBudget_zero (n t : ℕ) : sampleBudget n t 0 = 0

def Cslib.MCSP.budget (n s : ℕ) : ℕ

The number of gates a certificate may describe: the threshold, capped at the truth-table bound that every function meets.

def Cslib.MCSP.tableValue (table y : List Bool) : Bool

The value of the function of an instance at the input with bits y.

def Cslib.MCSP.tableFunction (m : ℕ) (T : List Bool) : BooleanFunction m

The function on m inputs with the truth table T, read as MCSP reads truth tables.

def Cslib.MCSP.validCertificate (m S : ℕ) (w : List Bool) : Bool

Whether w, read as a certificate for m inputs and gate budget S, describes a well-formed circuit code with a valid output wire.

def Cslib.MCSP.evalCertificate (m S : ℕ) (w y : List Bool) : Bool

Evaluate the certificate w (for m inputs and gate budget S) on input y.

def Cslib.MCSP.checkCertificateOn {α : Type} (tests : List α) (input : α → List Bool) (accept : α → Bool → Bool) (m S : ℕ) (w : List Bool) : Bool

A certificate verifier parameterized by a list of tests, the input bitstring of each test, and the acceptance condition on a test and the circuit output on its input.

def Cslib.MCSP.checkCertificate (accept : List Bool → Bool → Bool) (m S : ℕ) (w : List Bool) : Bool

A certificate verifier on all 2 ^ m inputs, parameterized by the acceptance condition on an input and the circuit output on that input.

theorem Cslib.MCSP.exists_circuit_of_checkCertificateOn {α : Type} {tests : List α} {input : α → List Bool} {accept : α → Bool → Bool} {m S : ℕ} {w : List Bool} (hw : checkCertificateOn tests input accept m S w = true) : ∃ (C : Circuits.Circuit Circuits.Boolean.signature m 1), C.size ≤ S ∧ ∀ t ∈ tests, ∀ (y : BitString m), input t = List.ofFn y → accept t (C.eval Circuits.Boolean.interpretation y 0) = true

An accepted certificate decoded by checkCertificateOn describes a circuit of size at most S meeting the acceptance condition on every test in tests whose input is List.ofFn y.

theorem Cslib.MCSP.exists_checkCertificateOn_append {α : Type} {tests : List α} {input : α → List Bool} {accept : α → Bool → Bool} {m S : ℕ} {C : Circuits.Circuit Circuits.Boolean.signature m 1} (hcS : C.size ≤ S) (haccept : ∀ t ∈ tests, ∃ (y : BitString m), input t = List.ofFn y ∧ accept t (C.eval Circuits.Boolean.interpretation y 0) = true) : ∃ (u : List Bool), u.length = Circuits.Boolean.certLength m S ∧ ∀ (extra : List Bool), checkCertificateOn tests input accept m S (u ++ extra) = true

A circuit of size at most S meeting the acceptance condition on every test in tests has a certificate of length certLength m S, accepted by checkCertificateOn whatever bits follow it.

theorem Cslib.MCSP.exists_circuit_of_checkCertificate {accept : List Bool → Bool → Bool} {m S : ℕ} {w : List Bool} (hw : checkCertificate accept m S w = true) : ∃ (C : Circuits.Circuit Circuits.Boolean.signature m 1), C.size ≤ S ∧ ∀ (y : BitString m), accept (List.ofFn y) (C.eval Circuits.Boolean.interpretation y 0) = true

An accepted certificate decoded by checkCertificate describes a circuit of size at most S meeting the acceptance condition on every input.

theorem Cslib.MCSP.exists_checkCertificate_append {accept : List Bool → Bool → Bool} {m S : ℕ} {C : Circuits.Circuit Circuits.Boolean.signature m 1} (hcS : C.size ≤ S) (haccept : ∀ (y : BitString m), accept (List.ofFn y) (C.eval Circuits.Boolean.interpretation y 0) = true) : ∃ (u : List Bool), u.length = Circuits.Boolean.certLength m S ∧ ∀ (extra : List Bool), checkCertificate accept m S (u ++ extra) = true

A circuit of size at most S meeting the acceptance condition has a certificate of length certLength m S, accepted whatever bits follow it.

theorem Cslib.MCSP.exists_circuit_of_validCertificate {n s : ℕ} {w : List Bool} (hw : validCertificate n s w = true) : ∃ (C : Circuits.Circuit Circuits.Boolean.signature n 1), C.size ≤ s ∧ ∀ (x : BitString n), C.eval Circuits.Boolean.interpretation x 0 = evalCertificate n s w (List.ofFn x)

Soundness of validCertificate: a well-formed certificate for (n, s) decodes to a circuit of size at most s whose evaluation agrees with evalCertificate.

theorem Cslib.MCSP.exists_validCertificate_of_circuit {n s : ℕ} (C : Circuits.Circuit Circuits.Boolean.signature n 1) (hcS : C.size ≤ s) : ∃ (w : List Bool), w.length = Circuits.Boolean.certLength n s ∧ validCertificate n s w = true ∧ ∀ (x : BitString n), evalCertificate n s w (List.ofFn x) = C.eval Circuits.Boolean.interpretation x 0

Completeness of validCertificate: every circuit of size at most s on n inputs has a canonical certificate of length certLength n s satisfying validCertificate whose evalCertificate agrees with the circuit on all n-bit inputs.

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

The verifier for MCSP: the certificate must describe a circuit on n inputs with at most budget n s gates (readCertificate) that agrees with the truth table on all 2 ^ n inputs.

Correctness

theorem Cslib.MCSP.getD_boundedBinaryValue_reverse_ofFn {α : Type u_1} {n : ℕ} (T : Fin (2 ^ n) → α) (y : BitString n) (default : α) : (List.ofFn T).getD (BitString.boundedBinaryValue (List.ofFn T).length (List.ofFn y).reverse) default = T ((BitString.equivFin n) y)

Generic truth-table indexing into a function represented as a list via List.ofFn.

theorem Cslib.MCSP.tableValue_ofFn (x : Instance) (y : BitString x.arity) : tableValue (List.ofFn x.table) (List.ofFn y) = x.function y

The verifier reads the function of an instance from its truth table.

@[simp]

theorem Cslib.MCSP.tableFunction_ofFn_truthTable (m : ℕ) (f : BooleanFunction m) : tableFunction m (List.ofFn ((truthTable m) f)) = f

The truth table of a function, as a list, is read back as the function.

noncomputable def Cslib.MCSP.certPolynomial : Polynomial ℕ

The polynomial bounding the length of certificates.

theorem Cslib.MCSP.certLength_sampleBudget_le {n t s L : ℕ} (hn : n ≤ L) (ht : t ≤ L) : Circuits.Boolean.certLength n (sampleBudget n t s) ≤ Polynomial.eval L certPolynomial

When the arity n and sample count t are each at most L, the certificate length at gate budget sampleBudget n t s is bounded by certPolynomial.eval L.

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

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

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

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

theorem Cslib.MCSP.isVerifier : Complexity.IsVerifier encInstance certPolynomial verifier MCSP

MCSP.verifier verifies MCSP, with certificates of length certPolynomial.

Polynomial time

def Cslib.MCSP.tableVerifier (r : (List Bool × ℕ) × List Bool) : Bool

The verifier on the bits of a truth table, a threshold and a certificate, with the number of inputs read from the length of the table: MCSP.verifier on raw data (Cslib.MCSP.verifier_eq_tableVerifier), defined on every list of bits.

theorem Cslib.MCSP.verifier_eq_tableVerifier (p : Instance × List Bool) : verifier p = tableVerifier ((List.ofFn p.1.table, p.1.threshold), p.2)

theorem Cslib.MCSP.complexity_le_of_tableVerifier {m s : ℕ} {T c : List Bool} (hT : T.length = 2 ^ m) (h : tableVerifier ((T, s), c) = true) : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (tableFunction m T)) ≤ s

An accepted certificate for a truth table of length 2 ^ m bounds the complexity of its function.

theorem Cslib.MCSP.exists_tableVerifier_append {m s : ℕ} {T : List Bool} (hT : T.length = 2 ^ m) (h : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (tableFunction m T)) ≤ s) : ∃ (u : List Bool), u.length = Circuits.Boolean.certLength m (budget m s) ∧ ∀ (extra : List Bool), tableVerifier ((T, s), u ++ extra) = true

A truth table of length 2 ^ m whose function has at most s gates has a certificate of length certLength m (budget m s), accepted whatever bits follow it.

theorem Cslib.MCSP.computableInPolyTime_tableValue : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => tableValue p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Looking up an input in a truth table is computable in polynomial time.

theorem Cslib.MCSP.computableInPolyTime_validCertificate {γ : Type} {encIn : γ ↪ List Bool} {m S : γ → ℕ} {w : γ → List Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => validCertificate (m a) (S a) (w a)) encIn Turing.MultiTapeTM.encBool

Checking well-formedness of a certificate is computable in polynomial time when m and S are given in unary.

theorem Cslib.MCSP.computableInPolyTime_evalCertificate {γ : Type} {encIn : γ ↪ List Bool} {m S : γ → ℕ} {w y : γ → List Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) (hy : Turing.MultiTapeTM.ComputableInPolyTime y encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalCertificate (m a) (S a) (w a) (y a)) encIn Turing.MultiTapeTM.encBool

Evaluating a certificate on an input is computable in polynomial time when m and S are given in unary.

theorem Cslib.MCSP.computableInPolyTime_checkCertificateOn {γ α : Type} {encIn : γ ↪ List Bool} {encTest : α ↪ List Bool} {tests : γ → List α} {input : α → List Bool} {m S : γ → ℕ} {w : γ → List Bool} {accept : γ → α → Bool → Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) (htests : Turing.MultiTapeTM.ComputableInPolyTime tests encIn (Turing.MultiTapeTM.encList encTest)) (hinput : Turing.MultiTapeTM.ComputableInPolyTime input encTest Turing.MultiTapeTM.encBits) (haccept : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (γ × α) × Bool) => accept p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encIn encTest) Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => checkCertificateOn (tests a) input (accept a) (m a) (S a) (w a)) encIn Turing.MultiTapeTM.encBool

A generic certificate verifier on a supplied list of tests is computable in polynomial time when its test list, input extraction, and acceptance condition are polynomial-time.

theorem Cslib.MCSP.computableInPolyTime_checkCertificate {γ : Type} {encIn : γ ↪ List Bool} {m S : γ → ℕ} {w : γ → List Bool} {accept : γ → List Bool → Bool → Bool} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) {size : ℕ → ℕ} (hsize : PolynomiallyBounded size) (hbudget : ∀ (a : γ), 2 ^ m a * (2 * m a + 1) ≤ size (encIn a).length) (haccept : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (γ × List Bool) × Bool) => accept p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encIn Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => checkCertificate (accept a) (m a) (S a) (w a)) encIn Turing.MultiTapeTM.encBool

A generic certificate verifier is computable in polynomial time when its acceptance condition is polynomial-time and the number of inputs is bounded by the input length.

theorem Cslib.MCSP.computableInPolyTime_sampleBudget {γ : Type} {encIn : γ ↪ List Bool} {m t s : γ → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => sampleBudget (m a) (t a) (s a)) encIn Turing.MultiTapeTM.encUnary

Computing sampleBudget (m a) (t a) (s a) in unary is polynomial-time when m a and t a are polynomial-time in unary and s a is polynomial-time in binary.

theorem Cslib.MCSP.computableInPolyTime_checkCertificate_table {α : Type} {encT : List α ↪ List Bool} {accept : List α → List Bool → Bool → Bool} (hlen : Turing.MultiTapeTM.ComputableInPolyTime (fun (T : List α) => T.length) encT Turing.MultiTapeTM.encUnary) (hlen_le : ∀ (T : List α), T.length ≤ (encT T).length) (haccept : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (List α × List Bool) × Bool) => accept p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encT Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (r : (List α × ℕ) × List Bool) => checkCertificate (accept r.1.1) (Nat.log 2 r.1.1.length) (sampleBudget (Nat.log 2 r.1.1.length) r.1.1.length r.1.2) r.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encT Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

A certificate verifier on a table list, threshold, and certificate is computable in polynomial time from encPair (encPair encT encNat) encBits when table length is computable in polynomial time into unary, the encoding length bounds the table length, and the acceptance condition is polynomial-time.

theorem Cslib.MCSP.computableInPolyTime_tableVerifier : Turing.MultiTapeTM.ComputableInPolyTime tableVerifier (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The verifier on raw data is polynomial-time.

theorem Cslib.MCSP.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The MCSP verifier is polynomial-time, on certificates of arbitrary length.

theorem Cslib.MCSP.mem_NP : MCSP ∈ Complexity.NP encInstance

MCSP is in NP, for instances encoded by their truth table and the threshold in binary.