Documentation

DescriptiveComplexity.Problems.Knapsack.CountingHardness

#Knapsack is parsimoniously #P-complete #

Karp's reduction of Exact Cover to Knapsack (DescriptiveComplexity.Problems.Knapsack.Hardness) is parsimonious as it stands. Its items are the sets of the family, one each, so a set of items is a subfamily; and the weights of a set of items sum to the target exactly when the subfamily is an exact cover, the digit of the block of a ground element counting the chosen sets that contain it. Hence the solutions of the interpreted instance are the exact covers of the set system, bijectively (DescriptiveComplexity.KnapRed.solEquiv).

source
def DescriptiveComplexity.KnapRed.solEquiv (A : Type) [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a₀ : A} (ha₀ : IsBot a₀) :
{ G : A → Prop // ExactCoverBy SSElem SSFam SSMem G } ≃ { S : kInterp.Map A → Prop // KnapsackSol (kInterp.Map A) S }

The solutions of the interpreted subset-sum instance are the exact covers of the set system, bijectively.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.KnapRed.sharpKnapsack_map (A : Type) [FirstOrder.Language.setSystem.Structure A] [LinearOrder A] [Finite A] [Nonempty A] :
    SharpKnapsack.Count (kInterp.Map A) = SharpExactCover.Count A

    Correctness of the interpretation, for counting.

    Dependency graph
    source
    noncomputable def DescriptiveComplexity.sharpExactCover_ordered_parsimonious_sharpKnapsack :
    OrderedParsimoniousReduction SharpExactCover SharpKnapsack

    #ExactCover reduces parsimoniously to #Knapsack.

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

      #Knapsack is parsimoniously #P-hard.

      Dependency graph
      source
      theorem DescriptiveComplexity.sharpKnapsack_sharpP_parsimoniousComplete :
      SharpP.ParsimoniousComplete SharpKnapsack

      #Knapsack is parsimoniously #P-complete, its weights being written in binary. Registered in the Lax archive as Lax280166.KnapsackComplete.sharpKnapsack_sharpP_parsimoniousComplete.

      Dependency graph
      source
      theorem DescriptiveComplexity.sharpKnapsack_sharpP_complete :
      SharpP.Complete SharpKnapsack

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

      Dependency graph