Reference · The Applied Higher-Order Functions catalogue

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

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

AHoF O72 Branch and Bound (optimization form) worked pruning step over exact rationals, reusing the shared bounding lemma (rainbow.algorithms.proofs.branch-and-bound). The optimization B&B shares D34's bounding structure: a subtree is pruned when its optimistic bound cannot beat the incumbent. Worked instance distinct from D34: a node with bound 5 against incumbent 12 is dominated -> pruned (and 5 <= 12 as a native at-most, so pruning is sound); a node with bound 15 > incumbent 12 is not dominated -> explored. 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.o72-branch-and-bound` prints this classification.

Depends onalgorithms.proofs.branch-and-bound

ahof-o72/prunes-weak-node :
  → lis/extends? 5 12 = data/true

ahof-o72/pruning-sound :
  → 5 ≤ 12

ahof-o72/explores-strong-node :
  → lis/extends? 15 12 = data/false

ahof-o72/branch-and-bound :
  → proposition/conjunction (lis/extends? 5 12 = data/true) (lis/extends? 15 12 = data/false)