Reference · Algorithm guarantees

rainbow.algorithms.proofs.simulated-annealing

Algorithm guaranteessrc/rainbow/algorithms/proofs/simulated_annealing.clj2 definitions, 4 theorems

AHoF O40 Simulated Annealing: the geometric temperature schedule and the deterministic (greedy-limit) Metropolis acceptance. The temperature cools by a constant rational factor each iteration, `T' = alpha * T` (exact nonnegative rational multiplication), and a candidate is accepted when it does not worsen the cost, `accept? = candidate-cost <= current-cost` (the decidable rational comparison). This reuses the exact-rational arithmetic and decidable comparison engines rather than the vector cone, so its structure is a scalar schedule plus a decision, not a vector update. The full Metropolis criterion accepts an uphill move with probability exp(-delta / T); that exponential is not exact-rational, so the probabilistic branch stays an executable-only concern and what is proved here is the cooling schedule and the deterministic acceptance. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.simulated-annealing` prints this classification.

annealing/cool :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

annealing/accept-better? :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

annealing/cool-unfold :
  (alpha temperature : ℚ≥0)
  → annealing/cool alpha temperature = alpha · temperature

annealing/accept-unfold :
  (candidate current : ℚ≥0)
  → failmon/safe? candidate current = audit/decide-nnrat-at-most candidate current

annealing/accept-better-example :
  → failmon/safe? 1 2 = data/true

annealing/reject-worse-example :
  → failmon/safe? 2 1 = data/false