Knapsack is in NP

The Σ₁ definition of DescriptiveComplexity.Knapsack. Verifying that a set of binary weights sums to the target is the one place in the catalog where the certificate has to carry arithmetic: the guess is

• sel, the chosen items;
• psum i p, the bits of the running total over the chosen items up to i;
• carry i p, the carries of the addition that appends i to that total,

and the kernel checks, first-order, that each step is a ripple-carry addition – every bit the exclusive or of the three inputs, every carry their majority – with no carry into the lowest position and none out of the highest. That the chain really computes the sum is DescriptiveComplexity.binNum_ripple, and that a chain exists whenever the sum fits is DescriptiveComplexity.exists_ripple (DescriptiveComplexity.Numbers.BinRel).

Walking the items in order is what makes a single relation psum enough, and it is why the vocabulary orders the items and not only the bit positions.

@[reducible, inline]

abbrev DescriptiveComplexity.ksTgtSym : ksSOLang.Relations 1

The tgt symbol over the sum.

Equations

• DescriptiveComplexity.ksTgtSym = Sum.inl FirstOrder.Language.bwTgt

def DescriptiveComplexity.knapsackGuessBlock : SOBlock

The single existential block of the Σ₁ definition of Knapsack: the chosen items (unary), the running partial sums and the carries (binary, an item and a bit position).

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.ksCarrySym : ksSOLang.Relations 2

The carry symbol over the sum.

Equations

• DescriptiveComplexity.ksCarrySym = Sum.inr DescriptiveComplexity.ksCarryRel

def DescriptiveComplexity.ksPSRel : knapsackGuessBlock.lang.Relations 2

The pS relation variable.

Equations

• DescriptiveComplexity.ksPSRel = ⟨DescriptiveComplexity.KnapsackGuessBlockIx.pS, DescriptiveComplexity.ksPSRel._proof_1⟩

inductive DescriptiveComplexity.KnapsackGuessBlockIx : Type

The relation variables of the block.

• sel : KnapsackGuessBlockIx

  The chosen items.

• pS : KnapsackGuessBlockIx

  The running partial sums: pS i p is the bit p of the total up to the item i.

• carry : KnapsackGuessBlockIx

  The carries of the step appending an item.

@[reducible, inline]

abbrev DescriptiveComplexity.ksBitSym : ksSOLang.Relations 2

The bit symbol over the sum.

Equations

• DescriptiveComplexity.ksBitSym = Sum.inl FirstOrder.Language.bwBit

@[reducible, inline]

abbrev DescriptiveComplexity.ksSelSym : ksSOLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.ksSelSym = Sum.inr DescriptiveComplexity.ksSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.ksPosnSym : ksSOLang.Relations 1

The posn symbol over the sum.

Equations

• DescriptiveComplexity.ksPosnSym = Sum.inl FirstOrder.Language.bwPosn

@[reducible, inline]

abbrev DescriptiveComplexity.ksPSSym : ksSOLang.Relations 2

The pS symbol over the sum.

Equations

• DescriptiveComplexity.ksPSSym = Sum.inr DescriptiveComplexity.ksPSRel

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqKnapsackGuessBlockIx : DecidableEq KnapsackGuessBlockIx

Equations

• DescriptiveComplexity.instDecidableEqKnapsackGuessBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev DescriptiveComplexity.ksItemSym : ksSOLang.Relations 1

The item symbol over the sum.

Equations

• DescriptiveComplexity.ksItemSym = Sum.inl FirstOrder.Language.bwItem

def DescriptiveComplexity.ksCarryRel : knapsackGuessBlock.lang.Relations 2

The carry relation variable.

Equations

• DescriptiveComplexity.ksCarryRel = ⟨DescriptiveComplexity.KnapsackGuessBlockIx.carry, DescriptiveComplexity.ksCarryRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.ksLeSym : ksSOLang.Relations 2

The le symbol over the sum.

Equations

• DescriptiveComplexity.ksLeSym = Sum.inl FirstOrder.Language.bwLe

def DescriptiveComplexity.ksSelRel : knapsackGuessBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.ksSelRel = ⟨DescriptiveComplexity.KnapsackGuessBlockIx.sel, DescriptiveComplexity.ksSelRel._proof_1⟩

@[instance_reducible]

instance DescriptiveComplexity.instFintypeKnapsackGuessBlockIx : Fintype KnapsackGuessBlockIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.ksSOLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.ksSOLang = FirstOrder.Language.binWeights.sum DescriptiveComplexity.knapsackGuessBlock.lang

