Subset sum

SubsetSum is the set of instances x : SubsetSumInstance of a list x.numbers of natural numbers, possibly with repetitions, and a target x.target such that some sub-multiset of x.numbers sums to x.target Sipser, Section 7.3. All numbers are encoded in binary (Turing.MultiTapeTM.encNat, digits least significant first); the NP-hardness proved here is for this encoding and is not strong NP-hardness. A certificate is a mask selecting entries of x.numbers (Cslib.Complexity.maskSelect), and the verifier adds the selected numbers in binary.

Sipser's reduction from 3SAT Sipser, Theorem 7.56 gives each of the n variables of a formula, numbered by first occurrence (Cslib.Logic.PL.CNF.distinctVars), and each of its m clauses a digit position. Each variable has two literal numbers, with digit one at the position of the variable and at the positions of the clauses containing the literal (ThreeSAT.literalDigits); each clause has two slack numbers with digit one at its position only. The target has digit one at every variable position and three at every clause position. At each position, all numbers together have at most five digits one, so no subfamily produces carries in any base above five (Cslib.Complexity.sum_sum_pow_eq_iff). We use base 8 rather than Sipser's base 10, so that digits are blocks of three bits; every number has at most n + m base-8 digits (ThreeSAT.lt_of_mem_digitNumbers, ThreeSAT.digitTarget_lt). Variable labels only enter through their order of first occurrence, so large binary labels do not enlarge the numbers. A literal repeated in a clause counts once, and a clause containing both literals of a variable is covered by both of its literal numbers. Formulas with a clause of more than three literals are not in ThreeSAT and are mapped to an instance without solutions.

Main definitions

• Cslib.Complexity.SubsetSumInstance, Cslib.Complexity.SubsetSum, Cslib.Complexity.encSubsetSum, Cslib.Complexity.SubsetSum.verifier.
• Cslib.Complexity.ThreeSAT.literalDigits, Cslib.Complexity.ThreeSAT.digitNumbers, Cslib.Complexity.ThreeSAT.digitTarget.
• Cslib.Complexity.ThreeSAT.toSubsetSum: Sipser's reduction.

Main results

• Cslib.Complexity.mem_SubsetSum_iff_sublist: solutions are subsequences of the numbers.
• Cslib.Complexity.SubsetSum.isVerifier, Cslib.Complexity.SubsetSum.mem_NP: SubsetSum ∈ NP encSubsetSum.
• Cslib.Complexity.ThreeSAT.digit_mem_SubsetSum_iff_counts, Cslib.Complexity.ThreeSAT.counts_iff_satisfiable: the digit construction has a solution exactly when the digit positions can be filled, exactly when the formula is satisfiable.
• Cslib.Complexity.ThreeSAT.toSubsetSum_mem_iff: correctness of Sipser's reduction.
• Cslib.Complexity.ThreeSAT.lt_of_mem_digitNumbers, Cslib.Complexity.ThreeSAT.digitTarget_lt: the numbers have O(n + m) digits.
• Cslib.Complexity.ThreeSAT.computableInPolyTime_toSubsetSum: the reduction is polynomial-time.
• Cslib.Complexity.polyTimeReducible_ThreeSAT_SubsetSum, Cslib.Complexity.SubsetSum_npHard, Cslib.Complexity.SubsetSum_npComplete: SubsetSum is NP-complete.

References

• M. Sipser, Introduction to the Theory of Computation
• R. M. Karp, Reducibility among combinatorial problems

structure Cslib.Complexity.SubsetSumInstance : Type

An instance of subset sum: a list of candidate natural numbers and a target sum.

• numbers : List ℕ

  The candidate natural numbers, possibly with repetitions.

• target : ℕ

  The target sum.

theorem Cslib.Complexity.SubsetSumInstance.ext_iff {x y : SubsetSumInstance} : x = y ↔ x.numbers = y.numbers ∧ x.target = y.target

theorem Cslib.Complexity.SubsetSumInstance.ext {x y : SubsetSumInstance} (numbers : x.numbers = y.numbers) (target : x.target = y.target) : x = y

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqSubsetSumInstance : DecidableEq SubsetSumInstance

