#Knapsack: counting the solutions of a subset-sum instance

The counting version of DescriptiveComplexity.Knapsack: the number of sets of items whose binary weights sum exactly to the target (DescriptiveComplexity.KnapsackSol).

Membership in #P (DescriptiveComplexity.sharpKnapsack_mem_sharpP) is where a counting definition differs from a Σ₁ one. The certificate of DescriptiveComplexity.knapsack_sigmaSODefinable carries, besides the chosen items, the running totals and the carries of an addition walk, and a count of certificates is a count of solutions only if a solution has one: the totals and carries are forced where the walk reads them (DescriptiveComplexity.isChain_agree), and the counting kernel (DescriptiveComplexity.sharpKnapsackKernel) forbids them anywhere else. The certificates are then the solutions, bijectively (DescriptiveComplexity.knapsackEquiv).

def DescriptiveComplexity.KnapsackSol (A : Type) [FirstOrder.Language.binWeights.Structure A] (S : A → Prop) : Prop

The set S of items is a solution: the instance is finite, its order is linear, and the weights of S sum exactly to the target.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.certOfWalk {A : Type} [FirstOrder.Language.binWeights.Structure A] (S : A → Prop) (PS Cy : A → A → Prop) : knapsackGuessBlock.Assignment A

The certificate built on a walk: the chosen items, and the totals and carries of the walk kept only where a walk reads them.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.certOfWalk S PS Cy DescriptiveComplexity.KnapsackGuessBlockIx.sel = fun (w : Fin 1 → A) => S (w 0)

theorem DescriptiveComplexity.exists_knapsackCert {A : Type} [FirstOrder.Language.binWeights.Structure A] [Finite A] {S : A → Prop} (h : KnapsackSol A S) : ∃ (PS : A → A → Prop) (Cy : A → A → Prop), IsChain BWLe BWItem BWLe BWPosn S BWBit PS Cy ∧ KnapsackCert A (certOfWalk S PS Cy)

A solution has a certificate.

theorem DescriptiveComplexity.knapsackSol_of_cert {A : Type} [FirstOrder.Language.binWeights.Structure A] [Finite A] {ρ : knapsackGuessBlock.Assignment A} (h : KnapsackCert A ρ) : KnapsackSol A fun (i : A) => ρ KnapsackGuessBlockIx.sel ![i]

The chosen items of a certificate are a solution.

noncomputable def DescriptiveComplexity.knapsackEquiv (A : Type) [FirstOrder.Language.binWeights.Structure A] [Finite A] : { ρ : knapsackGuessBlock.Assignment A // A ⊨ sharpKnapsackKernel } ≃ { S : A → Prop // KnapsackSol A S }

The solutions of a subset-sum instance 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.

noncomputable def DescriptiveComplexity.SharpKnapsack : CountingProblem FirstOrder.Language.binWeights

#Knapsack: the number of sets of items whose weights sum exactly to the target.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpKnapsack_support_iff (A : Type) [FirstOrder.Language.binWeights.Structure A] [Finite A] : SharpKnapsack.support.Holds A ↔ Knapsack.Holds A

The support of #Knapsack is Knapsack. Registered in the Lax archive as Lax280166.KnapsackComplete.sharpKnapsack_support_iff.

theorem DescriptiveComplexity.sharpKnapsack_mem_sharpP : SharpP.Mem SharpKnapsack

#Knapsack is in #P: a solution has exactly one certificate of the counting kernel.