Formula builders

def DescriptiveComplexity.kItemF {α : Type} (x : α) : ksSOLang.Formula α

x is an item, as a formula.

Equations

• DescriptiveComplexity.kItemF x = DescriptiveComplexity.ksItemSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.kPosnF {α : Type} (x : α) : ksSOLang.Formula α

x is a bit position, as a formula.

Equations

• DescriptiveComplexity.kPosnF x = DescriptiveComplexity.ksPosnSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.kBitF {α : Type} (i p : α) : ksSOLang.Formula α

The weight of i has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.kBitF i p = DescriptiveComplexity.ksBitSym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var p)

def DescriptiveComplexity.kTgtF {α : Type} (p : α) : ksSOLang.Formula α

The target has bit 1 at p, as a formula.

Equations

• DescriptiveComplexity.kTgtF p = DescriptiveComplexity.ksTgtSym.formula₁ (FirstOrder.Language.var p)

def DescriptiveComplexity.kLeF {α : Type} (x y : α) : ksSOLang.Formula α

x ≤ y, as a formula.

Equations

• DescriptiveComplexity.kLeF x y = DescriptiveComplexity.ksLeSym.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

def DescriptiveComplexity.kSelF {α : Type} (x : α) : ksSOLang.Formula α

x is chosen, as a formula.

Equations

• DescriptiveComplexity.kSelF x = DescriptiveComplexity.ksSelSym.formula₁ (FirstOrder.Language.var x)

def DescriptiveComplexity.kPSF {α : Type} (i p : α) : ksSOLang.Formula α

Bit p of the running total at i, as a formula.

Equations

• DescriptiveComplexity.kPSF i p = DescriptiveComplexity.ksPSSym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var p)

def DescriptiveComplexity.kCarryF {α : Type} (i p : α) : ksSOLang.Formula α

The carry at p of the step appending i, as a formula.

Equations

• DescriptiveComplexity.kCarryF i p = DescriptiveComplexity.ksCarrySym.formula₂ (FirstOrder.Language.var i) (FirstOrder.Language.var p)

def DescriptiveComplexity.kEqF {α : Type} (x y : α) : ksSOLang.Formula α

x = y, as a formula.

Equations

• DescriptiveComplexity.kEqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

def DescriptiveComplexity.kAddF {α : Type} (i p : α) : ksSOLang.Formula α

The bit that the item i contributes at p: its weight's bit, if it is chosen.

Equations

• DescriptiveComplexity.kAddF i p = DescriptiveComplexity.kSelF i ⊓ DescriptiveComplexity.kBitF i p

def DescriptiveComplexity.kXor3F {α : Type} (x y z : ksSOLang.Formula α) : ksSOLang.Formula α

The exclusive or of three formulas, as x ↔ (y ↔ z).

Equations

• DescriptiveComplexity.kXor3F x y z = x.iff (y.iff z)

def DescriptiveComplexity.kMaj3F {α : Type} (x y z : ksSOLang.Formula α) : ksSOLang.Formula α

The majority of three formulas.

Equations

• DescriptiveComplexity.kMaj3F x y z = x ⊓ y ⊔ (x ⊓ z ⊔ y ⊓ z)

noncomputable def DescriptiveComplexity.kMinItemF {α : Type} (i : α) : ksSOLang.Formula α

i is the first item, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.kMaxItemF {α : Type} (i : α) : ksSOLang.Formula α

i is the last item, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.kSuccItemF {α : Type} (i j : α) : ksSOLang.Formula α

j is the item right after i, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.kMinPosnF {α : Type} (p : α) : ksSOLang.Formula α

p is the lowest position, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.kMaxPosnF {α : Type} (p : α) : ksSOLang.Formula α

p is the highest position, as a formula.

Equations

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

noncomputable def DescriptiveComplexity.kSuccPosnF {α : Type} (p q : α) : ksSOLang.Formula α

q is the position right above p, as a formula.

Equations

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

The clauses

noncomputable def DescriptiveComplexity.knapsackKernel : ksSOLang.Sentence

The first-order kernel of the Σ₁ definition of Knapsack.

Equations

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

Realization

Membership

theorem DescriptiveComplexity.knapsack_sigmaSODefinable : SigmaSODefinable 1 Knapsack

Knapsack is Σ₁-definable: guess the chosen items, the running totals and the carries, and check first-order that each step is a ripple-carry addition whose last total is the target. Since NP is defined as Σ₁-definability, this is the membership half of the NP-completeness of Knapsack.