def Cslib.Complexity.instDecidableEqSubsetSumInstance.decEq (x✝ x✝¹ : SubsetSumInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instReprSubsetSumInstance : Repr SubsetSumInstance

def Cslib.Complexity.instReprSubsetSumInstance.repr : SubsetSumInstance → ℕ → Std.Format

theorem Cslib.Complexity.encSubsetSum_numbers_inO : Turing.MultiTapeTM.ComputableInO SubsetSumInstance.numbers encSubsetSum (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (fun (a : SubsetSumInstance) => (encSubsetSum a).length) fun (a : SubsetSumInstance) => (encSubsetSum a).length

theorem Cslib.Complexity.encSubsetSum_target_deg : Turing.MultiTapeTM.ComputableInDegree SubsetSumInstance.target encSubsetSum Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encSubsetSum_numbers_deg : Turing.MultiTapeTM.ComputableInDegree SubsetSumInstance.numbers encSubsetSum (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) 1 1

theorem Cslib.Complexity.encSubsetSum_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → List ℕ} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { numbers := x0 x, target := x1 x }) encIn encSubsetSum budget

theorem Cslib.Complexity.encSubsetSum_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : SubsetSumInstance) => (a.numbers, a.target)) encSubsetSum encSubsetSumFields 1 1

theorem Cslib.Complexity.encSubsetSum_target_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SubsetSumInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSubsetSum → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).target) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encSubsetSum_numbers_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → SubsetSumInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encSubsetSum → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).numbers) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.encSubsetSum_numbers_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SubsetSumInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encSubsetSum S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).numbers) encIn✝ (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) S✝

theorem Cslib.Complexity.encSubsetSum_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { numbers := x0 x, target := x1 x }) encIn encSubsetSum

def Cslib.Complexity.encSubsetSum : SubsetSumInstance ↪ List Bool

Instances ⟨a, t⟩ of SubsetSum: the list a, framed, each of its numbers framed, then the target t; all numbers in binary.

theorem Cslib.Complexity.encSubsetSum_target_inO : Turing.MultiTapeTM.ComputableInO SubsetSumInstance.target encSubsetSum Turing.MultiTapeTM.encNat (fun (a : SubsetSumInstance) => (encSubsetSum a).length) fun (a : SubsetSumInstance) => (encSubsetSum a).length

theorem Cslib.Complexity.encSubsetSum_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : List ℕ × ℕ) => { numbers := p.1, target := p.2 }) encSubsetSumFields encSubsetSum 1 1

theorem Cslib.Complexity.encSubsetSum_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → List ℕ} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { numbers := x0 x, target := x1 x }) encIn encSubsetSum (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encSubsetSum_target_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → SubsetSumInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encSubsetSum S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).target) encIn✝ Turing.MultiTapeTM.encNat S✝

@[reducible, inline]

abbrev Cslib.Complexity.encSubsetSumFields : List ℕ × ℕ ↪ List Bool

The tuple of the fields of encSubsetSum.

@[simp]

theorem Cslib.Complexity.encSubsetSum_apply (a : SubsetSumInstance) : encSubsetSum a = encSubsetSumFields (a.numbers, a.target)

def Cslib.Complexity.SubsetSum : Set SubsetSumInstance

The instances of subset sum: some sub-multiset of x.numbers sums to x.target [Kar72], Sipser, Chapter 7.

theorem Cslib.Complexity.mem_SubsetSum {x : SubsetSumInstance} : x ∈ SubsetSum ↔ ∃ s ≤ ↑x.numbers, s.sum = x.target

theorem Cslib.Complexity.mem_SubsetSum_iff_sublist {x : SubsetSumInstance} : x ∈ SubsetSum ↔ ∃ (s : List ℕ), s.Sublist x.numbers ∧ s.sum = x.target

Subset sum asks for a subsequence of the numbers with the target sum.

