Reference · Algorithm guarantees

rainbow.algorithms.proofs.branch-and-bound

Algorithm guaranteessrc/rainbow/algorithms/proofs/branch_and_bound.clj1 definitions, 3 theorems

AHoF D34 / O-family Branch and Bound: the bounding test that turns exhaustive enumeration into a pruned search. A node carries an optimistic bound on the best objective reachable in its subtree; when that bound is already dominated by the incumbent (the best solution found so far), the whole subtree is pruned because it cannot contain a better solution. The pruning predicate is the decidable rational comparison dominated? bound incumbent = decide (bound <= incumbent) Proved native and axiom-free: worked instances on concrete values -- bound 3 against incumbent 5 is dominated; the worked certificate 3 <= 5 (a native `nnrat/at-most`, obtained from the decision computing to true); and bound 7 against incumbent 5 is not dominated. The branching strategy and the bound function are executable concerns; what is proved here is the pruning predicate at these instances. That pruning never discards a better solution is the classical soundness of branch and bound and is not proved here. Requires `nnrat/at-most`, `audit/decide-nnrat-at-most`, and `nnrat/decide-at-most-true-sound` in the environment (all carried by the D63 checkpoint, as used by the geometric-convergence bounds). 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.branch-and-bound` prints this classification.

branch-and-bound/dominated? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

branch-and-bound/prunes-dominated-node :
  → search/poll-improves 3 5 = data/true

branch-and-bound/pruned-bound-dominated :
  → 3 ≤ 5

branch-and-bound/explores-promising-node :
  → search/poll-improves 7 5 = data/false