Documentation

Complexity.Computability.MCSP.NP

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 #

Main results #

References #

source
def Cslib.MCSP.encInstance :
Instance ↪ List Bool

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

Instances For
    source
    theorem Cslib.MCSP.encInstance_apply (x : Instance) :
    encInstance x = (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encNat) (List.ofFn x.table, x.threshold)
    source
    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.

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

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

      Instances For
        source
        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.

        Instances For

          Correctness #

          source
          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.

          source
          noncomputable def Cslib.MCSP.certPolynomial :
          Polynomial ℕ

          The polynomial bounding the length of certificates.

          Instances For
            source
            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.

            source
            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.

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

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

            Polynomial time #

            source
            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.

            Instances For
              source
              theorem Cslib.MCSP.verifier_eq_tableVerifier (p : Instance × List Bool) :
              verifier p = tableVerifier ((List.ofFn p.1.table, p.1.threshold), p.2)
              source
              theorem Cslib.MCSP.computableTidilyInPolyTime_tableVerifier :
              Turing.MultiTapeTM.ComputableTidilyInPolyTime 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.

              source
              theorem Cslib.MCSP.computableTidilyInPolyTime_verifier :
              Turing.MultiTapeTM.ComputableTidilyInPolyTime verifier (Turing.MultiTapeTM.encPair encInstance Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

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

              source
              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.