Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.subset-sum

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/subset_sum.clj1 definitions, 3 theorems

AHoF Subset Sum (dynamic programming): decide whether some subset of a set of positive integers sums to a target -- the canonical (weakly) NP-complete decision problem and the kernel of the partition problem and 0/1-knapsack feasibility. The DP fills a boolean table reachable[i][s] = 'some subset of the first i items sums to s', and each cell is the OR of two branches: EXCLUDE item i (reachable without it) or INCLUDE it (target s - value[i] reachable with the earlier items): reachable? include-branch? exclude-branch? = include-branch? OR exclude-branch? over booleans. Proved native and axiom-free: the reachability cell as the boolean DISJUNCTION of the include and exclude branches (via logic/if-data over Bool -- the complement of the conjunctions used elsewhere); that either branch being reachable makes the sum reachable; and that a sum is unreachable only when BOTH branches fail. The value iteration over items and sums is executable; what is proved is the reachability OR cell. Requires data/Bool, logic/if-data (both in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.subset-sum` prints this classification.

subset-sum/reachable? :
  (x₁ x₂ : data/Bool)
  → data/Bool

subset-sum/include-branch-reachable :
  → boolean/or data/true data/false = data/true

subset-sum/exclude-branch-reachable :
  → boolean/or data/false data/true = data/true

subset-sum/both-fail-unreachable :
  → boolean/or data/false data/false = data/false