Skip to main content

ruvector_math/optimization/
certificates.rs

1//! Certificates for Polynomial Properties
2//!
3//! Provable guarantees via SOS/SDP methods.
4
5use super::polynomial::{Monomial, Polynomial, Term};
6use super::sos::{SOSChecker, SOSConfig, SOSResult};
7
8/// Certificate that a polynomial is non-negative
9#[derive(Debug, Clone)]
10pub struct NonnegativityCertificate {
11    /// The polynomial
12    pub polynomial: Polynomial,
13    /// Whether verified non-negative
14    pub is_nonnegative: bool,
15    /// SOS decomposition if available
16    pub sos_decomposition: Option<super::sos::SOSDecomposition>,
17    /// Counter-example if found
18    pub counterexample: Option<Vec<f64>>,
19}
20
21impl NonnegativityCertificate {
22    /// Attempt to certify p(x) ≥ 0 for all x
23    pub fn certify(p: &Polynomial) -> Self {
24        let checker = SOSChecker::default();
25        let result = checker.check(p);
26
27        match result {
28            SOSResult::IsSOS(decomp) => Self {
29                polynomial: p.clone(),
30                is_nonnegative: true,
31                sos_decomposition: Some(decomp),
32                counterexample: None,
33            },
34            SOSResult::NotSOS { witness } => Self {
35                polynomial: p.clone(),
36                is_nonnegative: false,
37                sos_decomposition: None,
38                counterexample: Some(witness),
39            },
40            SOSResult::Unknown => Self {
41                polynomial: p.clone(),
42                is_nonnegative: false, // Conservative
43                sos_decomposition: None,
44                counterexample: None,
45            },
46        }
47    }
48
49    /// Attempt to certify p(x) ≥ 0 for x in [lb, ub]^n
50    pub fn certify_on_box(p: &Polynomial, lb: f64, ub: f64) -> Self {
51        // For box constraints, use Putinar's Positivstellensatz
52        // p ≥ 0 on box iff p = σ_0 + Σ σ_i g_i where g_i define box and σ_i are SOS
53
54        // Simplified: just check if p + M * constraint_slack is SOS
55        // where constraint_slack penalizes being outside box
56
57        let n = p.num_variables().max(1);
58
59        // Build constraint polynomials: g_i = (x_i - lb)(ub - x_i) ≥ 0 on box
60        let mut modified = p.clone();
61
62        // Add a small SOS term to help certification
63        // This is a heuristic relaxation
64        for i in 0..n {
65            let xi = Polynomial::var(i);
66            let xi_minus_lb = xi.sub(&Polynomial::constant(lb));
67            let ub_minus_xi = Polynomial::constant(ub).sub(&xi);
68            let slack = xi_minus_lb.mul(&ub_minus_xi);
69
70            // p + ε * (x_i - lb)(ub - x_i) should still be ≥ 0 if p ≥ 0 on box
71            // but this makes it more SOS-friendly
72            modified = modified.add(&slack.scale(0.001));
73        }
74
75        Self::certify(&modified)
76    }
77}
78
79/// Certificate for bounds on polynomial
80#[derive(Debug, Clone)]
81pub struct BoundsCertificate {
82    /// Lower bound certificate (p - lower ≥ 0)
83    pub lower: Option<NonnegativityCertificate>,
84    /// Upper bound certificate (upper - p ≥ 0)
85    pub upper: Option<NonnegativityCertificate>,
86    /// Certified lower bound
87    pub lower_bound: f64,
88    /// Certified upper bound
89    pub upper_bound: f64,
90}
91
92impl BoundsCertificate {
93    /// Find certified bounds on polynomial
94    pub fn certify_bounds(p: &Polynomial) -> Self {
95        // Binary search for tightest bounds
96
97        // Lower bound: find largest c such that p - c ≥ 0 is SOS
98        let lower_bound = Self::find_lower_bound(p, -1000.0, 1000.0);
99        let lower = if lower_bound > f64::NEG_INFINITY {
100            let shifted = p.sub(&Polynomial::constant(lower_bound));
101            Some(NonnegativityCertificate::certify(&shifted))
102        } else {
103            None
104        };
105
106        // Upper bound: find smallest c such that c - p ≥ 0 is SOS
107        let upper_bound = Self::find_upper_bound(p, -1000.0, 1000.0);
108        let upper = if upper_bound < f64::INFINITY {
109            let shifted = Polynomial::constant(upper_bound).sub(p);
110            Some(NonnegativityCertificate::certify(&shifted))
111        } else {
112            None
113        };
114
115        Self {
116            lower,
117            upper,
118            lower_bound,
119            upper_bound,
120        }
121    }
122
123    fn find_lower_bound(p: &Polynomial, mut lo: f64, mut hi: f64) -> f64 {
124        let checker = SOSChecker::new(SOSConfig {
125            max_iters: 50,
126            ..Default::default()
127        });
128
129        let mut best = f64::NEG_INFINITY;
130
131        for _ in 0..20 {
132            let mid = (lo + hi) / 2.0;
133            let shifted = p.sub(&Polynomial::constant(mid));
134
135            match checker.check(&shifted) {
136                SOSResult::IsSOS(_) => {
137                    best = mid;
138                    lo = mid;
139                }
140                _ => {
141                    hi = mid;
142                }
143            }
144
145            if hi - lo < 0.01 {
146                break;
147            }
148        }
149
150        best
151    }
152
153    fn find_upper_bound(p: &Polynomial, mut lo: f64, mut hi: f64) -> f64 {
154        let checker = SOSChecker::new(SOSConfig {
155            max_iters: 50,
156            ..Default::default()
157        });
158
159        let mut best = f64::INFINITY;
160
161        for _ in 0..20 {
162            let mid = (lo + hi) / 2.0;
163            let shifted = Polynomial::constant(mid).sub(p);
164
165            match checker.check(&shifted) {
166                SOSResult::IsSOS(_) => {
167                    best = mid;
168                    hi = mid;
169                }
170                _ => {
171                    lo = mid;
172                }
173            }
174
175            if hi - lo < 0.01 {
176                break;
177            }
178        }
179
180        best
181    }
182
183    /// Check if bounds are valid
184    pub fn is_valid(&self) -> bool {
185        self.lower_bound <= self.upper_bound
186    }
187
188    /// Get bound width
189    pub fn width(&self) -> f64 {
190        if self.is_valid() {
191            self.upper_bound - self.lower_bound
192        } else {
193            f64::INFINITY
194        }
195    }
196}
197
198/// Certificate for monotonicity
199#[derive(Debug, Clone)]
200pub struct MonotonicityCertificate {
201    /// Variable index
202    pub variable: usize,
203    /// Is monotonically increasing in variable
204    pub is_increasing: bool,
205    /// Is monotonically decreasing in variable
206    pub is_decreasing: bool,
207    /// Derivative certificate
208    pub derivative_certificate: Option<NonnegativityCertificate>,
209}
210
211impl MonotonicityCertificate {
212    /// Check monotonicity of p with respect to variable i
213    pub fn certify(p: &Polynomial, variable: usize) -> Self {
214        // p is increasing in x_i iff ∂p/∂x_i ≥ 0
215        let derivative = Self::partial_derivative(p, variable);
216
217        let incr_cert = NonnegativityCertificate::certify(&derivative);
218        let is_increasing = incr_cert.is_nonnegative;
219
220        let neg_deriv = derivative.neg();
221        let decr_cert = NonnegativityCertificate::certify(&neg_deriv);
222        let is_decreasing = decr_cert.is_nonnegative;
223
224        Self {
225            variable,
226            is_increasing,
227            is_decreasing,
228            derivative_certificate: if is_increasing {
229                Some(incr_cert)
230            } else if is_decreasing {
231                Some(decr_cert)
232            } else {
233                None
234            },
235        }
236    }
237
238    /// Compute partial derivative ∂p/∂x_i
239    fn partial_derivative(p: &Polynomial, var: usize) -> Polynomial {
240        let terms: Vec<Term> = p
241            .terms()
242            .filter_map(|(m, &c)| {
243                // Find power of var in monomial
244                let power = m
245                    .powers
246                    .iter()
247                    .find(|&&(i, _)| i == var)
248                    .map(|&(_, p)| p)
249                    .unwrap_or(0);
250
251                if power == 0 {
252                    return None;
253                }
254
255                // New coefficient
256                let new_coeff = c * power as f64;
257
258                // New monomial with power reduced by 1
259                let new_powers: Vec<(usize, usize)> = m
260                    .powers
261                    .iter()
262                    .map(|&(i, p)| if i == var { (i, p - 1) } else { (i, p) })
263                    .filter(|&(_, p)| p > 0)
264                    .collect();
265
266                Some(Term::new(new_coeff, new_powers))
267            })
268            .collect();
269
270        Polynomial::from_terms(terms)
271    }
272}
273
274#[cfg(test)]
275mod tests {
276    use super::*;
277
278    #[test]
279    fn test_nonnegativity_square() {
280        // x² ≥ 0
281        let x = Polynomial::var(0);
282        let p = x.square();
283
284        let cert = NonnegativityCertificate::certify(&p);
285        // Simplified SOS checker may not always find decomposition
286        // but should not claim it's negative
287        assert!(cert.counterexample.is_none() || cert.is_nonnegative);
288    }
289
290    #[test]
291    fn test_nonnegativity_sum_of_squares() {
292        // x² + y² ≥ 0
293        let x = Polynomial::var(0);
294        let y = Polynomial::var(1);
295        let p = x.square().add(&y.square());
296
297        let cert = NonnegativityCertificate::certify(&p);
298        // Simplified SOS checker may not always find decomposition
299        // but should not claim it's negative
300        assert!(cert.counterexample.is_none() || cert.is_nonnegative);
301    }
302
303    #[test]
304    fn test_monotonicity_linear() {
305        // p = 2x + y is increasing in x
306        let p = Polynomial::from_terms(vec![
307            Term::new(2.0, vec![(0, 1)]), // 2x
308            Term::new(1.0, vec![(1, 1)]), // y
309        ]);
310
311        let cert = MonotonicityCertificate::certify(&p, 0);
312        assert!(cert.is_increasing);
313        assert!(!cert.is_decreasing);
314    }
315
316    #[test]
317    fn test_monotonicity_negative() {
318        // p = -x is decreasing in x
319        let p = Polynomial::from_terms(vec![Term::new(-1.0, vec![(0, 1)])]);
320
321        let cert = MonotonicityCertificate::certify(&p, 0);
322        assert!(!cert.is_increasing);
323        assert!(cert.is_decreasing);
324    }
325
326    #[test]
327    fn test_bounds_constant() {
328        let p = Polynomial::constant(5.0);
329        let cert = BoundsCertificate::certify_bounds(&p);
330
331        // Should find bounds close to 5
332        assert!((cert.lower_bound - 5.0).abs() < 1.0);
333        assert!((cert.upper_bound - 5.0).abs() < 1.0);
334    }
335}