Documentation

DescriptiveComplexity.Problems.ZeroOneIP.CountingHardness

#0-1 integer programming is parsimoniously #P-complete #

The reduction of Knapsack to 0-1 integer programming (DescriptiveComplexity.Problems.ZeroOneIP.Hardness) reads a subset-sum instance as a program with one equation: the items become the columns, and the interpreted universe is a copy of the input. A set of items is a 0-1 vector, and it sums to the target exactly when the equation holds, so the solutions correspond bijectively (DescriptiveComplexity.IPRed.solEquiv).

source
def DescriptiveComplexity.IPRed.solEquiv (A : Type) [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] [Finite A] {a₀ : A} (ha₀ : IsBot a₀) :
{ S : A → Prop // KnapsackSol A S } ≃ { x : ipInterp.Map A → Prop // ZeroOneSol (ipInterp.Map A) x }

The solutions of the one-equation program are the solutions of the subset-sum instance, bijectively.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.IPRed.sharpZeroOneIP_map (A : Type) [FirstOrder.Language.binWeights.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
    SharpZeroOneIP.Count (ipInterp.Map A) = SharpKnapsack.Count A

    Correctness of the interpretation, for counting.

    Dependency graph
    source
    noncomputable def DescriptiveComplexity.sharpKnapsack_ordered_parsimonious_sharpZeroOneIP :
    OrderedParsimoniousReduction SharpKnapsack SharpZeroOneIP

    #Knapsack reduces parsimoniously to #0-1 integer programming.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.sharpZeroOneIP_sharpP_parsimoniousHard :
      SharpP.ParsimoniousHard SharpZeroOneIP

      #0-1 integer programming is parsimoniously #P-hard.

      Dependency graph
      source
      theorem DescriptiveComplexity.sharpZeroOneIP_sharpP_parsimoniousComplete :
      SharpP.ParsimoniousComplete SharpZeroOneIP

      #0-1 integer programming is parsimoniously #P-complete, its entries being written in binary. Registered in the Lax archive as Lax280166.ZeroOneIPComplete.sharpZeroOneIP_sharpP_parsimoniousComplete.

      Dependency graph
      source
      theorem DescriptiveComplexity.sharpZeroOneIP_sharpP_complete :
      SharpP.Complete SharpZeroOneIP

      SharpZeroOneIP is #P-complete: parsimoniously, hence under subtractive reductions.

      Dependency graph