Subset sum

DefinitionAttainable sums in exact subset sum#✓fully proved

Given a list \(x = (x_1, \dots, x_n)\) of natural numbers and a target \(t \in \mathbb{N}\), this timed procedure starts from the list \(L_0 = (0)\) and, for \(i = 1, \dots, n\) in order, forms \(L_i\) from \(L_{i-1}\) in four steps: add \(x_i\) to every entry of \(L_{i-1}\); merge \(L_{i-1}\) with this shifted list (the standard merge of two lists, comparing entries with \(\le\)); delete adjacent repeated values; and keep only the values at most \(t\). It returns \(L_n\). The counted events are the initial assignment and, in each phase, one event per addition, one per merge comparison, one per comparison of adjacent values, one per comparison with \(t\), and one for the phase assignment.

public def exactSubsetSumSums (xs : List Nat) (target : Nat) :
    TimeM Nat (List Nat) := do
  TimeM.tick 1
  xs.foldlM (fun saved x => do
    let shifted ← saved.mapM fun z => do
      TimeM.tick 1
      pure (z + x)
    let merged ← TimeM.merge saved shifted
    let unique ← adjacent merged
    let feasible ← unique.filterM fun z => do
      TimeM.tick 1
      pure (decide (z ≤ target))
    TimeM.tick 1
    pure feasible) [0]

Used by 14

Used byExact subset sum procedure · Optimality of exact subset sum · Exact subset sum returns the maximum of the computed sums · The number of computed sums is at most two to the power of the input length · The number of computed sums is at most the input total plus one · The number of computed sums is at most the target plus one · Characterization of the exact subset sum list · Prefixes of the powers of two attain every sum · The exact subset sum list is strictly increasing · Zero is always a computed sum · Event count of exact subset sum · Exponential lower bound for exact subset sum on powers of two · Exponential upper bound for exact subset sum · Pseudo-polynomial bound for exact subset sum

TheoremCharacterization of the exact subset sum list#✓fully proved

Let \(x\) be a list of natural numbers, \(t\) a natural number, and \(L\) the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\). A natural number \(z\) belongs to \(L\) if and only if \(z \le t\) and \(z\) is the sum of some sublist of \(x\) (a subsequence, not necessarily contiguous).

public theorem exactSubsetSumSums_mem (xs : List Nat) (target z : Nat) :
    z ∈ (exactSubsetSumSums xs target).ret ↔
      z ≤ target ∧ ∃ ys : List Nat, ys.Sublist xs ∧ ys.sum = z

Uses 1 · Used by 6

Statement usesAttainable sums in exact subset sum

Used byOptimality of exact subset sum · The number of computed sums is at most two to the power of the input length · The number of computed sums is at most the input total plus one · The number of computed sums is at most the target plus one · Prefixes of the powers of two attain every sum · Zero is always a computed sum

TheoremZero is always a computed sum#✓fully proved

For every list \(x\) of natural numbers and every natural number \(t\), the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\) contains \(0\).

public theorem exactSubsetSumSums_zero_mem (xs : List Nat) (target : Nat) :
    0 ∈ (exactSubsetSumSums xs target).ret

Uses 2 · Used by 1

Statement usesAttainable sums in exact subset sum

Proof usesCharacterization of the exact subset sum list

Used byOptimality of exact subset sum

TheoremThe exact subset sum list is strictly increasing#✓fully proved

For every list \(x\) of natural numbers and every natural number \(t\), the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\) is strictly increasing; in particular it has no repeated entries.

public theorem exactSubsetSumSums_sorted (xs : List Nat) (target : Nat) :
    (exactSubsetSumSums xs target).ret.Pairwise (· < ·)

Uses 1 · Used by 4

Statement usesAttainable sums in exact subset sum

Used byThe number of computed sums is at most two to the power of the input length · The number of computed sums is at most the input total plus one · The number of computed sums is at most the target plus one · Prefixes of the powers of two attain every sum

TheoremThe number of computed sums is at most two to the power of the input length#✓fully proved

For every list \(x\) of natural numbers, of length \(n\), and every natural number \(t\), the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\) has length at most \(2^n\).

