otspot_core/problem/certificate.rs
1//! Proof-carrying certificate types for solver outcomes.
2//!
3//! An [`OptimalCertificate`] can only be obtained by running [`prove_optimal`]
4//! (defined in `crate::qp::certificate`), which verifies all KKT conditions.
5//! Holding a certificate is a proof token: it is impossible to construct one
6//! without passing the full verifier.
7
8/// KKT optimality certificate — all fields private, minted only by [`prove_optimal`].
9///
10/// Construction is only possible via the `pub(crate) new` method called from
11/// `crate::qp::certificate::prove_optimal`. External code cannot build this
12/// struct directly, eliminating the "proof-less Optimal" anti-pattern.
13#[derive(Debug, Clone)]
14pub struct OptimalCertificate {
15 stationarity_rel: f64,
16 primal_residual_rel: f64,
17 bound_violation: f64,
18 complementarity_rel: f64,
19 dual_sign_violation: f64,
20 duality_gap_rel: f64,
21 tol: f64,
22}
23
24impl OptimalCertificate {
25 /// Internal constructor — only `crate::qp::certificate::prove_optimal` calls this.
26 pub(crate) fn new(
27 stationarity_rel: f64,
28 primal_residual_rel: f64,
29 bound_violation: f64,
30 complementarity_rel: f64,
31 dual_sign_violation: f64,
32 duality_gap_rel: f64,
33 tol: f64,
34 ) -> Self {
35 Self {
36 stationarity_rel,
37 primal_residual_rel,
38 bound_violation,
39 complementarity_rel,
40 dual_sign_violation,
41 duality_gap_rel,
42 tol,
43 }
44 }
45
46 /// Componentwise relative stationarity: `max_j |Qx+c+Aᵀy+z|_j / scale_j`.
47 pub fn stationarity_rel(&self) -> f64 { self.stationarity_rel }
48
49 /// Componentwise relative primal violation: `max_i viol_i / scale_i`.
50 pub fn primal_residual_rel(&self) -> f64 { self.primal_residual_rel }
51
52 /// Primal bound violation: `max_j max(lb_j−x_j, x_j−ub_j, 0) / scale_j`.
53 pub fn bound_violation(&self) -> f64 { self.bound_violation }
54
55 /// Complementarity: `max(|y_i · slack_i|, |z_j · (x_j−bnd_j)|) / normaliser`.
56 pub fn complementarity_rel(&self) -> f64 { self.complementarity_rel }
57
58 /// Dual-sign violation: `max_k viol_k / (1 + |v_k|)` over sign-constrained duals.
59 pub fn dual_sign_violation(&self) -> f64 { self.dual_sign_violation }
60
61 /// Relative duality gap: `|p_obj − d_obj| / max(|p|, |d|, 1)`.
62 pub fn duality_gap_rel(&self) -> f64 { self.duality_gap_rel }
63
64 /// Tolerance used when the certificate was issued.
65 pub fn tol(&self) -> f64 { self.tol }
66}
67
68/// Reason why [`prove_optimal`] failed to issue an [`OptimalCertificate`].
69///
70/// Contains the observed residuals and the names of the conditions that exceeded `tol`.
71#[derive(Debug, Clone)]
72pub struct NotProven {
73 /// Stationarity residual observed.
74 pub stationarity_rel: f64,
75 /// Primal residual observed.
76 pub primal_residual_rel: f64,
77 /// Bound violation observed.
78 pub bound_violation: f64,
79 /// Complementarity residual observed.
80 pub complementarity_rel: f64,
81 /// Dual-sign violation observed.
82 pub dual_sign_violation: f64,
83 /// Duality-gap residual observed.
84 pub duality_gap_rel: f64,
85 /// Tolerance against which residuals were compared.
86 pub tol: f64,
87 /// Names of conditions that exceeded `tol`.
88 pub failing_conditions: Vec<&'static str>,
89}
90
91/// Branch-and-bound gap certificate — minted only by the B&B driver when:
92/// - No region was abandoned due to a non-Optimal relaxation (`proof_uncertain == false`).
93/// - `(incumbent_obj - lower_bound) / max(1, |incumbent_obj|) ≤ gap_tol`.
94///
95/// Holding this value is a proof token: the incumbent is within `gap_tol` of the global
96/// optimum. External code cannot construct it (constructor is `pub(crate)`).
97#[derive(Debug, Clone)]
98pub struct BoundGapCertificate {
99 incumbent_obj: f64,
100 lower_bound: f64,
101 gap_rel: f64,
102 gap_tol: f64,
103}
104
105impl BoundGapCertificate {
106 pub(crate) fn new(incumbent_obj: f64, lower_bound: f64, gap_rel: f64, gap_tol: f64) -> Self {
107 Self { incumbent_obj, lower_bound, gap_rel, gap_tol }
108 }
109
110 /// Best integer-feasible objective found by the search.
111 pub fn incumbent_obj(&self) -> f64 { self.incumbent_obj }
112
113 /// Authenticated lower bound on the global optimum at termination.
114 pub fn lower_bound(&self) -> f64 { self.lower_bound }
115
116 /// Relative gap: `(incumbent_obj - lower_bound) / max(1, |incumbent_obj|)`.
117 pub fn gap_rel(&self) -> f64 { self.gap_rel }
118
119 /// Tolerance against which the gap was checked when the certificate was issued.
120 pub fn gap_tol(&self) -> f64 { self.gap_tol }
121}
122
123/// Placeholder for Farkas infeasibility certificate (Phase 2+).
124#[derive(Debug, Clone)]
125pub struct FarkasCertificate;
126
127/// Placeholder for unbounded-ray certificate (Phase 2+).
128#[derive(Debug, Clone)]
129pub struct UnboundedRayCertificate;
130
131/// Typed solver outcome carrying certificates.
132///
133/// Phase 1 adds the types; existing solver entry points are not yet wired here
134/// (connection happens in Phase 2+). The enum is defined now so that downstream
135/// code can import and pattern-match against it.
136#[derive(Debug)]
137pub enum SolveOutcome {
138 /// Globally optimal (PSD Q or LP); KKT verified.
139 Optimal {
140 x: Vec<f64>,
141 y: Vec<f64>,
142 z: Vec<f64>,
143 objective: f64,
144 cert: OptimalCertificate,
145 },
146 /// KKT-point for a non-convex QP (inertia-corrected IPM converged).
147 LocalOptimal {
148 x: Vec<f64>,
149 y: Vec<f64>,
150 z: Vec<f64>,
151 objective: f64,
152 kkt_cert: OptimalCertificate,
153 },
154 /// Primal infeasible; Farkas certificate attached.
155 Infeasible { cert: FarkasCertificate },
156 /// Primal unbounded; ray certificate attached.
157 Unbounded { cert: UnboundedRayCertificate },
158 /// Solver stopped before proof completion.
159 Incomplete {
160 incumbent: Option<Vec<f64>>,
161 reason: IncompleteReason,
162 },
163}
164
165/// Why a solve completed without a full optimality proof.
166#[derive(Debug, Clone)]
167pub enum IncompleteReason {
168 MaxIterations,
169 Timeout,
170 NumericalError,
171 SuboptimalSolution,
172 NonConvex(String),
173 NotSupported(String),
174}