sat_solver/sat/
trail.rs

1#![warn(clippy::all, clippy::pedantic, clippy::nursery, clippy::cargo)]
2use crate::sat::assignment::Assignment;
3use crate::sat::clause::Clause;
4use crate::sat::clause_storage::LiteralStorage;
5use crate::sat::literal::Literal;
6use crate::sat::solver::Solutions;
7use itertools::Itertools;
8use rustc_hash::FxHashMap;
9use smallvec::SmallVec;
10use std::marker::PhantomData;
11use std::ops::{Index, IndexMut};
12
13/// The reason for a literal being in the trail.
14///
15/// This enum specifies why a particular literal was assigned.
16#[derive(Debug, Clone, PartialEq, Eq, Default, Copy, Hash, PartialOrd, Ord)]
17pub enum Reason {
18    /// The literal was assigned as a decision by the solver.
19    #[default]
20    Decision,
21    /// The literal was assigned because it was part of an initial unit clause.
22    /// The `usize` stores the index of this unit clause in the original clause database.
23    Unit(usize),
24    /// The literal was assigned due to an implication from another clause.
25    /// The `usize` stores the index of the implying clause.
26    Clause(usize),
27}
28
29/// A step of the trail, representing a single literal assignment.
30///
31/// Each `Part` stores the assigned literal, the decision level at which
32/// it was assigned, and the reason for the assignment.
33#[derive(Debug, Clone, PartialEq, Eq, Default)]
34pub struct Part<L: Literal> {
35    /// The literal that was assigned.
36    pub(crate) lit: L,
37    /// The decision level at which this literal was assigned.
38    /// Level 0 is for pre-assigned literals (e.g. from unit clauses).
39    /// Subsequent levels correspond to solver decisions.
40    decision_level: usize,
41    /// The reason for this literal's assignment.
42    pub(crate) reason: Reason,
43}
44
45/// The trail itself, storing the sequence of assignments and related metadata.
46///
47/// The trail is a fundamental data structure in a CDCL SAT solver. It maintains
48/// the current partial assignment, the reasons for implications, and decision levels.
49/// `L` is the literal type, and `S` is the literal storage type used by clauses.
50#[derive(Debug, Clone, PartialEq, Eq, Default)]
51pub struct Trail<L: Literal, S: LiteralStorage<L>> {
52    /// The sequence of assignments (parts) forming the trail.
53    pub(crate) t: Vec<Part<L>>,
54    /// Index pointing to the next literal to be propagated in `t`.
55    /// Assignments from `t[0]` to `t[curr_idx - 1]` have been processed (propagated).
56    /// Assignments from `t[curr_idx]` onwards are pending propagation.
57    pub curr_idx: usize,
58    /// Maps a variable (by its `u32` ID) to the decision level at which it was assigned.
59    /// `lit_to_level[var_id] = decision_level`.
60    /// Stores 0 if the variable is unassigned or assigned at level 0.
61    lit_to_level: Vec<usize>,
62    /// Maps a variable (by its `u32` ID) to its position (index) in the `t` vector.
63    /// `lit_to_pos[var_id] = index_in_t`.
64    /// Stores 0 if the variable is unassigned (as `t[0]` is a valid position, this relies on
65    /// checking `lit_to_level` or other means to confirm assignment for var at pos 0).
66    /// More accurately, a non-zero value means it's assigned and on the trail.
67    pub lit_to_pos: Vec<usize>,
68    /// `PhantomData` to use the generic type `S` (`LiteralStorage`).
69    marker: PhantomData<*const S>,
70    /// Index separating original (non-learnt) clauses from learnt clauses.
71    /// Clauses with an index less than `cnf_non_learnt_idx` are considered original.
72    /// Clauses with an index greater than or equal to `cnf_non_learnt_idx` are learnt.
73    /// This is used by `remap_clause_indices`.
74    cnf_non_learnt_idx: usize,
75}
76
77impl<L: Literal, S: LiteralStorage<L>> Index<usize> for Trail<L, S> {
78    type Output = Part<L>;
79
80    /// Accesses a `Part` of the trail by its index.
81    ///
82    /// # Panics
83    /// This method will panic if `index` is out of bounds.
84    ///
85    /// # Safety
86    /// The `unsafe` block is used for a potential micro-optimisation by using
87    /// `get_unchecked`.
88    fn index(&self, index: usize) -> &Self::Output {
89        unsafe { self.t.get_unchecked(index) }
90    }
91}
92
93impl<L: Literal, S: LiteralStorage<L>> IndexMut<usize> for Trail<L, S> {
94    /// Mutably accesses a `Part` of the trail by its index.
95    ///
96    /// # Panics
97    /// This method will panic if `index` is out of bounds.
98    ///
99    /// # Safety
100    /// Similar to `Index::index`, this uses `get_unchecked_mut`.
101    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
102        unsafe { self.t.get_unchecked_mut(index) }
103    }
104}
105
106impl<L: Literal, S: LiteralStorage<L>> Trail<L, S> {
107    /// Returns the current decision level.
108    ///
109    /// The decision level is determined by the last assignment on the trail.
110    /// If the trail is empty or only contains assignments at level 0, it returns 0.
111    /// Otherwise, it returns the decision level of the assignment at `curr_idx - 1`.
112    #[must_use]
113    pub fn decision_level(&self) -> usize {
114        if self.curr_idx == 0 {
115            return 0;
116        }
117
118        let index = self.curr_idx - 1;
119        self[index].decision_level
120    }
121
122    /// Returns the total number of assignments currently on the trail.
123    #[must_use]
124    pub const fn len(&self) -> usize {
125        self.t.len()
126    }
127
128    /// Checks if the trail is empty (contains no assignments).
129    #[must_use]
130    pub const fn is_empty(&self) -> bool {
131        self.t.is_empty()
132    }
133
134    /// Returns the decision level at which variable `v` was assigned.
135    /// Returns 0 if the variable is unassigned or was assigned at level 0.
136    ///
137    /// # Safety
138    /// This function uses `get_unchecked` and assumes `v` (cast to `usize`)
139    /// is a valid index into `lit_to_level`. This means `v` must be less than
140    /// `num_vars` used to initialise the `Trail`.
141    #[must_use]
142    pub fn level(&self, v: u32) -> usize {
143        unsafe { *self.lit_to_level.get_unchecked(v as usize) }
144    }
145
146    /// Constructs a `Solutions` object from the current assignments on the trail.
147    /// This represents a complete model if the solver found satisfiability.
148    #[must_use]
149    pub fn solutions(&self) -> Solutions {
150        let literals = self.t.iter().map(|p| p.lit.to_i32()).collect_vec();
151        Solutions::new(&literals)
152    }
153
154    /// Creates a new `Trail`.
155    ///
156    /// Initialises the trail, potentially adding assignments from unit clauses
157    /// found in the initial `clauses` set. These initial assignments are at decision level 0.
158    ///
159    /// # Arguments
160    /// * `clauses`: A slice of initial clauses. Unit clauses from this set will be
161    ///   added to the trail.
162    /// * `num_vars`: The total number of variables in the problem. This is used to
163    ///   size internal mapping vectors.
164    ///
165    /// # Safety
166    /// The internal initialisation of `lit_to_pos` for unit clauses uses `get_unchecked_mut`.
167    /// This is safe if `lit.variable()` from a unit clause is less than `num_vars`.
168    #[must_use]
169    pub fn new(clauses: &[Clause<L, S>], num_vars: usize) -> Self {
170        let mut lit_to_pos = vec![0; num_vars];
171
172        let mut vec = Vec::with_capacity(num_vars);
173
174        vec.extend(
175            clauses
176                .iter()
177                .filter(|c| c.is_unit())
178                .enumerate()
179                .map(|(i, c)| {
180                    let lit = c[0];
181                    unsafe {
182                        *lit_to_pos.get_unchecked_mut(lit.variable() as usize) = i;
183                    }
184
185                    Part {
186                        lit,
187                        decision_level: 0,
188                        reason: Reason::Unit(i),
189                    }
190                }),
191        );
192
193        Self {
194            t: vec,
195            curr_idx: 0,
196            lit_to_level: vec![0; num_vars],
197            lit_to_pos,
198            marker: PhantomData,
199            cnf_non_learnt_idx: clauses.len(),
200        }
201    }
202
203    /// Pushes a new assignment (literal) onto the trail.
204    ///
205    /// If the variable of the literal is already assigned, this function does nothing.
206    /// Otherwise, it adds a new `Part` to the trail and updates `lit_to_level` and `lit_to_pos`.
207    ///
208    /// # Arguments
209    /// * `lit`: The literal being assigned.
210    /// * `decision_level`: The decision level at which this assignment occurs.
211    /// * `reason`: The reason for this assignment.
212    ///
213    /// # Safety
214    /// Uses `get_unchecked` to check `lit_to_pos` and `get_unchecked_mut` to update
215    /// `lit_to_level` and `lit_to_pos`.
216    pub fn push(&mut self, lit: L, decision_level: usize, reason: Reason) {
217        unsafe {
218            if *self.lit_to_pos.get_unchecked(lit.variable() as usize) != 0 {
219                return;
220            }
221        }
222
223        let pos = self.t.len();
224        self.t.push(Part {
225            lit,
226            decision_level,
227            reason,
228        });
229        let var = lit.variable() as usize;
230
231        unsafe {
232            *self.lit_to_level.get_unchecked_mut(var) = decision_level;
233            *self.lit_to_pos.get_unchecked_mut(var) = pos;
234        }
235    }
236
237    /// Resets the trail to an empty state.
238    ///
239    /// Clears all assignments and resets `curr_idx`, `lit_to_level`, and `lit_to_pos`.
240    /// This is used during solver restarts.
241    pub fn reset(&mut self) {
242        self.t.clear();
243        self.curr_idx = 0;
244        self.lit_to_level.fill(0);
245        self.lit_to_pos.fill(0);
246    }
247
248    /// Backtracks assignments to a specified decision level.
249    ///
250    /// Removes all assignments made at decision levels greater than or equal to `level`.
251    /// For each removed assignment, it unassigns the corresponding variable in the `Assignment` object `a`.
252    /// Updates `curr_idx` to point to the new end of the (propagated) trail.
253    ///
254    /// # Arguments
255    /// * `a`: A mutable reference to the `Assignment` object to update.
256    /// * `level`: The decision level to backtrack to. Assignments at this level and higher will be removed.
257    ///
258    /// # Safety
259    /// Uses `get_unchecked` and `get_unchecked_mut` on `lit_to_level` and `lit_to_pos`.
260    /// Assumes variable IDs from `self[i].lit.variable()` are valid indices.
261    pub fn backstep_to<A: Assignment>(&mut self, a: &mut A, level: usize) {
262        let mut truncate_at = 0;
263
264        for i in (0..self.len()).rev() {
265            let var = self[i].lit.variable();
266            unsafe {
267                if *self.lit_to_level.get_unchecked(var as usize) >= level {
268                    a.unassign(var);
269                    *self.lit_to_level.get_unchecked_mut(var as usize) = 0;
270                    *self.lit_to_pos.get_unchecked_mut(var as usize) = 0;
271                } else {
272                    truncate_at = i;
273                    break;
274                }
275            }
276        }
277
278        self.curr_idx = truncate_at;
279        self.t.truncate(truncate_at);
280    }
281
282    /// Returns a list of clause indices that are "locked".
283    ///
284    /// A clause is considered locked if one of its literals is on the trail,
285    /// and that literal was assigned as a result of an implication (i.e. `Reason::Clause`).
286    /// Such clauses cannot be removed during database cleaning if the literal they implied
287    /// is still on the trail, as they are part of the justification for the current assignment.
288    #[must_use]
289    pub fn get_locked_clauses(&self) -> SmallVec<[usize; 16]> {
290        let mut locked = SmallVec::<[usize; 16]>::new();
291        for part in &self.t {
292            if let Reason::Clause(c_ref) = part.reason {
293                locked.push(c_ref);
294            }
295        }
296        locked.sort_unstable();
297        locked.dedup();
298        locked
299    }
300
301    /// Remaps clause indices stored in `Reason::Clause` variants on the trail.
302    ///
303    /// This is necessary after clause database cleanup operations (like removing
304    /// redundant learnt clauses) where clause indices might change.
305    /// Only indices of learnt clauses (those with original index `>= self.cnf_non_learnt_idx`)
306    /// are considered for remapping.
307    ///
308    /// # Arguments
309    /// * `map`: A hash map where keys are old clause indices and values are new clause indices.
310    pub fn remap_clause_indices(&mut self, map: &FxHashMap<usize, usize>) {
311        for part in &mut self.t {
312            if let Reason::Clause(ref mut c_ref) = part.reason {
313                if *c_ref >= self.cnf_non_learnt_idx {
314                    if let Some(new_ref) = map.get(c_ref) {
315                        *c_ref = *new_ref;
316                    }
317                }
318            }
319        }
320    }
321}
322
323#[cfg(test)]
324mod tests {
325    use super::*;
326    use crate::sat::literal::{Literal as LiteralTrait, PackedLiteral};
327
328    const NUM_VARS: usize = 5;
329
330    type MockLit = PackedLiteral;
331    type MockLiteralStorage = SmallVec<[PackedLiteral; 8]>;
332    type MockClause = Clause<MockLit, MockLiteralStorage>;
333
334    #[test]
335    fn test_new_empty() {
336        let clauses: [MockClause; 0] = [];
337        let trail = Trail::<MockLit, MockLiteralStorage>::new(&clauses, NUM_VARS);
338        assert!(trail.is_empty());
339        assert_eq!(trail.curr_idx, 0);
340        assert_eq!(trail.lit_to_level.len(), NUM_VARS);
341        assert_eq!(trail.lit_to_pos.len(), NUM_VARS);
342        assert!(trail.lit_to_level.iter().all(|&lvl| lvl == 0));
343        assert!(trail.lit_to_pos.iter().all(|&pos| pos == 0));
344        assert_eq!(trail.cnf_non_learnt_idx, 0);
345    }
346
347    fn l(lit: i32) -> PackedLiteral {
348        PackedLiteral::from_i32(lit)
349    }
350
351    #[test]
352    fn test_new_with_unit_clauses() {
353        let clauses = [
354            std::iter::once(1).collect::<MockClause>(),
355            std::iter::once(-2).collect::<MockClause>(),
356            [1, 3].into_iter().collect::<MockClause>(),
357        ];
358        let trail = Trail::<MockLit, MockLiteralStorage>::new(&clauses, NUM_VARS);
359
360        assert_eq!(trail.len(), 2);
361        assert_eq!(trail.curr_idx, 0);
362
363        assert_eq!(trail[0].lit, l(1));
364        assert_eq!(trail[0].decision_level, 0);
365        assert_eq!(trail[0].reason, Reason::Unit(0));
366        assert_eq!(trail.level(0), 0);
367        assert_eq!(trail.lit_to_pos[0], 0);
368
369        assert_eq!(trail[1].lit, l(-2));
370        assert_eq!(trail[1].decision_level, 0);
371        assert_eq!(trail[1].reason, Reason::Unit(1));
372        assert_eq!(trail.level(1), 0);
373        assert_eq!(trail.lit_to_pos[1], 0);
374
375        assert_eq!(trail.level(2), 0);
376        assert_eq!(trail.lit_to_pos[2], 1);
377
378        assert_eq!(trail.cnf_non_learnt_idx, 3);
379    }
380
381    #[test]
382    fn test_push_simple() {
383        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
384        trail.reset();
385
386        let lit1 = l(1);
387        trail.push(lit1, 1, Reason::Decision);
388
389        assert_eq!(trail.len(), 1);
390        assert_eq!(trail[0].lit, lit1);
391        assert_eq!(trail[0].decision_level, 1);
392        assert_eq!(trail[0].reason, Reason::Decision);
393        assert_eq!(trail.level(0), 0);
394        assert_eq!(trail.lit_to_pos[0], 0);
395
396        let lit2 = l(-2);
397        trail.push(lit2, 1, Reason::Clause(0));
398
399        assert_eq!(trail.len(), 2);
400        assert_eq!(trail[1].lit, lit2);
401        assert_eq!(trail[1].decision_level, 1);
402        assert_eq!(trail[1].reason, Reason::Clause(0));
403        assert_eq!(trail.level(1), 1);
404        assert_eq!(trail.lit_to_pos[1], 0);
405    }
406
407    #[test]
408    fn test_push_already_assigned_due_to_pos_not_zero() {
409        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
410        trail.reset();
411
412        trail.push(l(1), 1, Reason::Decision);
413        assert_eq!(trail.len(), 1);
414
415        trail.push(l(2), 1, Reason::Decision);
416        assert_eq!(trail.len(), 2);
417        assert_eq!(trail.lit_to_pos[1], 0);
418
419        trail.push(l(2), 1, Reason::Decision);
420        assert_eq!(trail.len(), 2);
421
422        trail.push(l(1), 1, Reason::Decision);
423        assert_eq!(
424            trail.len(),
425            3,
426            "Bug: Re-pushed var 0 because lit_to_pos[0] == 0"
427        );
428    }
429
430    #[test]
431    fn test_decision_level() {
432        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
433        assert_eq!(trail.decision_level(), 0);
434
435        trail.push(l(1), 1, Reason::Decision);
436        trail.curr_idx = 1;
437        assert_eq!(trail.decision_level(), 1);
438
439        trail.push(l(2), 1, Reason::Clause(0));
440        trail.curr_idx = 2;
441        assert_eq!(trail.decision_level(), 1);
442
443        trail.push(l(3), 2, Reason::Decision);
444        trail.curr_idx = 3;
445        assert_eq!(trail.decision_level(), 2);
446
447        trail.curr_idx = 0;
448        assert_eq!(trail.decision_level(), 0);
449    }
450
451    #[test]
452    fn test_len_is_empty() {
453        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
454        assert_eq!(trail.len(), 0);
455        assert!(trail.is_empty());
456
457        trail.push(l(1), 1, Reason::Decision);
458        assert_eq!(trail.len(), 1);
459        assert!(!trail.is_empty());
460    }
461
462    #[test]
463    fn test_level() {
464        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
465        trail.reset();
466
467        assert_eq!(trail.level(0), 0);
468
469        trail.push(l(1), 1, Reason::Decision);
470        assert_eq!(trail.level(0), 0);
471        assert_eq!(trail.level(1), 1);
472
473        trail.push(l(-3), 2, Reason::Decision);
474        assert_eq!(trail.level(2), 0);
475    }
476
477    #[test]
478    fn test_solutions() {
479        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
480        trail.reset();
481
482        let sol_empty = trail.solutions();
483        assert!(sol_empty.is_empty());
484    }
485
486    #[test]
487    fn test_reset() {
488        let clauses = [std::iter::once(1).collect::<MockClause>()];
489        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&clauses, NUM_VARS);
490
491        assert_eq!(trail.len(), 1);
492        assert_eq!(trail.level(0), 0);
493        assert_eq!(trail.lit_to_pos[0], 0);
494
495        trail.push(l(2), 1, Reason::Decision);
496        assert_eq!(trail.len(), 2);
497        assert_eq!(trail.level(1), 0);
498        assert_eq!(trail.lit_to_pos[1], 0);
499
500        trail.reset();
501        assert!(trail.is_empty());
502        assert_eq!(trail.curr_idx, 0);
503        assert!(trail.lit_to_level.iter().all(|&lvl| lvl == 0));
504        assert!(trail.lit_to_pos.iter().all(|&pos| pos == 0));
505    }
506
507    #[test]
508    fn test_remap_clause_indices() {
509        let mut trail = Trail::<MockLit, MockLiteralStorage>::new(&[], NUM_VARS);
510        trail.reset();
511        trail.cnf_non_learnt_idx = 50;
512
513        trail.push(l(1), 1, Reason::Clause(10));
514        trail.push(l(2), 1, Reason::Clause(100));
515        trail.push(l(3), 1, Reason::Clause(101));
516        trail.push(l(4), 1, Reason::Clause(102));
517
518        let mut map = FxHashMap::default();
519        map.insert(100, 70);
520        map.insert(101, 71);
521
522        trail.remap_clause_indices(&map);
523
524        assert_eq!(trail[0].reason, Reason::Clause(10));
525        assert_eq!(trail[1].reason, Reason::Clause(70));
526        assert_eq!(trail[2].reason, Reason::Clause(71));
527        assert_eq!(trail[3].reason, Reason::Clause(102));
528    }
529}
sat_solver/sat/trail.rs

sat_solver/sat/
trail.rs
