Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.hungarian

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

AHoF Hungarian Algorithm (Kuhn-Munkres): find a minimum-cost perfect assignment of n agents to n tasks in O(n^3) -- the exact solver for the assignment problem (job scheduling, tracking, matching). It repeatedly subtracts row and column minima to expose ZERO reduced costs and searches for a perfect matching among those tight cells, adjusting when none exists. A cell is a candidate for the assignment exactly when its reduced cost has reached zero (is tight): tight? reduced-cost = decide (reduced-cost <= 0) over exact-rational reduced costs (which are non-negative after each reduction, so <= 0 means exactly 0). Proved native and axiom-free: the tightness test; that a zero-reduced-cost cell is tight (assignable); the certificate that a tight cell's reduced cost is at most zero, hence exactly zero (native nnrat/at-most) -- so it incurs no extra cost over the reduced optimum; and that a positive reduced cost is not yet tight. The row/column reductions and augmenting search are executable; what is proved is the tight-cell decision. Requires nnrat/at-most, audit/decide-nnrat-at-most, nnrat/decide-at-most-true-sound (all 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.hungarian` prints this classification.

hungarian/tight? :
  (x₁ : ℚ≥0)
  → data/Bool

hungarian/zero-reduced-cost-tight :
  → hungarian/tight? 0 = data/true

hungarian/tight-cost-zero :
  → 0 ≤ 0

hungarian/positive-cost-not-tight :
  → hungarian/tight? 3 = data/false