theorem Cslib.Complexity.map_mem_SubsetSum_iff {ι : Type u_1} [DecidableEq ι] {xs : List ι} (hxs : xs.Nodup) (f : ι → ℕ) (t : ℕ) : { numbers := List.map f xs, target := t } ∈ SubsetSum ↔ ∃ F ⊆ xs.toFinset, ∑ x ∈ F, f x = t

A sub-multiset of the values of a duplicate-free list sums to t exactly when a subset of the list does.

def Cslib.Complexity.SubsetSum.verifier : SubsetSumInstance × List Bool → Bool

The verifier for SubsetSum, a mask verifier (Cslib.Complexity.maskVerifier): the numbers selected by the certificate mask sum to the target.

theorem Cslib.Complexity.SubsetSum.isVerifier : IsVerifier encSubsetSum Polynomial.X verifier SubsetSum

SubsetSum.verifier verifies SubsetSum with certificates as long as the encoded instance.

theorem Cslib.Complexity.SubsetSum.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encSubsetSum Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The SubsetSum verifier is polynomial-time: it selects the masked numbers, adds them in binary and compares the sum with the target.

theorem Cslib.Complexity.SubsetSum.mem_NP : SubsetSum ∈ NP encSubsetSum

SubsetSum belongs to NP.

The digit construction

def Cslib.Complexity.ThreeSAT.covers (φ : Logic.PL.CNF ℕ) (i : ℕ) (b : Bool) (j : ℕ) : Bool

Whether clause j of φ contains the literal of sign b of variable number i of φ.distinctVars.

def Cslib.Complexity.ThreeSAT.literalDigits (φ : Logic.PL.CNF ℕ) (i : ℕ) (b : Bool) : List ℕ

The digit positions of the number of a literal: the position i of its variable, and the position φ.distinctVars.length + j of every clause j containing it.

def Cslib.Complexity.ThreeSAT.octal (ps : List ℕ) : ℕ

The number whose base-8 digits are one at the positions ps and zero elsewhere, for distinct positions.

def Cslib.Complexity.ThreeSAT.digitNumbers (φ : Logic.PL.CNF ℕ) : List ℕ

The numbers of the digit construction: two literal numbers for each variable, and two slack numbers with the single digit of each clause.

def Cslib.Complexity.ThreeSAT.digitTarget (φ : Logic.PL.CNF ℕ) : ℕ

The target of the digit construction: digit one at each variable position and digit three at each clause position.

def Cslib.Complexity.ThreeSAT.toSubsetSum (φ : Logic.PL.CNF ℕ) : SubsetSumInstance

Sipser's reduction from ThreeSAT to SubsetSum: the digit construction for formulas whose clauses have at most three literals, and an instance without solutions otherwise.

Correctness

theorem Cslib.Complexity.ThreeSAT.covers_eq_true_iff {φ : Logic.PL.CNF ℕ} {i : ℕ} {b : Bool} {j : ℕ} : covers φ i b j = true ↔ ∃ l ∈ List.getD φ j [], List.idxOf l.1 φ.distinctVars = i ∧ l.2 = b

Clause j covers the literal number (i, b) when it contains a literal of sign b whose variable is number i of φ.distinctVars.

@[reducible, inline]

abbrev Cslib.Complexity.ThreeSAT.Item : Type

The items of the digit construction: literal numbers (i, b) and slack numbers (j, c).

theorem Cslib.Complexity.ThreeSAT.lt_of_mem_digitNumbers {φ : Logic.PL.CNF ℕ} {a : ℕ} (ha : a ∈ digitNumbers φ) : a < 8 ^ (φ.distinctVars.length + List.length φ)

Size of the digit construction. Every number has at most φ.distinctVars.length + φ.length base-8 digits, that is, three binary digits per variable and per clause.

theorem Cslib.Complexity.ThreeSAT.digitTarget_lt {φ : Logic.PL.CNF ℕ} : digitTarget φ < 8 ^ (φ.distinctVars.length + List.length φ)

The target has at most φ.distinctVars.length + φ.length base-8 digits.