public theorem exactSubsetSumSums_length_le_pow (xs : List Nat) (target : Nat) :
    (exactSubsetSumSums xs target).ret.length ≤ 2 ^ xs.length

Uses 3 · Used by 1

Statement usesAttainable sums in exact subset sum

Proof usesCharacterization of the exact subset sum list · The exact subset sum list is strictly increasing

Used byExponential upper bound for exact subset sum

TheoremThe number of computed sums is at most the target plus one#✓fully proved

For every list \(x\) of natural numbers and every natural number \(t\), the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\) has length at most \(t + 1\).

public theorem exactSubsetSumSums_length_le_target (xs : List Nat) (target : Nat) :
    (exactSubsetSumSums xs target).ret.length ≤ target + 1

Uses 3 · Used by 1

Statement usesAttainable sums in exact subset sum

Proof usesCharacterization of the exact subset sum list · The exact subset sum list is strictly increasing

Used byPseudo-polynomial bound for exact subset sum

TheoremThe number of computed sums is at most the input total plus one#✓fully proved

For every list \(x\) of natural numbers with sum \(S\) and every natural number \(t\), the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\) has length at most \(S + 1\).

public theorem exactSubsetSumSums_length_le_sum (xs : List Nat) (target : Nat) :
    (exactSubsetSumSums xs target).ret.length ≤ xs.sum + 1

Uses 3 · Used by 1

Statement usesAttainable sums in exact subset sum

Proof usesCharacterization of the exact subset sum list · The exact subset sum list is strictly increasing

Used byPseudo-polynomial bound for exact subset sum

TheoremPrefixes of the powers of two attain every sum#✓fully proved

Let \(i \le n\) be natural numbers. On the list \(1, 2, 4, \dots, 2^{i-1}\) (the first \(i\) entries of \(1, 2, \dots, 2^{n-1}\)) with target \(2^n - 1\), the final list of sums computed by the exact subset sum traversal is exactly \(0, 1, 2, \dots, 2^i - 1\) in increasing order.

public theorem exactSubsetSumSums_powers_of_two (n i : Nat) (hi : i ≤ n) :
    (exactSubsetSumSums (((List.range n).map (fun j => 2 ^ j)).take i)
      (2 ^ n - 1)).ret = List.range (2 ^ i)

Uses 3 · Used by 1

Statement usesAttainable sums in exact subset sum

Proof usesCharacterization of the exact subset sum list · The exact subset sum list is strictly increasing

Used byExponential lower bound for exact subset sum on powers of two

DefinitionExact subset sum procedure#✓fully proved

Given a list \(x\) of natural numbers and a target \(t \in \mathbb{N}\), the procedure first computes the list \(L = (\ell_1, \dots, \ell_m)\) of attainable sums of \(x\) with target \(t\), then scans it from left to right, keeping a running maximum that starts at \(0\), and returns \(\max(0, \ell_1, \dots, \ell_m)\). Its counted events are those of computing \(L\) plus one per entry of \(L\).

public def exactSubsetSum (xs : List Nat) (target : Nat) : TimeM Nat Nat := do
  let sums ← exactSubsetSumSums xs target
  sums.foldlM (fun best z => do
    TimeM.tick 1
    pure (max best z)) 0

Uses 1 · Used by 9

Statement usesAttainable sums in exact subset sum

Used byOptimality of exact subset sum · Optimality of exact subset sum for distinct positive inputs · Exact subset sum returns the maximum of the computed sums · Event count of exact subset sum · Exponential lower bound for exact subset sum on powers of two · Exponential upper bound for exact subset sum · Pseudo-polynomial bound for exact subset sum · Polynomial event bound for exact subset sum with a polynomially bounded target · Polynomial event bound for exact subset sum with polynomially bounded inputs

TheoremExact subset sum returns the maximum of the computed sums#✓fully proved

For every list \(x\) of natural numbers and every natural number \(t\), the value returned by the exact subset sum algorithm on \(x\) with target \(t\) equals \(\max(\cdots\max(\max(0, s_1), s_2)\cdots, s_k)\), where \(s_1, \dots, s_k\) is the final list of sums computed by the exact subset sum traversal on \(x\) with target \(t\).

