Binary-weighted instances, and Karp's Knapsack

This file opens the binary encoding of DescriptiveComplexity.Numbers.BinRel, the one the last four problems of Karp's list need: numbers that must be exponential in the size of the instance, hence written in binary. Under the unary encoding of DescriptiveComplexity.Numbers.Unary these problems are solvable in polynomial time by dynamic programming, so they are simply not NP-hard there – the representation is not a detail of the encoding but part of the statement.

The vocabulary

FirstOrder.Language.binWeights carries

• item and posn, the items and the bit positions;
• bit i p, “the weight of the item i has bit 1 at the position p”;
• tgt p, the bits of the target;
• le, a linear order – on the positions it fixes the place values, and on the items it is what the Σ₁ definition walks along when it verifies the arithmetic.

Being a linear order is not automatic for a relation symbol, so it is folded into the yes-instances (DescriptiveComplexity.IsLinOrd), exactly as 3SAT folds its width bound in.

The decoding

DescriptiveComplexity.bitRank is the rank of a position – how many positions lie strictly below it – and DescriptiveComplexity.binNum decodes a set of positions as ∑ 2 ^ rank. Both are defined for an arbitrary relation Le, with no well-formedness assumption, which keeps them total and makes isomorphism-invariance a plain transport statement; when Le is a linear order they agree with DescriptiveComplexity.binValue of the numbers layer.

The sum ranges over a set rather than a Finset, via finsum, so that no finiteness assumption is needed to state the value; on an infinite universe it is 0, which no yes-instance ever looks at since finiteness is part of the problem.

inductive FirstOrder.Language.binWeightsRel : ℕ → Type

Relation symbols of binary-weighted instances.

• item : binWeightsRel 1

  item i: i is an item.

• posn : binWeightsRel 1

  posn p: p is a bit position.

• bit : binWeightsRel 2

  bit i p: the weight of i has bit 1 at position p.

• tgt : binWeightsRel 1

  tgt p: the target has bit 1 at position p.

• le : binWeightsRel 2

  le a b: the linear order carrying the place values.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqBinWeightsRel {a✝ : ℕ} : DecidableEq (binWeightsRel a✝)

Equations

• FirstOrder.Language.instDecidableEqBinWeightsRel = FirstOrder.Language.instDecidableEqBinWeightsRel.decEq

def FirstOrder.Language.instDecidableEqBinWeightsRel.decEq {a✝ : ℕ} (x✝ x✝¹ : binWeightsRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

def FirstOrder.Language.binWeights : Language

The relational language of binary-weighted instances: items and bit positions, the bits of each item's weight and of the target, and a linear order.

Equations

• FirstOrder.Language.binWeights = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.binWeightsRel }

instance FirstOrder.Language.instIsRelationalBinWeights : Language.binWeights.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.bwItem : Language.binWeights.Relations 1

The item symbol.

Equations

• FirstOrder.Language.bwItem = FirstOrder.Language.binWeightsRel.item

@[reducible, inline]

abbrev FirstOrder.Language.bwPosn : Language.binWeights.Relations 1

The position symbol.

Equations

• FirstOrder.Language.bwPosn = FirstOrder.Language.binWeightsRel.posn

@[reducible, inline]

abbrev FirstOrder.Language.bwBit : Language.binWeights.Relations 2

The bit symbol.

Equations

• FirstOrder.Language.bwBit = FirstOrder.Language.binWeightsRel.bit

@[reducible, inline]

abbrev FirstOrder.Language.bwTgt : Language.binWeights.Relations 1

The target symbol.

Equations

• FirstOrder.Language.bwTgt = FirstOrder.Language.binWeightsRel.tgt

@[reducible, inline]

abbrev FirstOrder.Language.bwLe : Language.binWeights.Relations 2

The order symbol.

Equations

• FirstOrder.Language.bwLe = FirstOrder.Language.binWeightsRel.le

The shorthands of the vocabulary

def DescriptiveComplexity.BWItem {A : Type} [FirstOrder.Language.binWeights.Structure A] (a : A) : Prop

Being an item.

Equations

• DescriptiveComplexity.BWItem a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bwItem ![a]

def DescriptiveComplexity.BWPosn {A : Type} [FirstOrder.Language.binWeights.Structure A] (a : A) : Prop

Being a bit position.

Equations

• DescriptiveComplexity.BWPosn a = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bwPosn ![a]

def DescriptiveComplexity.BWBit {A : Type} [FirstOrder.Language.binWeights.Structure A] (i p : A) : Prop

The bit of an item's weight at a position.

Equations

• DescriptiveComplexity.BWBit i p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bwBit ![i, p]

def DescriptiveComplexity.BWTgt {A : Type} [FirstOrder.Language.binWeights.Structure A] (p : A) : Prop

The bits of the target.

Equations

• DescriptiveComplexity.BWTgt p = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bwTgt ![p]

def DescriptiveComplexity.BWLe {A : Type} [FirstOrder.Language.binWeights.Structure A] (a b : A) : Prop

The order carrying the place values.

Equations

• DescriptiveComplexity.BWLe a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.bwLe ![a, b]

noncomputable def DescriptiveComplexity.BWWeight {A : Type} [FirstOrder.Language.binWeights.Structure A] (i : A) : ℕ

The weight of an item, decoded.

Equations

• DescriptiveComplexity.BWWeight i = DescriptiveComplexity.binNum DescriptiveComplexity.BWLe DescriptiveComplexity.BWPosn (DescriptiveComplexity.BWBit i)

noncomputable def DescriptiveComplexity.BWTarget (A : Type) [FirstOrder.Language.binWeights.Structure A] : ℕ

The target of a binary-weighted instance, decoded.

Equations

• DescriptiveComplexity.BWTarget A = DescriptiveComplexity.binNum DescriptiveComplexity.BWLe DescriptiveComplexity.BWPosn DescriptiveComplexity.BWTgt

The problem

def DescriptiveComplexity.HasSubsetSum (A : Type) [FirstOrder.Language.binWeights.Structure A] : Prop

A binary-weighted instance is a yes-instance of Knapsack when its order is a linear order and some set of items has weights summing exactly to the target. (Karp's KNAPSACK is this subset-sum question.)

Equations

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

theorem DescriptiveComplexity.hasSubsetSum_iso {A B : Type} [FirstOrder.Language.binWeights.Structure A] [FirstOrder.Language.binWeights.Structure B] (e : FirstOrder.Language.binWeights.Equiv A B) : HasSubsetSum A ↔ HasSubsetSum B

Being a yes-instance of Knapsack is isomorphism-invariant.

def DescriptiveComplexity.Knapsack : DecisionProblem FirstOrder.Language.binWeights

KNAPSACK, as a problem on binary-weighted instances: is there a set of items whose weights sum exactly to the target? The weights are written in binary, which is what makes the problem NP-hard rather than polynomial-time.

Equations

• DescriptiveComplexity.Knapsack = { Holds := fun (A : Type) (inst : FirstOrder.Language.binWeights.Structure A) => DescriptiveComplexity.HasSubsetSum A, iso_invariant := ⋯ }