theorem Cslib.Complexity.ThreeSAT.digit_mem_SubsetSum_iff_counts {φ : Logic.PL.CNF ℕ} (hφ : ∀ c ∈ φ, List.length c ≤ 3) : { numbers := digitNumbers φ, target := digitTarget φ } ∈ SubsetSum ↔ ∃ A ⊆ Finset.range φ.distinctVars.length ×ˢ Finset.univ, ∃ B ⊆ Finset.range (List.length φ) ×ˢ Finset.univ, (∀ i < φ.distinctVars.length, {a ∈ A | a.1 = i}.card = 1) ∧ ∀ j < List.length φ, {a ∈ A | covers φ a.1 a.2 j = true}.card + {c ∈ B | c.1 = j}.card = 3

The digit construction in terms of column counts: a solution chooses literal numbers A and slack numbers B so that each variable position holds one chosen literal number and each clause position three chosen numbers.

theorem Cslib.Complexity.ThreeSAT.counts_iff_satisfiable {φ : Logic.PL.CNF ℕ} (hφ : ∀ c ∈ φ, List.length c ≤ 3) : (∃ A ⊆ Finset.range φ.distinctVars.length ×ˢ Finset.univ, ∃ B ⊆ Finset.range (List.length φ) ×ˢ Finset.univ, (∀ i < φ.distinctVars.length, {a ∈ A | a.1 = i}.card = 1) ∧ ∀ j < List.length φ, {a ∈ A | covers φ a.1 a.2 j = true}.card + {c ∈ B | c.1 = j}.card = 3) ↔ φ.Satisfiable

Column counts as in digit_mem_SubsetSum_iff_counts exist exactly when the formula is satisfiable: the chosen literal numbers are the true literals, and slack numbers fill each clause position up to three.

theorem Cslib.Complexity.ThreeSAT.toSubsetSum_mem_iff (φ : Logic.PL.CNF ℕ) : toSubsetSum φ ∈ SubsetSum ↔ φ ∈ ThreeSAT

Correctness of Sipser's reduction. A formula belongs to ThreeSAT exactly when its digit construction has a sub-multiset summing to the target.

Polynomial time

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_covers : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ((Logic.PL.CNF ℕ × ℕ) × Bool) × ℕ) => covers p.1.1.1 p.1.1.2 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool

Testing whether a clause contains a literal is polynomial-time.

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_literalDigits : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × ℕ) × Bool) => literalDigits p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)

Listing the digit positions of a literal number is polynomial-time.

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_literalDigits' {α : Type} {input : α ↪ List Bool} {φ : α → Logic.PL.CNF ℕ} {i : α → ℕ} {b : α → Bool} (hφ : Turing.MultiTapeTM.ComputableInPolyTime φ input encCNF) (hi : Turing.MultiTapeTM.ComputableInPolyTime i input Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime b input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => literalDigits (φ a) (i a) (b a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary)

Composition rule for literalDigits.

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_octal : Turing.MultiTapeTM.ComputableInPolyTime octal (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encNat

A number with digits zero and one is computed in binary from its unary digit positions.

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_digitNumbers : Turing.MultiTapeTM.ComputableInPolyTime digitNumbers encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

The numbers of the digit construction are computed in polynomial time.

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_digitTarget : Turing.MultiTapeTM.ComputableInPolyTime digitTarget encCNF Turing.MultiTapeTM.encNat

The target of the digit construction is computed in polynomial time.

theorem Cslib.Complexity.ThreeSAT.computableInPolyTime_toSubsetSum : Turing.MultiTapeTM.ComputableInPolyTime toSubsetSum encCNF encSubsetSum

Sipser's reduction is computable in polynomial time.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_SubsetSum : PolyTimeReducible encCNF encSubsetSum ThreeSAT SubsetSum

ThreeSAT reduces to SubsetSum in polynomial time by Sipser's digit construction.

theorem Cslib.Complexity.SubsetSum_npHard : NPHard encSubsetSum SubsetSum

SubsetSum is NP-hard.

theorem Cslib.Complexity.SubsetSum_npComplete : NPComplete encSubsetSum SubsetSum

Subset sum is NP-complete, with the numbers and the target in binary [Kar72], Sipser, Theorem 7.56.