public theorem exactSubsetSum_ret (xs : List Nat) (target : Nat) :
    (exactSubsetSum xs target).ret =
      (exactSubsetSumSums xs target).ret.foldl max 0

Uses 2 · Used by 1

Statement usesExact subset sum procedure · Attainable sums in exact subset sum

Used byOptimality of exact subset sum

TheoremEvent count of exact subset sum#✓fully proved

Let \(x = (x_1, \dots, x_n)\) be a list of natural numbers and \(t \in \mathbb{N}\) a target. For \(0 \le i \le n\) let \(L_i\) be the list of attainable sums of the prefix \((x_1, \dots, x_i)\) with target \(t\). For \(i < n\) let \(M_i\) be the merge of \(L_i\) with the list obtained by adding \(x_{i+1}\) to every entry of \(L_i\), let \(c_i\) be the number of comparisons this merge makes, and let \(D_i\) be \(M_i\) with adjacent repeated values deleted. Then the number of counted events of the exact subset-sum procedure on \(x\) and \(t\) is

\[1 + n + \sum_{i=0}^{n-1} \bigl(|L_i| + c_i + (|M_i| - 1) + |D_i|\bigr) + |L_n|,\]

where \(|\cdot|\) denotes length and \(|M_i| - 1\) is truncated subtraction of natural numbers.

public theorem exactSubsetSum_time (xs : List Nat) (target : Nat) :
    (exactSubsetSum xs target).time = 1 + xs.length +
      ((List.range xs.length).map fun i =>
        let saved := (exactSubsetSumSums (xs.take i) target).ret
        let merged := TimeM.merge saved (saved.map (fun z => z + xs.getD i 0))
        saved.length + merged.time + (merged.ret.length - 1) +
          (merged.ret.destutter (· ≠ ·)).length).sum +
      (exactSubsetSumSums xs target).ret.length

Uses 2 · Used by 1

Statement usesExact subset sum procedure · Attainable sums in exact subset sum

Used byExponential lower bound for exact subset sum on powers of two

TheoremExponential lower bound for exact subset sum on powers of two#✓fully proved

For every \(n \in \mathbb{N}\), the exact subset-sum procedure on the list \((2^0, 2^1, \dots, 2^{n-1})\) (empty when \(n = 0\)) with target \(2^n - 1\) makes at least \(2^n - 1\) counted events.

public theorem exactSubsetSum_time_ge_powers_of_two (n : Nat) :
    2 ^ n - 1 ≤
      (exactSubsetSum ((List.range n).map (fun j => 2 ^ j)) (2 ^ n - 1)).time

Uses 4

Statement usesExact subset sum procedure

Proof usesAttainable sums in exact subset sum · Prefixes of the powers of two attain every sum · Event count of exact subset sum

TheoremExponential upper bound for exact subset sum#✓fully proved

For every list \(x\) of \(n\) natural numbers and every target \(t \in \mathbb{N}\), the exact subset-sum procedure on \(x\) and \(t\) makes at most \(1 + n + 7(2^n - 1) + 2^n\) counted events.

public theorem exactSubsetSum_time_le_exponential (xs : List Nat) (target : Nat) :
    (exactSubsetSum xs target).time ≤
      1 + xs.length + 7 * (2 ^ xs.length - 1) + 2 ^ xs.length

Uses 3

Statement usesExact subset sum procedure

Proof usesAttainable sums in exact subset sum · The number of computed sums is at most two to the power of the input length

TheoremPseudo-polynomial bound for exact subset sum#✓fully proved

For every list \(x\) of \(n\) natural numbers with sum \(s\) and every target \(t \in \mathbb{N}\), the exact subset-sum procedure on \(x\) and \(t\) makes at most \(1 + n + (7n + 1)\min(t + 1, s + 1)\) counted events.

public theorem exactSubsetSum_time_le_numeric (xs : List Nat) (target : Nat) :
    (exactSubsetSum xs target).time ≤ 1 + xs.length +
      (7 * xs.length + 1) * min (target + 1) (xs.sum + 1)

Uses 4 · Used by 2

Statement usesExact subset sum procedure

Proof usesAttainable sums in exact subset sum · The number of computed sums is at most the input total plus one · The number of computed sums is at most the target plus one

