Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.branch-and-bound

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/branch_and_bound.clj0 definitions, 4 theorems

AHoF D34 worked Branch and Bound pruning step over exact rationals, reusing the shared bounding lemma (rainbow.algorithms.proofs.branch-and-bound, branch-and-bound/*). A node whose optimistic bound 2 is at most the incumbent 8 is dominated, so its subtree is pruned; pruning is sound because the bound really is <= the incumbent (a native nnrat/at-most), so nothing better than the incumbent is discarded. A node whose bound 9 exceeds the incumbent 8 is not dominated and must be explored. This second catalog row is discharged by the reused general lemma. Proved native and axiom-free. Scope (measured by the kernel): this module has 4 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.branch-and-bound` prints this classification.

Depends onalgorithms.proofs.branch-and-bound

ahof-d34/prunes-weak-node :
  → bin-packing/fits? 2 8 = data/true

ahof-d34/pruning-sound :
  → 2 ≤ 8

ahof-d34/explores-strong-node :
  → bin-packing/fits? 9 8 = data/false

ahof-d34/branch-and-bound :
  → proposition/conjunction (bin-packing/fits? 2 8 = data/true) (bin-packing/fits? 9 8 = data/false)