Skip to main content

pounce_presolve/fbbt/
orchestrator.rs

1//! FBBT outer loop: sweep all constraints to tighten variable bounds
2//! to a fixed point (or `max_iter`).
3//!
4//! ```text
5//! for iter in 0..max_iter:
6//!     for each constraint i:
7//!         tape = provider.constraint_expression(i)   # None ⇒ skip
8//!         forward = forward_pass(tape, x_lo, x_hi)
9//!         result  = reverse_pass(tape, &forward, [g_lo[i], g_hi[i]])
10//!         if result.infeasible: report and bail
11//!         for each Var(j) slot s in tape:
12//!             new_bound = result.slots[s]
13//!             tighten x_lo[j], x_hi[j] against new_bound
14//!             if improvement > tol: mark progress
15//!     if no progress this iter: break
16//! ```
17//!
18//! Matches the Belotti, Cafieri, Lee, Liberti (2010) algorithm,
19//! including the Gauss-Seidel-style sweep (each constraint sees the
20//! freshly tightened bounds from earlier constraints in the same
21//! iteration). Tolerance-based termination — FBBT does not converge
22//! finitely in general.
23//!
24//! Issue [#62].
25//!
26//! [#62]: https://github.com/jkitchin/pounce/issues/62
27
28use pounce_common::types::Number;
29use pounce_nlp::expression_provider::{ExpressionProvider, FbbtOp};
30
31use crate::fbbt::forward::forward_pass;
32use crate::fbbt::interval::Interval;
33use crate::fbbt::reverse::reverse_pass;
34
35/// Knobs for [`run_fbbt`]. Defaults match the proposed `presolve_*`
36/// option set in issue #62.
37#[derive(Debug, Clone, Copy)]
38pub struct FbbtConfig {
39    /// Minimum bound improvement (in absolute units of the variable)
40    /// to keep iterating. Per Belotti et al., FBBT must terminate by
41    /// tolerance, not by convergence.
42    pub tol: Number,
43    /// Outer sweep cap.
44    pub max_iter: usize,
45    /// Cap on the number of constraints to examine per sweep. `0`
46    /// means unlimited. Useful as a wall-time guard on very large
47    /// problems where the first few constraints carry most of the
48    /// tightening.
49    pub max_constraints: usize,
50}
51
52impl Default for FbbtConfig {
53    fn default() -> Self {
54        Self {
55            tol: 1.0e-6,
56            max_iter: 10,
57            max_constraints: 0,
58        }
59    }
60}
61
62/// What the orchestrator did.
63#[derive(Debug, Clone, Default, PartialEq)]
64pub struct FbbtReport {
65    /// Number of outer sweeps actually executed (≤ `cfg.max_iter`).
66    pub iterations: usize,
67    /// Total number of `(variable, bound)` tightening events across
68    /// all sweeps and all constraints.
69    pub bound_updates: usize,
70    /// Index of the constraint that proved infeasibility, if any.
71    /// When set, the variable bounds in the caller's arrays are
72    /// undefined and must not be trusted.
73    pub infeasibility_witness: Option<usize>,
74    /// Sum of absolute bound improvements across all updates — for
75    /// reporting, not part of the algorithm.
76    pub total_tightening: Number,
77}
78
79/// Run FBBT against `provider` until quiescent or `cfg.max_iter`.
80///
81/// `x_lo` / `x_hi` are read AND written. They start as the user's
82/// declared variable bounds and end as the FBBT-tightened bounds. On
83/// detected infeasibility, the contents are left in their
84/// partially-updated state and `report.infeasibility_witness` is
85/// `Some(constraint_idx)`.
86///
87/// `g_lo` / `g_hi` are the constraint bounds, length `m`. Providers
88/// that return `None` for a constraint index are skipped silently
89/// (FBBT can't tighten without a structural expression).
90///
91/// `row_kept`, when `Some`, is a length-`n_constraints` mask: rows whose
92/// entry is `false` are skipped entirely. A presolve caller passes the
93/// Phase-0 `row_kept_inner` mask here so propagation never runs over a
94/// row an earlier auxiliary elimination dropped — over the aux-clamped
95/// variable bounds such an eliminated row can manufacture a spurious
96/// infeasibility (the issue #53 row-filtering Phase 1 already performs).
97/// `None` means "consider every row" (the standalone / test default).
98pub fn run_fbbt(
99    provider: &dyn ExpressionProvider,
100    n_vars: usize,
101    n_constraints: usize,
102    x_lo: &mut [Number],
103    x_hi: &mut [Number],
104    g_lo: &[Number],
105    g_hi: &[Number],
106    row_kept: Option<&[bool]>,
107    cfg: &FbbtConfig,
108) -> FbbtReport {
109    let mut report = FbbtReport::default();
110
111    assert_eq!(x_lo.len(), n_vars, "x_lo length");
112    assert_eq!(x_hi.len(), n_vars, "x_hi length");
113    assert_eq!(g_lo.len(), n_constraints, "g_lo length");
114    assert_eq!(g_hi.len(), n_constraints, "g_hi length");
115    if let Some(mask) = row_kept {
116        assert_eq!(mask.len(), n_constraints, "row_kept length");
117    }
118
119    let cap = if cfg.max_constraints == 0 {
120        n_constraints
121    } else {
122        cfg.max_constraints.min(n_constraints)
123    };
124
125    // Per-variable scratch, allocated ONCE and reused across every
126    // constraint and sweep. A constraint's tape typically touches only
127    // a handful of variables, so we never want to allocate or scan an
128    // `O(n_vars)` buffer per constraint. `tighten[j]` holds the running
129    // intersection of the reverse-propagated intervals for variable `j`
130    // *within the current constraint*; `last_seen[j]` stamps which
131    // constraint last wrote `tighten[j]` (so the first `Var(j)` slot of
132    // a constraint overwrites rather than intersecting stale data, with
133    // no per-constraint reset); `touched` lists the distinct variables
134    // this constraint actually mentions, so the apply step iterates only
135    // those. `stamp` is a monotonic per-constraint-visit counter.
136    let mut tighten: Vec<Interval> = vec![Interval::ENTIRE; n_vars];
137    let mut last_seen: Vec<usize> = vec![usize::MAX; n_vars];
138    let mut touched: Vec<usize> = Vec::new();
139    let mut stamp: usize = 0;
140
141    for _iter in 0..cfg.max_iter {
142        report.iterations += 1;
143        let mut improved = false;
144
145        for i in 0..cap {
146            if let Some(mask) = row_kept {
147                if !mask[i] {
148                    continue;
149                }
150            }
151            let Some(tape) = provider.constraint_expression(i) else {
152                continue;
153            };
154            if tape.is_empty() {
155                continue;
156            }
157
158            let forward = match forward_pass(&tape, x_lo, x_hi) {
159                Ok(v) => v,
160                Err(_) => continue, // Malformed tape or out-of-range — skip safely.
161            };
162            let bound = Interval::new(g_lo[i], g_hi[i]);
163            let reverse = reverse_pass(&tape, &forward, bound);
164            if reverse.infeasible {
165                report.infeasibility_witness = Some(i);
166                return report;
167            }
168
169            // Aggregate per-variable tightening: a variable can
170            // appear in multiple `Var(j)` slots of the tape (when
171            // the constraint references it without CSE sharing).
172            // Each slot may carry a different reverse-propagated
173            // interval; the variable's tightened interval is the
174            // INTERSECTION of all those slot intervals. We touch only
175            // the variables this constraint mentions — the `stamp`
176            // guards a first-write-overwrites-then-intersect discipline
177            // on the reused `tighten` scratch, so no `O(n_vars)` reset.
178            stamp += 1;
179            touched.clear();
180            for (slot_idx, op) in tape.ops.iter().enumerate() {
181                if let FbbtOp::Var(j) = *op {
182                    if last_seen[j] == stamp {
183                        tighten[j] = tighten[j].intersect(reverse.slots[slot_idx]);
184                    } else {
185                        last_seen[j] = stamp;
186                        tighten[j] = reverse.slots[slot_idx];
187                        touched.push(j);
188                    }
189                }
190            }
191
192            // Apply — only the variables this constraint touched. Any
193            // variable absent from the tape keeps an ENTIRE interval and
194            // could never tighten or be empty, so iterating `touched`
195            // alone is exactly equivalent to the old `0..n_vars` scan.
196            for &j in &touched {
197                let t = tighten[j];
198                if t.is_empty() {
199                    report.infeasibility_witness = Some(i);
200                    return report;
201                }
202                if t.is_entire() {
203                    continue;
204                }
205                let new_lo = x_lo[j].max(t.lo);
206                let new_hi = x_hi[j].min(t.hi);
207                if new_lo > new_hi {
208                    report.infeasibility_witness = Some(i);
209                    return report;
210                }
211                let delta_lo = (new_lo - x_lo[j]).max(0.0);
212                let delta_hi = (x_hi[j] - new_hi).max(0.0);
213                let delta = delta_lo.max(delta_hi);
214                if delta > cfg.tol {
215                    x_lo[j] = new_lo;
216                    x_hi[j] = new_hi;
217                    report.bound_updates += 1;
218                    report.total_tightening += delta;
219                    improved = true;
220                } else if delta_lo > 0.0 || delta_hi > 0.0 {
221                    // Tiny tightening below tol — apply but don't
222                    // count as progress.
223                    x_lo[j] = new_lo;
224                    x_hi[j] = new_hi;
225                }
226            }
227        }
228
229        if !improved {
230            break;
231        }
232    }
233
234    report
235}
236
237#[cfg(test)]
238mod tests {
239    use super::*;
240    use pounce_nlp::expression_provider::{FbbtOp, FbbtTape};
241
242    /// Test helper: a provider that just returns a stored vec of
243    /// tapes, one per constraint.
244    struct StubProvider {
245        tapes: Vec<Option<FbbtTape>>,
246    }
247
248    impl ExpressionProvider for StubProvider {
249        fn constraint_expression(&self, i: usize) -> Option<FbbtTape> {
250            self.tapes.get(i).and_then(|t| t.clone())
251        }
252    }
253
254    /// `x² + y² = 1` with initial box `[-10, 10]²`. Each variable
255    /// should be tightened to a subset of `[-1, 1]`.
256    #[test]
257    fn unit_circle_tightens_box() {
258        let tape = FbbtTape {
259            ops: vec![
260                FbbtOp::Var(0),
261                FbbtOp::PowInt(0, 2),
262                FbbtOp::Var(1),
263                FbbtOp::PowInt(2, 2),
264                FbbtOp::Add(1, 3),
265            ],
266        };
267        let provider = StubProvider {
268            tapes: vec![Some(tape)],
269        };
270        let mut x_lo = vec![-10.0, -10.0];
271        let mut x_hi = vec![10.0, 10.0];
272        let r = run_fbbt(
273            &provider,
274            2,
275            1,
276            &mut x_lo,
277            &mut x_hi,
278            &[1.0],
279            &[1.0],
280            None,
281            &FbbtConfig::default(),
282        );
283        assert!(r.infeasibility_witness.is_none());
284        // Both variables must tighten (one update each, per-variable).
285        assert!(r.bound_updates >= 2, "got {} updates", r.bound_updates);
286        for (lo, hi) in x_lo.iter().zip(&x_hi) {
287            assert!(*lo >= -1.0 - 1e-6, "lo = {lo}");
288            assert!(*hi <= 1.0 + 1e-6, "hi = {hi}");
289        }
290    }
291
292    /// `exp(x) ≤ 10` ⇒ `x ≤ ln 10 ≈ 2.302`.
293    #[test]
294    fn exp_upper_bound_tightens() {
295        let tape = FbbtTape {
296            ops: vec![FbbtOp::Var(0), FbbtOp::Exp(0)],
297        };
298        let provider = StubProvider {
299            tapes: vec![Some(tape)],
300        };
301        let mut x_lo = vec![-10.0];
302        let mut x_hi = vec![10.0];
303        let r = run_fbbt(
304            &provider,
305            1,
306            1,
307            &mut x_lo,
308            &mut x_hi,
309            &[Number::NEG_INFINITY],
310            &[10.0],
311            None,
312            &FbbtConfig::default(),
313        );
314        assert!(r.infeasibility_witness.is_none());
315        // ln(10) ≈ 2.3026.
316        assert!(x_hi[0] <= 2.31, "x_hi = {}", x_hi[0]);
317        // Lower bound unaffected by an upper-only constraint.
318        assert_eq!(x_lo[0], -10.0);
319    }
320
321    /// Cross-constraint iteration: constraint A tightens y, after
322    /// which constraint B (which mentions y on its RHS) can tighten
323    /// x further than a single pass would.
324    ///
325    /// * A: `y² ≤ 1` ⇒ `y ∈ [-1, 1]` (tightens y from [-10, 10]).
326    /// * B: `x + y² = 0.5` ⇒ once y ∈ [-1, 1], y² ∈ [0, 1], so
327    ///   `x = 0.5 - y² ∈ [-0.5, 0.5]`. Before A runs, B would only
328    ///   tighten x to `[0.5 - 100, 0.5 - 0] = [-99.5, 0.5]`.
329    #[test]
330    fn coupled_constraints_iterate() {
331        let tape_a = FbbtTape {
332            ops: vec![FbbtOp::Var(1), FbbtOp::PowInt(0, 2)],
333        };
334        let tape_b = FbbtTape {
335            ops: vec![
336                FbbtOp::Var(0),
337                FbbtOp::Var(1),
338                FbbtOp::PowInt(1, 2),
339                FbbtOp::Add(0, 2),
340            ],
341        };
342        let provider = StubProvider {
343            tapes: vec![Some(tape_a), Some(tape_b)],
344        };
345        let mut x_lo = vec![-10.0, -10.0];
346        let mut x_hi = vec![10.0, 10.0];
347        let r = run_fbbt(
348            &provider,
349            2,
350            2,
351            &mut x_lo,
352            &mut x_hi,
353            &[Number::NEG_INFINITY, 0.5],
354            &[1.0, 0.5],
355            None,
356            &FbbtConfig::default(),
357        );
358        assert!(r.infeasibility_witness.is_none());
359        // y was tightened to [-1, 1].
360        assert!(x_lo[1] >= -1.0 - 1e-6, "y_lo = {}", x_lo[1]);
361        assert!(x_hi[1] <= 1.0 + 1e-6, "y_hi = {}", x_hi[1]);
362        // x was tightened to [-0.5, 0.5] — only achievable when the
363        // first sweep gave y² ≤ 1 before constraint B fires.
364        assert!(x_lo[0] >= -0.5 - 1e-6, "x_lo = {}", x_lo[0]);
365        assert!(x_hi[0] <= 0.5 + 1e-6, "x_hi = {}", x_hi[0]);
366    }
367
368    /// FBBT should detect infeasibility: x ∈ [10, 20] but
369    /// `x ∈ [1, 5]` from the constraint.
370    #[test]
371    fn detects_infeasibility() {
372        let tape = FbbtTape {
373            ops: vec![FbbtOp::Var(0)],
374        };
375        let provider = StubProvider {
376            tapes: vec![Some(tape)],
377        };
378        let mut x_lo = vec![10.0];
379        let mut x_hi = vec![20.0];
380        let r = run_fbbt(
381            &provider,
382            1,
383            1,
384            &mut x_lo,
385            &mut x_hi,
386            &[1.0],
387            &[5.0],
388            None,
389            &FbbtConfig::default(),
390        );
391        assert_eq!(r.infeasibility_witness, Some(0));
392    }
393
394    /// Constraint without expression (provider returns None) →
395    /// no-op, no tightening, no infeasibility.
396    #[test]
397    fn missing_expression_is_silent_noop() {
398        let provider = StubProvider { tapes: vec![None] };
399        let mut x_lo = vec![-1.0];
400        let mut x_hi = vec![1.0];
401        let r = run_fbbt(
402            &provider,
403            1,
404            1,
405            &mut x_lo,
406            &mut x_hi,
407            &[-100.0],
408            &[100.0],
409            None,
410            &FbbtConfig::default(),
411        );
412        assert!(r.infeasibility_witness.is_none());
413        assert_eq!(r.bound_updates, 0);
414        assert_eq!(x_lo, vec![-1.0]);
415        assert_eq!(x_hi, vec![1.0]);
416    }
417
418    /// Max-iter cap: a fixed-point that needs many sweeps must stop
419    /// at `cfg.max_iter`. We test by setting `max_iter = 1` and
420    /// observing the bound is loose.
421    #[test]
422    fn max_iter_caps_iteration_count() {
423        let tape_sum = FbbtTape {
424            ops: vec![FbbtOp::Var(0), FbbtOp::Var(1), FbbtOp::Add(0, 1)],
425        };
426        let tape_diff = FbbtTape {
427            ops: vec![FbbtOp::Var(0), FbbtOp::Var(1), FbbtOp::Sub(0, 1)],
428        };
429        let provider = StubProvider {
430            tapes: vec![Some(tape_sum), Some(tape_diff)],
431        };
432        let mut x_lo = vec![-10.0, -10.0];
433        let mut x_hi = vec![10.0, 10.0];
434        let cfg = FbbtConfig {
435            tol: 1e-6,
436            max_iter: 1,
437            max_constraints: 0,
438        };
439        let r = run_fbbt(
440            &provider,
441            2,
442            2,
443            &mut x_lo,
444            &mut x_hi,
445            &[1.0, 0.0],
446            &[1.0, 0.0],
447            None,
448            &cfg,
449        );
450        assert!(r.infeasibility_witness.is_none());
451        assert_eq!(r.iterations, 1);
452        // After one sweep the box should still be much wider than
453        // 1e-3 (the converged width seen in the previous test).
454        let width0 = x_hi[0] - x_lo[0];
455        let width1 = x_hi[1] - x_lo[1];
456        assert!(
457            width0 > 1e-3 || width1 > 1e-3,
458            "single sweep already converged unexpectedly"
459        );
460    }
461
462    /// `max_constraints` caps the per-sweep workload.
463    #[test]
464    fn max_constraints_truncates_sweep() {
465        let tape_a = FbbtTape {
466            ops: vec![FbbtOp::Var(0)],
467        };
468        let tape_b = FbbtTape {
469            ops: vec![FbbtOp::Var(1)],
470        };
471        let provider = StubProvider {
472            tapes: vec![Some(tape_a), Some(tape_b)],
473        };
474        let mut x_lo = vec![-10.0, -10.0];
475        let mut x_hi = vec![10.0, 10.0];
476        let cfg = FbbtConfig {
477            tol: 1e-6,
478            max_iter: 5,
479            max_constraints: 1, // skip constraint 1
480        };
481        let _ = run_fbbt(
482            &provider,
483            2,
484            2,
485            &mut x_lo,
486            &mut x_hi,
487            &[-1.0, -1.0],
488            &[1.0, 1.0],
489            None,
490            &cfg,
491        );
492        // x_0 must have tightened, x_1 untouched.
493        assert!(x_lo[0] >= -1.0 - 1e-12);
494        assert!(x_hi[0] <= 1.0 + 1e-12);
495        assert_eq!(x_lo[1], -10.0);
496        assert_eq!(x_hi[1], 10.0);
497    }
498
499    /// A variable that appears in two structurally distinct `Var(j)`
500    /// slots of one constraint must end with the INTERSECTION of both
501    /// slots' reverse-propagated intervals — this exercises the reused
502    /// scratch's `stamp`-guarded "first slot overwrites, later slots
503    /// intersect" discipline, the subtle part of the sparse-apply
504    /// rewrite (M28).
505    ///
506    /// A variable appearing in two structurally distinct `Var(j)` slots
507    /// of one constraint must end with the INTERSECTION of both slots'
508    /// reverse intervals. The squared slot comes FIRST (yielding the
509    /// tight `x ≤ √6 ≈ 2.449`) and the linear slot SECOND (yielding only
510    /// the loose `x ≤ 6`); in a *single sweep* the correct intersection
511    /// gives `x_hi ≈ 2.449`, whereas an aggregation bug that kept just
512    /// the last slot would leave `x_hi ≈ 6`. Using `max_iter = 1` is
513    /// essential — iterating to a fixed point would wash the difference
514    /// out, since all slot intervals coincide at the root.
515    ///
516    /// `x² + x = 6` over `x ∈ [0, 10]` (true root x = 2).
517    #[test]
518    fn duplicate_var_slots_intersect() {
519        let tape = FbbtTape {
520            ops: vec![
521                FbbtOp::Var(0),       // slot 0: base of x²  (tight slot)
522                FbbtOp::PowInt(0, 2), // slot 1: x²
523                FbbtOp::Var(0),       // slot 2: linear x    (loose slot)
524                FbbtOp::Add(1, 2),    // slot 3: x² + x
525            ],
526        };
527        let provider = StubProvider {
528            tapes: vec![Some(tape)],
529        };
530        let mut x_lo = vec![0.0];
531        let mut x_hi = vec![10.0];
532        let cfg = FbbtConfig {
533            tol: 1e-6,
534            max_iter: 1, // single sweep — see doc comment
535            max_constraints: 0,
536        };
537        let r = run_fbbt(
538            &provider,
539            1,
540            1,
541            &mut x_lo,
542            &mut x_hi,
543            &[6.0],
544            &[6.0],
545            None,
546            &cfg,
547        );
548        assert!(r.infeasibility_witness.is_none());
549        assert_eq!(x_lo[0], 0.0, "lower bound unchanged in one sweep");
550        // √6 ≈ 2.449: requires the FIRST (squared) slot's interval to be
551        // intersected in. Keeping only the last (linear) slot leaves 6.
552        assert!(
553            x_hi[0] <= 2.45,
554            "x_hi = {} — duplicate Var slots were not intersected (got the loose linear slot)",
555            x_hi[0]
556        );
557        assert!(
558            x_hi[0] >= 2.449 - 1e-3,
559            "x_hi = {} unexpectedly tight",
560            x_hi[0]
561        );
562    }
563
564    /// Soundness fuzz on a quadratic: any feasible point of the
565    /// original problem must still be feasible w.r.t. the
566    /// FBBT-tightened bounds.
567    #[test]
568    fn fuzz_soundness_pointwise() {
569        // y² + x = 5, with original bounds x ∈ [-10, 5], y ∈ [-3, 3].
570        let tape = FbbtTape {
571            ops: vec![
572                FbbtOp::Var(1),
573                FbbtOp::PowInt(0, 2),
574                FbbtOp::Var(0),
575                FbbtOp::Add(1, 2),
576            ],
577        };
578        let provider = StubProvider {
579            tapes: vec![Some(tape)],
580        };
581        let mut x_lo = vec![-10.0, -3.0];
582        let mut x_hi = vec![5.0, 3.0];
583        let _ = run_fbbt(
584            &provider,
585            2,
586            1,
587            &mut x_lo,
588            &mut x_hi,
589            &[5.0],
590            &[5.0],
591            None,
592            &FbbtConfig::default(),
593        );
594        // For y values on a grid, x = 5 - y²; test that (x, y) lies
595        // inside the tightened box.
596        for k in -30..=30 {
597            let y = k as Number / 10.0;
598            if !(-3.0..=3.0).contains(&y) {
599                continue;
600            }
601            let x = 5.0 - y * y;
602            if !(-10.0..=5.0).contains(&x) {
603                continue;
604            }
605            assert!(
606                x_lo[0] - 1e-6 <= x && x <= x_hi[0] + 1e-6,
607                "feasible x={x} dropped (bounds {} .. {})",
608                x_lo[0],
609                x_hi[0]
610            );
611            assert!(
612                x_lo[1] - 1e-6 <= y && y <= x_hi[1] + 1e-6,
613                "feasible y={y} dropped"
614            );
615        }
616    }
617
618    /// H12: the `row_kept` mask must keep FBBT from ever touching a row a
619    /// prior presolve phase dropped. Constraint 0 demands `x = 5` over the
620    /// box `x ∈ [0, 1]` — infeasible. With no mask FBBT (correctly, for a
621    /// live row) flags it; but when Phase 0 has dropped that row, running
622    /// propagation against the aux-clamped box manufactures a spurious
623    /// infeasibility. Masking the row out must suppress that and leave the
624    /// box untouched.
625    #[test]
626    fn dropped_row_is_skipped_and_does_not_flag_infeasible() {
627        let tape = FbbtTape {
628            ops: vec![FbbtOp::Var(0)],
629        };
630        // Row 0: `x = 5` (bound [5,5]); row 1: a no-op (`None` tape).
631        let provider = StubProvider {
632            tapes: vec![Some(tape), None],
633        };
634        let g_lo = [5.0, 0.0];
635        let g_hi = [5.0, 0.0];
636        let cfg = FbbtConfig::default();
637
638        // Control — row 0 live: FBBT flags it infeasible against [0,1].
639        let mut x_lo = [0.0];
640        let mut x_hi = [1.0];
641        let r = run_fbbt(
642            &provider, 1, 2, &mut x_lo, &mut x_hi, &g_lo, &g_hi, None, &cfg,
643        );
644        assert_eq!(
645            r.infeasibility_witness,
646            Some(0),
647            "a live `x = 5` row over [0,1] must read infeasible (control)"
648        );
649
650        // Fixed — row 0 dropped by Phase 0: masked out, no false infeasibility.
651        let mut x_lo = [0.0];
652        let mut x_hi = [1.0];
653        let r = run_fbbt(
654            &provider,
655            1,
656            2,
657            &mut x_lo,
658            &mut x_hi,
659            &g_lo,
660            &g_hi,
661            Some(&[false, true]),
662            &cfg,
663        );
664        assert_eq!(
665            r.infeasibility_witness, None,
666            "a dropped row must never manufacture infeasibility"
667        );
668        assert_eq!(
669            (x_lo[0], x_hi[0]),
670            (0.0, 1.0),
671            "the box must be untouched when the only constraint is masked out"
672        );
673    }
674}