Used byPolynomial event bound for exact subset sum with a polynomially bounded target · Polynomial event bound for exact subset sum with polynomially bounded inputs

TheoremPolynomial event bound for exact subset sum with a polynomially bounded target#✓fully proved

Let \(x\) be a list of \(n\) natural numbers and let \(t, d \in \mathbb{N}\) with \(t \le n^d\). Then the exact subset-sum procedure on \(x\) and \(t\) makes at most \(1 + n + (7n + 1)(n^d + 1)\) counted events.

public theorem exactSubsetSum_time_le_of_target_le_pow (xs : List Nat) (target d : Nat)
    (ht : target ≤ xs.length ^ d) :
    (exactSubsetSum xs target).time ≤ 1 + xs.length +
      (7 * xs.length + 1) * (xs.length ^ d + 1)

Uses 2

Statement usesExact subset sum procedure

Proof usesPseudo-polynomial bound for exact subset sum

TheoremPolynomial event bound for exact subset sum with polynomially bounded inputs#✓fully proved

Let \(x\) be a list of \(n\) natural numbers and let \(d \in \mathbb{N}\) be such that every entry of \(x\) is at most \(n^d\). Then for every target \(t \in \mathbb{N}\) the exact subset-sum procedure on \(x\) and \(t\) makes at most \(1 + n + (7n + 1)(n \cdot n^d + 1)\) counted events.

public theorem exactSubsetSum_time_le_of_values_le_pow (xs : List Nat) (target d : Nat)
    (hx : ∀ x ∈ xs, x ≤ xs.length ^ d) :
    (exactSubsetSum xs target).time ≤ 1 + xs.length +
      (7 * xs.length + 1) * (xs.length * xs.length ^ d + 1)

Uses 2

Statement usesExact subset sum procedure

Proof usesPseudo-polynomial bound for exact subset sum

TheoremOptimality of exact subset sum#✓fully proved

Let \(x\) be a list of natural numbers, \(t\) a natural number, and \(r\) the value returned by the exact subset sum algorithm on \(x\) with target \(t\). Then \(r\) is the sum of some sublist of \(x\) (a subsequence, not necessarily contiguous), \(r \le t\), and every sublist of \(x\) whose sum is at most \(t\) has sum at most \(r\).

The entries of \(x\) may be zero or repeated.

public theorem exactSubsetSum_optimal (xs : List Nat) (target : Nat) :
    (∃ ys : List Nat, ys.Sublist xs ∧ ys.sum = (exactSubsetSum xs target).ret) ∧
      (exactSubsetSum xs target).ret ≤ target ∧
      ∀ ys : List Nat, ys.Sublist xs → ys.sum ≤ target →
        ys.sum ≤ (exactSubsetSum xs target).ret

Uses 5 · Used by 1

Statement usesExact subset sum procedure

Proof usesAttainable sums in exact subset sum · Characterization of the exact subset sum list · Zero is always a computed sum · Exact subset sum returns the maximum of the computed sums

Used byOptimality of exact subset sum for distinct positive inputs

TheoremOptimality of exact subset sum for distinct positive inputs#✓fully proved

Let \(x\) be a list of distinct positive natural numbers, \(t\) a positive natural number, and \(r\) the value returned by the exact subset sum algorithm on \(x\) with target \(t\). Then \(r\) is the sum of some sublist of \(x\) (a subsequence, not necessarily contiguous), \(r \le t\), and every sublist of \(x\) whose sum is at most \(t\) has sum at most \(r\).

These are the hypotheses of CLRS, Section 35.5; the proof does not use them.

public theorem exactSubsetSum_optimal_of_positive (xs : List Nat) (target : Nat)
    (_hd : xs.Nodup) (_hp : ∀ x ∈ xs, 0 < x) (_ht : 0 < target) :
    (∃ ys : List Nat, ys.Sublist xs ∧ ys.sum = (exactSubsetSum xs target).ret) ∧
      (exactSubsetSum xs target).ret ≤ target ∧
      ∀ ys : List Nat, ys.Sublist xs → ys.sum ≤ target →
        ys.sum ≤ (exactSubsetSum xs target).ret

Uses 2

Statement usesExact subset sum procedure

Proof usesOptimality of exact subset sum

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.