Module optimize 

Certified SAT-based optimization. We have no native MaxSAT/ILP solver, so we minimise an integer cost the honest way: binary-search the smallest feasible cost bound, where each query is a certified decision (prove_unsat → Sat witness or RUP-Refuted). The result is a certified optimum — a witness at the optimum and a refutation at optimum−1 — not merely a value we happened to find.

feasible_at(bound) must be MONOTONE: feasible at b ⇒ feasible at b+1 (e.g. “cost ≤ b” via crate::cardinality::at_most).

Structs

MinResult

The outcome of a certified minimization.

Functions

minimize_certified

Binary-search [lo, hi] for the least bound with feasible_at(bound) satisfiable. Returns None if even hi is infeasible or a query leaves the supported fragment.