logicaffeine_proof/
linarith_solve.rs

1//! The decision core for linear integer arithmetic: Fourier-Motzkin elimination
2//! that tracks the non-negative combination it eliminates with, so an
3//! unsatisfiable system yields its **Farkas certificate** — the multipliers `λᵢ ≥ 0`
4//! on the original constraints such that `Σ λᵢ·constraintᵢ` is a positive constant
5//! `≤ 0` (a contradiction). The proof engine reconstructs a kernel proof from those
6//! multipliers via `le_mul_nonneg`/`le_add_mono` + the Bool no-confusion
7//! discriminator. Pure and self-contained — no kernel, no certificates here.
8
9use std::collections::BTreeMap;
10
11use crate::ProofTerm;
12
13/// A linear expression `Σ cⱼ·xⱼ + constant` over the integers (zero coefficients
14/// pruned, so equality is canonical).
15#[derive(Clone, Debug, PartialEq, Eq)]
16pub struct LinExpr {
17    pub coeffs: BTreeMap<String, i64>,
18    pub constant: i64,
19}
20
21impl LinExpr {
22    fn constant(c: i64) -> Self {
23        LinExpr { coeffs: BTreeMap::new(), constant: c }
24    }
25    fn var(name: &str) -> Self {
26        let mut coeffs = BTreeMap::new();
27        coeffs.insert(name.to_string(), 1);
28        LinExpr { coeffs, constant: 0 }
29    }
30    fn prune(mut self) -> Self {
31        self.coeffs.retain(|_, c| *c != 0);
32        self
33    }
34    fn add(&self, o: &Self) -> Self {
35        let mut coeffs = self.coeffs.clone();
36        for (k, v) in &o.coeffs {
37            *coeffs.entry(k.clone()).or_insert(0) += v;
38        }
39        LinExpr { coeffs, constant: self.constant + o.constant }.prune()
40    }
41    fn neg(&self) -> Self {
42        LinExpr {
43            coeffs: self.coeffs.iter().map(|(k, v)| (k.clone(), -v)).collect(),
44            constant: -self.constant,
45        }
46    }
47    pub fn sub(&self, o: &Self) -> Self {
48        self.add(&o.neg())
49    }
50    /// True when this is a bare integer constant (no variables remain).
51    pub fn is_const(&self) -> bool {
52        self.coeffs.is_empty()
53    }
54    fn scale(&self, k: i64) -> Self {
55        LinExpr {
56            coeffs: self.coeffs.iter().map(|(x, v)| (x.clone(), v * k)).collect(),
57            constant: self.constant * k,
58        }
59        .prune()
60    }
61    fn is_constant(&self) -> bool {
62        self.coeffs.is_empty()
63    }
64    fn coeff(&self, v: &str) -> i64 {
65        self.coeffs.get(v).copied().unwrap_or(0)
66    }
67}
68
69/// Parse a [`ProofTerm`] into a linear expression, or `None` if it is non-linear
70/// (e.g. `mul` of two non-constants). Numeric constants are literals; other names
71/// are variables; `add`/`sub`/`mul` build the form.
72pub fn parse_lin(t: &ProofTerm) -> Option<LinExpr> {
73    match t {
74        ProofTerm::Constant(s) => Some(match s.parse::<i64>() {
75            Ok(n) => LinExpr::constant(n),
76            Err(_) => LinExpr::var(s),
77        }),
78        ProofTerm::Variable(s) | ProofTerm::BoundVarRef(s) => Some(LinExpr::var(s)),
79        ProofTerm::Function(name, args) => match (name.as_str(), args.as_slice()) {
80            ("add", [a, b]) => Some(parse_lin(a)?.add(&parse_lin(b)?)),
81            ("sub", [a, b]) => Some(parse_lin(a)?.sub(&parse_lin(b)?)),
82            ("mul", [a, b]) => {
83                let (la, lb) = (parse_lin(a)?, parse_lin(b)?);
84                if la.is_constant() {
85                    Some(lb.scale(la.constant))
86                } else if lb.is_constant() {
87                    Some(la.scale(lb.constant))
88                } else {
89                    None
90                }
91            }
92            _ => None,
93        },
94        ProofTerm::Group(_) => None,
95    }
96}
97
98/// A row of the elimination: the constraint `e ≤ 0`, tagged with the non-negative
99/// combination `prov` (original-constraint index → multiplier) that produced it.
100#[derive(Clone, Debug)]
101struct Row {
102    e: LinExpr,
103    prov: BTreeMap<usize, i64>,
104}
105
106fn combine_prov(a: &BTreeMap<usize, i64>, ka: i64, b: &BTreeMap<usize, i64>, kb: i64) -> BTreeMap<usize, i64> {
107    let mut out = BTreeMap::new();
108    for (i, v) in a {
109        *out.entry(*i).or_insert(0) += v * ka;
110    }
111    for (i, v) in b {
112        *out.entry(*i).or_insert(0) += v * kb;
113    }
114    out.retain(|_, v| *v != 0);
115    out
116}
117
118/// Given constraints `cᵢ ≤ 0`, find a non-negative integer combination
119/// `Σ λᵢ·cᵢ = (positive constant) ≤ 0` — a Farkas refutation. Returns the
120/// multipliers `λᵢ`, or `None` if the system is satisfiable over ℚ (so no rational
121/// Farkas certificate exists).
122pub fn find_farkas(constraints: &[LinExpr]) -> Option<BTreeMap<usize, i64>> {
123    let mut rows: Vec<Row> = constraints
124        .iter()
125        .enumerate()
126        .map(|(i, e)| Row { e: e.clone(), prov: BTreeMap::from([(i, 1)]) })
127        .collect();
128
129    let contradiction = |rows: &[Row]| -> Option<BTreeMap<usize, i64>> {
130        rows.iter()
131            .find(|r| r.e.is_constant() && r.e.constant > 0)
132            .map(|r| r.prov.clone())
133    };
134    if let Some(p) = contradiction(&rows) {
135        return Some(p);
136    }
137
138    // Eliminate variables one at a time (Fourier-Motzkin).
139    let mut vars: Vec<String> = rows
140        .iter()
141        .flat_map(|r| r.e.coeffs.keys().cloned())
142        .collect();
143    vars.sort();
144    vars.dedup();
145
146    for v in vars {
147        let (mut pos, mut neg, mut zero) = (Vec::new(), Vec::new(), Vec::new());
148        for r in rows {
149            match r.e.coeff(&v) {
150                c if c > 0 => pos.push(r),
151                c if c < 0 => neg.push(r),
152                _ => zero.push(r),
153            }
154        }
155        let mut next = zero;
156        for p in &pos {
157            for n in &neg {
158                let (pc, nc) = (p.e.coeff(&v), -n.e.coeff(&v)); // both > 0
159                // nc·p + pc·n  cancels v (coeff: nc·pc + pc·(-nc) = 0).
160                next.push(Row {
161                    e: p.e.scale(nc).add(&n.e.scale(pc)),
162                    prov: combine_prov(&p.prov, nc, &n.prov, pc),
163                });
164            }
165        }
166        rows = next;
167        if let Some(p) = contradiction(&rows) {
168            return Some(p);
169        }
170    }
171    contradiction(&rows)
172}
173
174/// `Σ multipliers[i]·constraints[i]`. For a valid Farkas certificate this is a
175/// bare positive constant (the variables cancel) — that constant is the `d` in the
176/// reconstructed contradiction `0 ≤ -d`.
177pub fn combine(constraints: &[LinExpr], multipliers: &BTreeMap<usize, i64>) -> LinExpr {
178    let mut acc = LinExpr::constant(0);
179    for (&i, &m) in multipliers {
180        acc = acc.add(&constraints[i].scale(m));
181    }
182    acc
183}
184
185#[cfg(test)]
186mod tests {
187    use super::*;
188
189    fn cst(c: i64) -> ProofTerm {
190        ProofTerm::Constant(c.to_string())
191    }
192    fn var(s: &str) -> ProofTerm {
193        ProofTerm::Constant(s.to_string())
194    }
195    fn f(n: &str, a: Vec<ProofTerm>) -> ProofTerm {
196        ProofTerm::Function(n.to_string(), a)
197    }
198    /// The constraint from `l ≤ r`: `l - r ≤ 0`.
199    fn le_constraint(l: ProofTerm, r: ProofTerm) -> LinExpr {
200        parse_lin(&l).unwrap().sub(&parse_lin(&r).unwrap())
201    }
202
203    #[test]
204    fn parses_linear_forms() {
205        // 2*x + 3  -  (x + 1)  =  x + 2
206        let e = le_constraint(f("add", vec![f("mul", vec![cst(2), var("x")]), cst(3)]), f("add", vec![var("x"), cst(1)]));
207        assert_eq!(e.coeff("x"), 1);
208        assert_eq!(e.constant, 2);
209    }
210
211    #[test]
212    fn rejects_nonlinear() {
213        assert!(parse_lin(&f("mul", vec![var("x"), var("y")])).is_none());
214    }
215
216    #[test]
217    fn chain_contradiction_5_le_x_le_3() {
218        // 5 ≤ x  →  5 - x ≤ 0 ;  x ≤ 3  →  x - 3 ≤ 0.  Sum = 2 ≤ 0 (contradiction).
219        let cs = vec![le_constraint(cst(5), var("x")), le_constraint(var("x"), cst(3))];
220        let cert = find_farkas(&cs).expect("5≤x≤3 is unsatisfiable");
221        assert_eq!(cert.get(&0), Some(&1));
222        assert_eq!(cert.get(&1), Some(&1));
223    }
224
225    #[test]
226    fn scaling_contradiction_needs_a_multiplier() {
227        // 2 ≤ x  →  2 - x ≤ 0 ;  2*x ≤ 3  →  2x - 3 ≤ 0.
228        // 2·(2 - x) + 1·(2x - 3) = 1 ≤ 0  — contradiction, multiplier 2 on the first.
229        let cs = vec![
230            le_constraint(cst(2), var("x")),
231            le_constraint(f("mul", vec![cst(2), var("x")]), cst(3)),
232        ];
233        let cert = find_farkas(&cs).expect("2≤x and 2x≤3 is unsatisfiable");
234        assert_eq!(cert.get(&0), Some(&2), "needs to scale `2 ≤ x` by 2");
235        assert_eq!(cert.get(&1), Some(&1));
236    }
237
238    #[test]
239    fn two_variable_contradiction() {
240        // x ≤ y, y ≤ z, z ≤ x - 1  →  x ≤ y ≤ z ≤ x-1  →  x ≤ x-1  →  1 ≤ 0.
241        let cs = vec![
242            le_constraint(var("x"), var("y")),
243            le_constraint(var("y"), var("z")),
244            le_constraint(var("z"), f("sub", vec![var("x"), cst(1)])),
245        ];
246        let cert = find_farkas(&cs).expect("the cycle is unsatisfiable");
247        assert_eq!(cert.get(&0), Some(&1));
248        assert_eq!(cert.get(&1), Some(&1));
249        assert_eq!(cert.get(&2), Some(&1));
250    }
251
252    #[test]
253    fn satisfiable_system_has_no_certificate() {
254        // 1 ≤ x, x ≤ 5  — consistent.
255        let cs = vec![le_constraint(cst(1), var("x")), le_constraint(var("x"), cst(5))];
256        assert!(find_farkas(&cs).is_none(), "1≤x≤5 is satisfiable");
257    }
258}
logicaffeine_proof/linarith_solve.rs

logicaffeine_proof/
linarith_solve.rs
