logicaffeine_proof/
lrat.rs

1//! LRAT refutations at scale: hint chains found by watched-literal propagation, trimmed to the clauses a refutation
2//! uses, and replayed by a checker that trusts nothing the search did.
3//!
4//! A CDCL solve leaves its learned clauses in order, each derivable by reverse unit propagation (RUP) from the
5//! formula and the clauses before it ([`crate::cdcl::Solver::learned`]). [`crate::rup::check_refutation`] replays
6//! such a trace by propagating the whole database to a fixpoint for every clause, a cost a circuit miter of tens of
7//! thousands of clauses cannot pay a learned clause. [`refutation`] instead finds each clause's LRAT hint chain
8//! (Cruz-Filipe et al., 2017) with two watched literals (Moskewicz et al., *Chaff*, 2001), walking the trace
9//! backward from the empty clause, the `drat-trim` order (Wetzler, Heule & Hunt, 2014): a learned clause no later
10//! step uses is never checked and never shipped. [`check`] replays a proof in time linear in its hints, and
11//! [`Lrat::to_text`] prints the standard LRAT text that [`crate::proof_emit::check_lrat`] and `cake_lpr` read.
12//! [`derivation`] trims the same way back from any target clauses of a log, not only the empty one — what one
13//! incremental solver derives across many queries — and [`check_derivation`] replays it and finds each target.
14//!
15//! Ids follow the LRAT convention: the formula's clauses are `1..=n` in order, the `j`-th learned clause is
16//! `n + 1 + j`, and the empty clause takes the id after the last learned one. A trimmed proof skips the ids of the
17//! clauses it drops.
18
19use std::collections::{HashMap, HashSet};
20
21use crate::cdcl::Lit;
22use crate::rup::{clause_state, set_true, ClauseState};
23
24/// One addition of an LRAT refutation: under the clause's negation each hinted clause, in order, is unit, until the
25/// last conflicts.
26#[derive(Clone, Debug, PartialEq, Eq)]
27pub struct LratStep {
28    pub id: u64,
29    pub clause: Vec<Lit>,
30    pub hints: Vec<u64>,
31}
32
33/// An LRAT refutation of a formula whose clauses carry the ids `1..=n`: additions in increasing id order, ending
34/// in the empty clause.
35#[derive(Clone, Debug, PartialEq, Eq)]
36pub struct Lrat {
37    pub steps: Vec<LratStep>,
38}
39
40impl Lrat {
41    /// The proof as LRAT text: `<id> <clause> 0 <hints> 0` a line, literals in DIMACS numbering.
42    pub fn to_text(&self) -> String {
43        let mut out = String::new();
44        for step in &self.steps {
45            out.push_str(&step.id.to_string());
46            for &l in &step.clause {
47                out.push(' ');
48                out.push_str(&dimacs(l).to_string());
49            }
50            out.push_str(" 0");
51            for &h in &step.hints {
52                out.push(' ');
53                out.push_str(&h.to_string());
54            }
55            out.push_str(" 0\n");
56        }
57        out
58    }
59}
60
61fn dimacs(l: Lit) -> i64 {
62    let v = l.var() as i64 + 1;
63    if l.is_positive() {
64        v
65    } else {
66        -v
67    }
68}
69
70/// The trimmed LRAT refutation of `original` that `learned` (each clause RUP from the formula and the clauses before
71/// it) carries to the empty clause, or `None` when the empty clause is not RUP from them all or a learned clause the
72/// refutation needs is not RUP in its place: the [`derivation`] of the empty clause, after the learned clauses.
73pub fn refutation(num_vars: usize, original: &[Vec<Lit>], learned: &[Vec<Lit>]) -> Option<Lrat> {
74    let mut log = learned.to_vec();
75    log.push(Vec::new());
76    derivation(num_vars, original, &log, &[learned.len()])
77}
78
79/// The trimmed LRAT derivation of the clauses of `log` that `targets` names (by index) from `original`, every clause of
80/// `log` RUP from the formula and the clauses before it: a step for each target and for each log clause a step it
81/// leans on needs, in log order, the `j`-th log clause numbered after the formula's. `None` when a target, or a clause
82/// one needs, is not RUP in its place, or a target names no log clause.
83pub fn derivation(num_vars: usize, original: &[Vec<Lit>], log: &[Vec<Lit>], targets: &[usize]) -> Option<Lrat> {
84    let n = original.len();
85    if original.iter().chain(log).flatten().any(|l| l.var() as usize >= num_vars) || targets.iter().any(|&t| t >= log.len()) {
86        return None;
87    }
88    let mut db = Propagator::new(num_vars, original.iter().chain(log));
89    let mut needed = vec![false; n + log.len()];
90    for &t in targets {
91        needed[n + t] = true;
92    }
93    let mut chains: Vec<Option<Vec<u64>>> = vec![None; log.len()];
94    for j in (0..log.len()).rev() {
95        db.deactivate(n + j);
96        if !needed[n + j] {
97            continue;
98        }
99        let chain = db.chain(&log[j])?;
100        for &h in &chain {
101            needed[(h - 1) as usize] = true;
102        }
103        chains[j] = Some(chain);
104    }
105    let steps = chains
106        .into_iter()
107        .enumerate()
108        .filter_map(|(j, chain)| chain.map(|hints| LratStep { id: (n + 1 + j) as u64, clause: log[j].clone(), hints }))
109        .collect();
110    Some(Lrat { steps })
111}
112
113/// Whether `proof` refutes `original`: every step's id exceeds the one before it (and the formula's), every hint
114/// names a clause already present, every step's hints replay (each unit under the step's negation, the last a
115/// conflict), and a step derives the empty clause. Every literal must lie below `num_vars`.
116pub fn check(num_vars: usize, original: &[Vec<Lit>], proof: &Lrat) -> bool {
117    let in_range = |c: &[Lit]| c.iter().all(|l| (l.var() as usize) < num_vars);
118    if !original.iter().all(|c| in_range(c)) {
119        return false;
120    }
121    let mut db: HashMap<u64, &[Lit]> =
122        original.iter().enumerate().map(|(i, c)| (i as u64 + 1, c.as_slice())).collect();
123    let mut assign: Vec<Option<bool>> = vec![None; num_vars];
124    let mut last = original.len() as u64;
125    for step in &proof.steps {
126        if step.id <= last || !in_range(&step.clause) {
127            return false;
128        }
129        if !replay(&db, &step.clause, &step.hints, &mut assign) {
130            return false;
131        }
132        if step.clause.is_empty() {
133            return true;
134        }
135        db.insert(step.id, &step.clause);
136        last = step.id;
137    }
138    false
139}
140
141/// Whether `proof` derives every clause of `claims` from `original`: every step's id exceeds the one before it (and the
142/// formula's), every hint names a clause already present, every step's hints replay, and each claim, its literals in
143/// any order, is the clause of a step or of the formula. Every literal must lie below `num_vars`.
144pub fn check_derivation(num_vars: usize, original: &[Vec<Lit>], proof: &Lrat, claims: &[Vec<Lit>]) -> bool {
145    let in_range = |c: &[Lit]| c.iter().all(|l| (l.var() as usize) < num_vars);
146    if !original.iter().all(|c| in_range(c)) {
147        return false;
148    }
149    let mut db: HashMap<u64, &[Lit]> =
150        original.iter().enumerate().map(|(i, c)| (i as u64 + 1, c.as_slice())).collect();
151    let mut assign: Vec<Option<bool>> = vec![None; num_vars];
152    let mut last = original.len() as u64;
153    for step in &proof.steps {
154        if step.id <= last || !in_range(&step.clause) || !replay(&db, &step.clause, &step.hints, &mut assign) {
155            return false;
156        }
157        db.insert(step.id, &step.clause);
158        last = step.id;
159    }
160    let key = |c: &[Lit]| -> Vec<(u32, bool)> {
161        let mut k: Vec<(u32, bool)> = c.iter().map(|l| (l.var(), l.is_positive())).collect();
162        k.sort_unstable();
163        k.dedup();
164        k
165    };
166    let have: HashSet<Vec<(u32, bool)>> = db.values().map(|c| key(c)).collect();
167    claims.iter().all(|c| have.contains(&key(c)))
168}
169
170/// Replay one step's hints under the negation of `clause`, leaving `assign` cleared.
171fn replay(db: &HashMap<u64, &[Lit]>, clause: &[Lit], hints: &[u64], assign: &mut [Option<bool>]) -> bool {
172    let mut set: Vec<Lit> = Vec::new();
173    let mut verdict = false;
174    'replay: {
175        for &l in clause {
176            let nl = l.negated();
177            if !set_true(assign, nl) {
178                verdict = true;
179                break 'replay;
180            }
181            set.push(nl);
182        }
183        for (i, h) in hints.iter().enumerate() {
184            let Some(c) = db.get(h) else { break 'replay };
185            match clause_state(c, assign) {
186                ClauseState::Conflict => {
187                    verdict = i + 1 == hints.len();
188                    break 'replay;
189                }
190                ClauseState::Unit(u) => {
191                    set_true(assign, u);
192                    set.push(u);
193                }
194                ClauseState::Quiet => break 'replay,
195            }
196        }
197    }
198    for l in set {
199        assign[l.var() as usize] = None;
200    }
201    verdict
202}
203
204/// What a clause is to the propagator once its repeated literals are merged.
205#[derive(Clone, Copy, PartialEq, Eq)]
206enum Shape {
207    Empty,
208    Unit,
209    Watched,
210    Tautology,
211}
212
213/// A clause database for repeated RUP queries: two watched literals a clause, clauses switched off one by one as the
214/// backward walk passes them, every query starting from an empty assignment.
215struct Propagator {
216    /// Each clause with its repeated literals merged; a watched clause keeps its two watches in front.
217    clauses: Vec<Vec<Lit>>,
218    shape: Vec<Shape>,
219    active: Vec<bool>,
220    /// Per literal, the clauses watching it: visited when the literal becomes false.
221    watches: Vec<Vec<usize>>,
222    units: Vec<usize>,
223    empties: Vec<usize>,
224    value: Vec<i8>,
225    /// Per variable, the clause that forced it plus one (0 when assumed or unset).
226    reason: Vec<usize>,
227    /// Per variable, its place on the trail.
228    pos: Vec<usize>,
229    trail: Vec<Lit>,
230    seen: Vec<bool>,
231}
232
233fn widx(l: Lit) -> usize {
234    ((l.var() as usize) << 1) | (!l.is_positive()) as usize
235}
236
237impl Propagator {
238    fn new<'a>(num_vars: usize, clauses: impl Iterator<Item = &'a Vec<Lit>>) -> Propagator {
239        let mut p = Propagator {
240            clauses: Vec::new(),
241            shape: Vec::new(),
242            active: Vec::new(),
243            watches: vec![Vec::new(); num_vars * 2],
244            units: Vec::new(),
245            empties: Vec::new(),
246            value: vec![0; num_vars],
247            reason: vec![0; num_vars],
248            pos: vec![0; num_vars],
249            trail: Vec::new(),
250            seen: vec![false; num_vars],
251        };
252        for c in clauses {
253            let ci = p.clauses.len();
254            let mut lits: Vec<Lit> = Vec::with_capacity(c.len());
255            for &l in c {
256                if !lits.contains(&l) {
257                    lits.push(l);
258                }
259            }
260            let shape = if lits.iter().any(|l| lits.contains(&l.negated())) {
261                Shape::Tautology
262            } else {
263                match lits.len() {
264                    0 => Shape::Empty,
265                    1 => Shape::Unit,
266                    _ => Shape::Watched,
267                }
268            };
269            match shape {
270                Shape::Empty => p.empties.push(ci),
271                Shape::Unit => p.units.push(ci),
272                Shape::Watched => {
273                    p.watches[widx(lits[0])].push(ci);
274                    p.watches[widx(lits[1])].push(ci);
275                }
276                Shape::Tautology => {}
277            }
278            p.clauses.push(lits);
279            p.shape.push(shape);
280            p.active.push(true);
281        }
282        p
283    }
284
285    fn deactivate(&mut self, ci: usize) {
286        self.active[ci] = false;
287    }
288
289    fn val(&self, l: Lit) -> i8 {
290        let v = self.value[l.var() as usize];
291        if l.is_positive() {
292            v
293        } else {
294            -v
295        }
296    }
297
298    fn assign(&mut self, l: Lit, reason: usize) {
299        let v = l.var() as usize;
300        self.value[v] = if l.is_positive() { 1 } else { -1 };
301        self.reason[v] = reason;
302        self.pos[v] = self.trail.len();
303        self.trail.push(l);
304    }
305
306    /// The hint chain that refutes `¬c` over the active clauses, or `None` when propagation stops short of a
307    /// conflict.
308    fn chain(&mut self, c: &[Lit]) -> Option<Vec<u64>> {
309        let result = self.search(c);
310        for i in 0..self.trail.len() {
311            let v = self.trail[i].var() as usize;
312            self.value[v] = 0;
313            self.reason[v] = 0;
314        }
315        self.trail.clear();
316        result
317    }
318
319    fn search(&mut self, c: &[Lit]) -> Option<Vec<u64>> {
320        if let Some(&e) = self.empties.iter().find(|&&e| self.active[e]) {
321            return Some(vec![e as u64 + 1]);
322        }
323        for &l in c {
324            let nl = l.negated();
325            match self.val(nl) {
326                1 => {}
327                -1 => return Some(Vec::new()),
328                _ => self.assign(nl, 0),
329            }
330        }
331        for k in 0..self.units.len() {
332            let ci = self.units[k];
333            if !self.active[ci] {
334                continue;
335            }
336            let u = self.clauses[ci][0];
337            match self.val(u) {
338                1 => {}
339                -1 => return Some(self.explain(ci)),
340                _ => self.assign(u, ci + 1),
341            }
342        }
343        let mut head = 0;
344        while head < self.trail.len() {
345            let falsified = self.trail[head].negated();
346            head += 1;
347            let ws = std::mem::take(&mut self.watches[widx(falsified)]);
348            let mut kept: Vec<usize> = Vec::with_capacity(ws.len());
349            let mut conflict = None;
350            let mut i = 0;
351            while i < ws.len() {
352                let ci = ws[i];
353                i += 1;
354                if !self.active[ci] {
355                    kept.push(ci);
356                    continue;
357                }
358                if self.clauses[ci][0] == falsified {
359                    self.clauses[ci].swap(0, 1);
360                }
361                let first = self.clauses[ci][0];
362                if self.val(first) == 1 {
363                    kept.push(ci);
364                    continue;
365                }
366                let replacement = (2..self.clauses[ci].len()).find(|&k| self.val(self.clauses[ci][k]) != -1);
367                if let Some(k) = replacement {
368                    self.clauses[ci].swap(1, k);
369                    let w = widx(self.clauses[ci][1]);
370                    self.watches[w].push(ci);
371                    continue;
372                }
373                kept.push(ci);
374                if self.val(first) == -1 {
375                    conflict = Some(ci);
376                    break;
377                }
378                self.assign(first, ci + 1);
379            }
380            kept.extend_from_slice(&ws[i..]);
381            self.watches[widx(falsified)] = kept;
382            if let Some(ci) = conflict {
383                return Some(self.explain(ci));
384            }
385        }
386        None
387    }
388
389    /// The reasons behind every literal of the conflict clause `ci`, in trail order, then `ci` itself.
390    fn explain(&mut self, ci: usize) -> Vec<u64> {
391        let mut needed: Vec<(usize, usize)> = Vec::new();
392        let mut stack: Vec<usize> = self.clauses[ci].iter().map(|l| l.var() as usize).collect();
393        let mut marked: Vec<usize> = Vec::new();
394        while let Some(v) = stack.pop() {
395            if self.seen[v] {
396                continue;
397            }
398            self.seen[v] = true;
399            marked.push(v);
400            let r = self.reason[v];
401            if r != 0 {
402                needed.push((self.pos[v], r - 1));
403                stack.extend(self.clauses[r - 1].iter().map(|l| l.var() as usize));
404            }
405        }
406        for v in marked {
407            self.seen[v] = false;
408        }
409        needed.sort_unstable();
410        let mut chain: Vec<u64> = needed.into_iter().map(|(_, r)| r as u64 + 1).collect();
411        chain.push(ci as u64 + 1);
412        chain
413    }
414}
415
416#[cfg(test)]
417#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/lrat/tests.rs"]
418mod tests;
logicaffeine_proof/lrat.rs

logicaffeine_proof/
lrat.rs
