Documentation

DescriptiveComplexity.Problems.ZeroOneIP.Counting

#0-1 integer programming: counting the 0-1 solutions #

The counting version of DescriptiveComplexity.ZeroOneIP: the number of 0-1 vectors x with C x = d (DescriptiveComplexity.ZeroOneSol), the entries being written in binary.

Membership in #P (DescriptiveComplexity.sharpZeroOneIP_mem_sharpP) is Knapsack's argument once per row (DescriptiveComplexity.Problems.Knapsack.Counting): the walks of a certificate are forced where they are read (DescriptiveComplexity.isChain_agree) and forbidden elsewhere by the counting kernel, so a solution has exactly one certificate (DescriptiveComplexity.zeroOneIPEquiv).

source
def DescriptiveComplexity.ZeroOneSol (A : Type) [FirstOrder.Language.zeroOneIP.Structure A] (x : A → Prop) :
Prop

The set x of columns is a solution: the instance is finite, its order is linear, and every equation holds.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.certOfWalks {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] (x : A → Prop) (PS Cy : A → A → A → Prop) :
    zeroOneIPGuessBlock.Assignment A

    The certificate built on a family of walks: the chosen columns, and the totals and carries of each row's walk kept only where a walk reads them.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.exists_zeroOneIPCert {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] [Finite A] {x : A → Prop} (h : ZeroOneSol A x) :
      ∃ (PS : A → A → A → Prop) (Cy : A → A → A → Prop), (∀ (r : A), IPRow r → IsChain IPLe IPCol IPLe IPPosn x (IPCoef r) (PS r) (Cy r)) ∧ ZeroOneIPCert A (certOfWalks x PS Cy)

      A solution has a certificate.

      Dependency graph
      source
      theorem DescriptiveComplexity.zeroOneSol_of_cert {A : Type} [FirstOrder.Language.zeroOneIP.Structure A] [Finite A] {ρ : zeroOneIPGuessBlock.Assignment A} (h : ZeroOneIPCert A ρ) :
      ZeroOneSol A fun (j : A) => ρ ZeroOneIPGuessBlockIx.x ![j]

      The chosen columns of a certificate are a solution.

      Dependency graph
      source
      noncomputable def DescriptiveComplexity.zeroOneIPEquiv (A : Type) [FirstOrder.Language.zeroOneIP.Structure A] [Finite A] :
      { ρ : zeroOneIPGuessBlock.Assignment A // A ⊨ sharpZeroOneIPKernel } ≃ { x : A → Prop // ZeroOneSol A x }

      The solutions of a 0-1 integer program are the witnesses of the counting kernel, bijectively: a solution has exactly one certificate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        noncomputable def DescriptiveComplexity.SharpZeroOneIP :
        CountingProblem FirstOrder.Language.zeroOneIP

        #0-1 integer programming: the number of 0-1 vectors satisfying every equation of the program.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.sharpZeroOneIP_support_iff (A : Type) [FirstOrder.Language.zeroOneIP.Structure A] [Finite A] :
          SharpZeroOneIP.support.Holds A ↔ ZeroOneIP.Holds A

          The support of #0-1 integer programming is 0-1 integer programming. Registered in the Lax archive as Lax280166.ZeroOneIPComplete.sharpZeroOneIP_support_iff.

          Dependency graph
          source
          theorem DescriptiveComplexity.sharpZeroOneIP_mem_sharpP :
          SharpP.Mem SharpZeroOneIP

          #0-1 integer programming is in #P.

          Dependency graph