Reference · Algorithm guarantees

rainbow.algorithms.proofs.penalty-method

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

AHoF O48 Penalty Method: the transform that turns a constrained problem into an unconstrained one by folding a penalty on constraint violation into the objective: augmented(x) = objective(x) + rho * penalty(x) where rho is the penalty weight and penalty(x) measures constraint violation (zero when feasible). This is exact-rational multiplication and addition; the constraint functions and the outer schedule that grows rho are the executable concern. What is proved is the augmented-objective recurrence and worked instances: with a feasible point (penalty 0) the augmented value equals the objective, and an infeasible point adds the weighted violation. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 1 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.penalty-method` prints this classification.

penalty/augmented :
  (x₁ x₂ x₃ : ℚ≥0)
  → ℚ≥0

penalty/augmented-unfold :
  (objective rho penalty : ℚ≥0)
  → penalty/augmented objective rho penalty = objective + rho · penalty

penalty/infeasible-example :
  → penalty/augmented 1 2 3 = 7

penalty/feasible-example :
  → penalty/augmented 5 2 0 = 5