sat_solver/sat/
propagation.rs

1#![warn(clippy::all, clippy::pedantic, clippy::nursery, clippy::cargo)]
2//! Defines traits and implementations for literal propagation in a SAT solver.
3//!
4//! Propagation is the process of deducing new assignments based on the current
5//! partial assignment and the clauses of the formula. The most common form is
6//! Unit Propagation: if a clause becomes unit (all but one of its literals are
7//! false, and the remaining one is unassigned), then that remaining literal
8//! must be assigned true to satisfy the clause.
9//!
10//! This module provides:
11//! - The `Propagator` trait, defining a common interface for different propagation strategies.
12//! - `WatchedLiterals`: An efficient implementation of unit propagation using the
13//!   watched literals scheme. Each clause watches two of its non-false literals.
14//!   Propagation only needs to occur when one of these watched literals becomes false.
15//! - `UnitSearch`: A simpler, less optimised propagator that iterates through all clauses
16//!   to find unit clauses or conflicts.
17//! - `UnitPropagationWithPureLiterals`: A propagator that combines unit propagation
18//!   with the heuristic of assigning pure literals (literals that appear with only
19//!   one polarity in the remaining active formula).
20
21use crate::sat::assignment::Assignment;
22use crate::sat::clause::Clause;
23use crate::sat::clause_storage::LiteralStorage;
24use crate::sat::cnf::Cnf;
25use crate::sat::literal::Literal;
26use crate::sat::literal::Variable;
27use crate::sat::preprocessing::PureLiteralElimination;
28use crate::sat::trail::{Reason, Trail};
29use clap::ValueEnum;
30use itertools::Itertools;
31use smallvec::SmallVec;
32use std::fmt::{Debug, Display};
33use std::marker::PhantomData;
34use std::ops::{Index, IndexMut};
35
36/// Trait defining the interface for a literal propagation mechanism.
37///
38/// Implementors of this trait are responsible for identifying and applying
39/// consequences of the current partial assignment (e.g. unit propagation).
40///
41/// # Type Parameters
42///
43/// * `L`: The `Literal` type.
44/// * `S`: The `LiteralStorage` type for clauses.
45/// * `A`: The `Assignment` type managing variable states.
46pub trait Propagator<L: Literal, S: LiteralStorage<L>, A: Assignment>: Debug + Clone {
47    /// Creates a new propagator instance
48    ///
49    /// # Arguments
50    ///
51    /// * `cnf`: A reference to the `Cnf` formula.
52    fn new(cnf: &Cnf<L, S>) -> Self;
53
54    /// Informs the propagator about a new clause being added to the formula.
55    /// This is particularly relevant for watched literal schemes to set up watches.
56    ///
57    /// # Arguments
58    ///
59    /// * `clause`: The clause being added.
60    /// * `idx`: The index of the clause in the `Cnf`'s clause list.
61    fn add_clause(&mut self, clause: &Clause<L, S>, idx: usize);
62
63    /// Performs propagation based on the current assignments in the `trail`.
64    ///
65    /// It iterates through newly assigned literals on the `trail` (those not yet processed
66    /// by `propagate`) and deduces further assignments. Enqueued assignments are added
67    /// to the `trail` and `assignment` state.
68    ///
69    /// # Arguments
70    ///
71    /// * `trail`: Mutable reference to the `Trail`, where new propagations are enqueued.
72    /// * `assignment`: Mutable reference to the `Assignment` state.
73    /// * `cnf`: Mutable reference to the `Cnf` formula (e.g. for clause access, modification for watched literals).
74    ///
75    /// # Returns
76    ///
77    /// - `Some(clause_idx)` if a conflict is detected (clause at `clause_idx` is falsified).
78    /// - `None` if propagation completes without conflict.
79    fn propagate(
80        &mut self,
81        trail: &mut Trail<L, S>,
82        assignment: &mut A,
83        cnf: &mut Cnf<L, S>,
84    ) -> Option<usize>;
85
86    /// Returns the total number of propagations performed by this instance.
87    fn num_propagations(&self) -> usize;
88
89    /// Helper function to add a propagated literal to the trail.
90    ///
91    /// This is a static method often used by propagator implementations.
92    /// The propagated literal is assigned at the current decision level of the trail.
93    ///
94    /// # Arguments
95    ///
96    /// * `lit`: The literal being propagated.
97    /// * `clause_idx`: The index of the clause that forced this propagation (the reason).
98    /// * `trail`: Mutable reference to the `Trail`.
99    fn add_propagation(lit: L, clause_idx: usize, trail: &mut Trail<L, S>) {
100        trail.push(lit, trail.decision_level(), Reason::Clause(clause_idx));
101    }
102
103    /// Cleans up internal propagator state related to learnt clauses.
104    ///
105    /// When learnt clauses are removed or re-indexed during clause database cleaning,
106    /// the propagator (especially watched literals) needs to update its references.
107    ///
108    /// # Arguments
109    ///
110    /// * `learnt_idx`: An index used to determine which watches to clean. For example,
111    ///   watches to clauses with indices `>= learnt_idx` might be removed if
112    ///   that part of the clause database was rebuilt.
113    fn cleanup_learnt(&mut self, learnt_idx: usize);
114}
115
116/// Implements unit propagation using the watched literals scheme (also known as two-watched literals or 2WL).
117#[derive(Debug, Clone, PartialEq, Eq, Default)]
118pub struct WatchedLiterals<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize = 8> {
119    watches: Vec<SmallVec<[usize; N]>>,
120    num_propagations: usize,
121    marker: PhantomData<*const (L, S, A)>,
122}
123
124impl<L: Literal, S: LiteralStorage<L> + Debug, A: Assignment, const N: usize> Propagator<L, S, A>
125    for WatchedLiterals<L, S, A, N>
126{
127    fn new(cnf: &Cnf<L, S>) -> Self {
128        let num_literal_indices = if cnf.num_vars == 0 {
129            0
130        } else {
131            cnf.num_vars * 2
132        };
133        let st = vec![SmallVec::new(); num_literal_indices];
134
135        let mut wl = Self {
136            watches: st,
137            num_propagations: 0,
138            marker: PhantomData,
139        };
140
141        for (i, clause) in cnf
142            .iter()
143            .enumerate()
144            .filter(|(_, c)| c.len() >= 2 && !c.is_unit() && !c.is_deleted())
145        {
146            wl.add_clause(clause, i);
147        }
148        wl
149    }
150
151    fn add_clause(&mut self, clause: &Clause<L, S>, idx: usize) {
152        if clause.len() < 2 || clause.is_deleted() {
153            return;
154        }
155        let a = clause[0];
156        let b = clause[1];
157        debug_assert_ne!(
158            a.variable(),
159            b.variable(),
160            "Clause {idx}: Attempting to watch two \
161        literals of the same variable: {a:?} and {b:?}"
162        );
163
164        self[a].push(idx);
165        self[b].push(idx);
166    }
167
168    fn propagate(
169        &mut self,
170        trail: &mut Trail<L, S>,
171        assignment: &mut A,
172        cnf: &mut Cnf<L, S>,
173    ) -> Option<usize> {
174        while trail.curr_idx < trail.len() {
175            let lit = trail[trail.curr_idx].lit;
176            trail.curr_idx = trail.curr_idx.wrapping_add(1);
177            assignment.assign(lit);
178            self.num_propagations = self.num_propagations.wrapping_add(1);
179
180            let watch_list_clone = self[lit.negated().index()].clone();
181            if let Some(idx) = self.propagate_watch(&watch_list_clone, trail, assignment, cnf) {
182                return Some(idx);
183            }
184        }
185        None
186    }
187
188    fn num_propagations(&self) -> usize {
189        self.num_propagations
190    }
191
192    fn cleanup_learnt(&mut self, learnt_idx: usize) {
193        for i in &mut self.watches {
194            i.retain(|&mut j| j < learnt_idx);
195        }
196    }
197}
198
199impl<L: Literal, S: LiteralStorage<L> + Debug, A: Assignment, const N: usize>
200    WatchedLiterals<L, S, A, N>
201{
202    /// Propagates watches for the given indices.
203    /// /// This method iterates through the provided indices and processes each clause
204    /// using `process_clause`. If a clause is found to be falsified, it returns the index
205    /// of that clause.
206    ///
207    /// # Arguments
208    /// * `indices`: A slice of indices representing the clauses to process.
209    /// * `trail`: A mutable reference to the `Trail` where new propagations are added.
210    /// * `assignment`: A reference to the current `Assignment` state.
211    /// * `cnf`: A mutable reference to the `Cnf` formula containing the clauses.
212    ///
213    /// # Returns
214    /// * `Some(usize)`: If a clause is found to be falsified, returns the index of that clause.
215    /// * `None`: If no clauses are falsified, returns `None`.
216    pub fn propagate_watch(
217        &mut self,
218        indices: &[usize],
219        trail: &mut Trail<L, S>,
220        assignment: &A,
221        cnf: &mut Cnf<L, S>,
222    ) -> Option<usize> {
223        indices
224            .iter()
225            .find_map(|&idx| self.process_clause(idx, trail, assignment, cnf))
226    }
227
228    /// Processes a clause by checking the values of its watched literals.
229    /// This method checks the first two literals of the clause and determines
230    /// the outcome based on their values:
231    /// - If the first literal is true, the clause is satisfied, and no further action is needed.
232    /// - If both literals are false, the clause is falsified, and its index is returned.
233    /// - If the first literal is unassigned, it is handled by calling `handle_false`.
234    /// - If the second literal is unassigned, it is swapped with the first literal,
235    ///   and `handle_false` is called for the second literal.
236    ///
237    /// # Arguments
238    ///
239    /// * `clause_idx`: The index of the clause to process.
240    /// * `trail`: A mutable reference to the `Trail` where new propagations are added.
241    /// * `assignment`: A reference to the current `Assignment` state.
242    /// * `cnf`: A mutable reference to the `Cnf` formula containing the clauses.
243    ///
244    /// # Returns
245    ///
246    /// * `Some(usize)`: If the clause is found to be falsified, returns the index of that clause.
247    /// * `None`: If the clause is satisfied or not falsified, returns `None`.
248    pub fn process_clause(
249        &mut self,
250        clause_idx: usize,
251        trail: &mut Trail<L, S>,
252        assignment: &A,
253        cnf: &mut Cnf<L, S>,
254    ) -> Option<usize> {
255        let clause = &mut cnf[clause_idx];
256
257        let first = clause[0];
258        let second = clause[1];
259
260        let first_value = assignment.literal_value(first);
261
262        if first_value == Some(true) {
263            return None;
264        }
265
266        let second_value = assignment.literal_value(second);
267
268        match (first_value, second_value) {
269            (Some(false), Some(false)) => {
270                debug_assert!(
271                    clause
272                        .iter()
273                        .all(|&l| assignment.literal_value(l) == Some(false)),
274                    "Clause: {clause:?} is not false, Values: {:?}, idx: {clause_idx}, trail: \
275                    {:?}",
276                    clause
277                        .iter()
278                        .map(|&l| assignment.literal_value(l))
279                        .collect_vec(),
280                    trail,
281                );
282                Some(clause_idx)
283            }
284            (None, Some(false)) => {
285                self.handle_false(first, clause_idx, assignment, cnf, trail);
286                None
287            }
288            (Some(false), None) => {
289                clause.swap(0, 1);
290                self.handle_false(second, clause_idx, assignment, cnf, trail);
291                None
292            }
293            (_, Some(true)) => {
294                clause.swap(0, 1);
295                None
296            }
297            (Some(true), _) | (None, None) => None,
298        }
299    }
300
301    fn handle_false(
302        &mut self,
303        other_lit: L,
304        clause_idx: usize,
305        assignment: &A,
306        cnf: &mut Cnf<L, S>,
307        trail: &mut Trail<L, S>,
308    ) {
309        if let Some(new_lit_idx) = Self::find_new_watch(clause_idx, cnf, assignment) {
310            self.handle_new_watch(clause_idx, new_lit_idx, cnf);
311        } else {
312            debug_assert!(
313                assignment.literal_value(other_lit).is_none(),
314                "In handle_false, \
315            other_lit ({other_lit:?}) was expected to be unassigned but is {:?}. Clause idx \
316            {clause_idx}",
317                assignment.literal_value(other_lit)
318            );
319            Self::add_propagation(other_lit, clause_idx, trail);
320        }
321    }
322
323    fn find_new_watch(clause_idx: usize, cnf: &Cnf<L, S>, assignment: &A) -> Option<usize> {
324        let clause = &cnf[clause_idx];
325        clause
326            .iter()
327            .skip(2)
328            .position(|&l| assignment.literal_value(l) != Some(false))
329            .map(|i| i.wrapping_add(2))
330    }
331
332    fn handle_new_watch(&mut self, clause_idx: usize, new_lit_idx: usize, cnf: &mut Cnf<L, S>) {
333        debug_assert!(new_lit_idx >= 2);
334
335        let new_lit = cnf[clause_idx][new_lit_idx];
336        let prev_lit = cnf[clause_idx][1];
337
338        cnf[clause_idx].swap(1, new_lit_idx);
339
340        self[new_lit].push(clause_idx);
341
342        if let Some(pos) = self[prev_lit].iter().position(|&i| i == clause_idx) {
343            self[prev_lit].swap_remove(pos);
344        }
345    }
346}
347
348impl<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize> Index<usize>
349    for WatchedLiterals<L, S, A, N>
350{
351    type Output = SmallVec<[usize; N]>;
352    #[inline]
353    fn index(&self, index: usize) -> &Self::Output {
354        unsafe { self.watches.get_unchecked(index) }
355    }
356}
357
358impl<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize> IndexMut<usize>
359    for WatchedLiterals<L, S, A, N>
360{
361    #[inline]
362    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
363        unsafe { self.watches.get_unchecked_mut(index) }
364    }
365}
366
367impl<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize> Index<Variable>
368    for WatchedLiterals<L, S, A, N>
369{
370    type Output = SmallVec<[usize; N]>;
371    #[inline]
372    fn index(&self, index: Variable) -> &Self::Output {
373        &self[index as usize]
374    }
375}
376
377impl<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize> IndexMut<Variable>
378    for WatchedLiterals<L, S, A, N>
379{
380    #[inline]
381    fn index_mut(&mut self, index: Variable) -> &mut Self::Output {
382        &mut self[index as usize]
383    }
384}
385
386impl<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize> Index<L>
387    for WatchedLiterals<L, S, A, N>
388{
389    type Output = SmallVec<[usize; N]>;
390    #[inline]
391    fn index(&self, index: L) -> &Self::Output {
392        &self[index.index()]
393    }
394}
395
396impl<L: Literal, S: LiteralStorage<L>, A: Assignment, const N: usize> IndexMut<L>
397    for WatchedLiterals<L, S, A, N>
398{
399    #[inline]
400    fn index_mut(&mut self, index: L) -> &mut Self::Output {
401        &mut self[index.index()]
402    }
403}
404
405/// A simple unit propagation strategy that iterates through all clauses.
406#[derive(Debug, Clone, PartialEq, Eq, Default)]
407pub struct UnitSearch<L: Literal, S: LiteralStorage<L>, A: Assignment>(
408    usize, // num_propagations
409    PhantomData<(L, S, A)>,
410);
411
412impl<L: Literal, S: LiteralStorage<L>, A: Assignment> Propagator<L, S, A> for UnitSearch<L, S, A> {
413    fn new(_: &Cnf<L, S>) -> Self {
414        Self(0, PhantomData)
415    }
416
417    fn add_clause(&mut self, _: &Clause<L, S>, _: usize) {}
418
419    fn propagate(
420        &mut self,
421        trail: &mut Trail<L, S>,
422        assignment: &mut A,
423        cnf: &mut Cnf<L, S>,
424    ) -> Option<usize> {
425        loop {
426            let mut new_propagations_this_scan = false;
427            while trail.curr_idx < trail.len() {
428                let lit = trail[trail.curr_idx].lit;
429                trail.curr_idx = trail.curr_idx.wrapping_add(1);
430                assignment.assign(lit);
431                self.0 = self.0.wrapping_add(1);
432            }
433
434            match Self::process_cnf_scan(trail, assignment, cnf) {
435                Some(ScanResult::Conflict(idx)) => return Some(idx),
436                Some(ScanResult::Propagated) => new_propagations_this_scan = true,
437                None => {}
438            }
439
440            if !new_propagations_this_scan && trail.curr_idx == trail.len() {
441                return None;
442            }
443        }
444    }
445
446    fn num_propagations(&self) -> usize {
447        self.0
448    }
449
450    fn cleanup_learnt(&mut self, _: usize) {}
451}
452
453enum UnitSearchResult<L: Literal> {
454    Unsat(usize),
455    Unit(L),
456    Continue,
457}
458
459enum ScanResult {
460    Conflict(usize),
461    Propagated,
462}
463
464impl<L: Literal, S: LiteralStorage<L>, A: Assignment> UnitSearch<L, S, A> {
465    fn process_cnf_scan(
466        trail: &mut Trail<L, S>,
467        assignment: &A,
468        cnf: &Cnf<L, S>,
469    ) -> Option<ScanResult> {
470        let mut propagated_in_scan = false;
471        for (idx, clause) in cnf.iter().enumerate() {
472            if clause.is_deleted() {
473                continue;
474            }
475            match Self::process_clause_eval(clause, assignment, idx) {
476                UnitSearchResult::Unsat(idx) => return Some(ScanResult::Conflict(idx)),
477                UnitSearchResult::Unit(lit) => {
478                    if assignment.var_value(lit.variable()).is_none() {
479                        Self::add_propagation(lit, idx, trail);
480                        propagated_in_scan = true;
481                    }
482                }
483                UnitSearchResult::Continue => {}
484            }
485        }
486        if propagated_in_scan {
487            Some(ScanResult::Propagated)
488        } else {
489            None
490        }
491    }
492
493    fn process_clause_eval(
494        clause: &Clause<L, S>,
495        assignment: &A,
496        idx: usize,
497    ) -> UnitSearchResult<L> {
498        let mut unassigned_lit_opt = None;
499        let mut num_unassigned = 0;
500
501        for &lit in clause.iter() {
502            match assignment.literal_value(lit) {
503                Some(true) => return UnitSearchResult::Continue,
504                Some(false) => {}
505                None => {
506                    num_unassigned += 1;
507                    if unassigned_lit_opt.is_none() {
508                        unassigned_lit_opt = Some(lit);
509                    }
510                    if num_unassigned > 1 {
511                        return UnitSearchResult::Continue;
512                    }
513                }
514            }
515        }
516
517        if num_unassigned == 1 {
518            UnitSearchResult::Unit(
519                unassigned_lit_opt
520                    .expect("num_unassigned is 1, so unassigned_lit_opt must be Some"),
521            )
522        } else if num_unassigned == 0 {
523            UnitSearchResult::Unsat(idx)
524        } else {
525            UnitSearchResult::Continue
526        }
527    }
528}
529
530/// A propagator that combines `UnitSearch` with periodic pure literal assignment.
531#[derive(Debug, Clone, PartialEq, Eq, Default)]
532pub struct UnitPropagationWithPureLiterals<L: Literal, S: LiteralStorage<L>, A: Assignment>(
533    UnitSearch<L, S, A>,
534);
535
536impl<L: Literal, S: LiteralStorage<L>, A: Assignment> Propagator<L, S, A>
537    for UnitPropagationWithPureLiterals<L, S, A>
538{
539    fn new(cnf: &Cnf<L, S>) -> Self {
540        Self(UnitSearch::new(cnf))
541    }
542
543    fn add_clause(&mut self, clause: &Clause<L, S>, idx: usize) {
544        self.0.add_clause(clause, idx);
545    }
546
547    fn propagate(
548        &mut self,
549        trail: &mut Trail<L, S>,
550        assignment: &mut A,
551        cnf: &mut Cnf<L, S>,
552    ) -> Option<usize> {
553        loop {
554            if let Some(idx) = self.0.propagate(trail, assignment, cnf) {
555                return Some(idx);
556            }
557
558            let trail_len_before_pures = trail.len();
559            let curr_idx_before_pures = trail.curr_idx;
560
561            Self::find_pure_literals_assign(trail, assignment, cnf);
562
563            if curr_idx_before_pures == trail.len() && trail_len_before_pures == trail.len() {
564                return None;
565            }
566        }
567    }
568
569    fn num_propagations(&self) -> usize {
570        self.0.num_propagations()
571    }
572
573    fn cleanup_learnt(&mut self, learnt_idx: usize) {
574        self.0.cleanup_learnt(learnt_idx);
575    }
576}
577
578impl<L: Literal, S: LiteralStorage<L>, A: Assignment> UnitPropagationWithPureLiterals<L, S, A> {
579    fn find_pure_literals_assign(trail: &mut Trail<L, S>, assignment: &A, cnf: &Cnf<L, S>) {
580        let pures = PureLiteralElimination::find_pures(&cnf.clauses);
581        for &lit in &pures {
582            if assignment.var_value(lit.variable()).is_none() {
583                Self::add_propagation(lit, 0, trail);
584            }
585        }
586    }
587}
588
589/// Enum representing different propagator implementations.
590#[derive(Debug, Clone, PartialEq, Eq)]
591pub enum PropagatorImpls<L: Literal, S: LiteralStorage<L>, A: Assignment> {
592    /// Watched literals propagator.
593    WatchedLiterals(WatchedLiterals<L, S, A>),
594    /// Unit search propagator.
595    UnitSearch(UnitSearch<L, S, A>),
596    /// Unit propagation with pure literals propagator.
597    UnitPropagationWithPureLiterals(UnitPropagationWithPureLiterals<L, S, A>),
598}
599
600impl<L: Literal, S: LiteralStorage<L>, A: Assignment> Propagator<L, S, A>
601    for PropagatorImpls<L, S, A>
602{
603    fn new(cnf: &Cnf<L, S>) -> Self {
604        Self::WatchedLiterals(WatchedLiterals::new(cnf))
605    }
606
607    fn add_clause(&mut self, clause: &Clause<L, S>, idx: usize) {
608        match self {
609            Self::WatchedLiterals(wl) => wl.add_clause(clause, idx),
610            Self::UnitSearch(us) => us.add_clause(clause, idx),
611            Self::UnitPropagationWithPureLiterals(up) => up.add_clause(clause, idx),
612        }
613    }
614
615    fn propagate(
616        &mut self,
617        trail: &mut Trail<L, S>,
618        assignment: &mut A,
619        cnf: &mut Cnf<L, S>,
620    ) -> Option<usize> {
621        match self {
622            Self::WatchedLiterals(wl) => wl.propagate(trail, assignment, cnf),
623            Self::UnitSearch(us) => us.propagate(trail, assignment, cnf),
624            Self::UnitPropagationWithPureLiterals(up) => up.propagate(trail, assignment, cnf),
625        }
626    }
627
628    fn num_propagations(&self) -> usize {
629        match self {
630            Self::WatchedLiterals(wl) => wl.num_propagations(),
631            Self::UnitSearch(us) => us.num_propagations(),
632            Self::UnitPropagationWithPureLiterals(up) => up.num_propagations(),
633        }
634    }
635
636    fn cleanup_learnt(&mut self, learnt_idx: usize) {
637        match self {
638            Self::WatchedLiterals(wl) => wl.cleanup_learnt(learnt_idx),
639            Self::UnitSearch(us) => us.cleanup_learnt(learnt_idx),
640            Self::UnitPropagationWithPureLiterals(up) => up.cleanup_learnt(learnt_idx),
641        }
642    }
643}
644
645/// Enum representing the type of propagator to use in the SAT solver.
646#[derive(Debug, Clone, PartialEq, Eq, Copy, Hash, Default, ValueEnum)]
647pub enum PropagatorType {
648    /// Watched literals propagator, which uses the watched literals scheme for efficient unit propagation.
649    #[default]
650    WatchedLiterals,
651    /// Unit search propagator, which iterates through clauses to find unit clauses.
652    UnitSearch,
653    /// Unit propagation with pure literals, which combines unit propagation with the heuristic of assigning pure literals.
654    UnitPropagationWithPureLiterals,
655}
656
657impl Display for PropagatorType {
658    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
659        match self {
660            Self::WatchedLiterals => write!(f, "watched-literals"),
661            Self::UnitSearch => write!(f, "unit-search"),
662            Self::UnitPropagationWithPureLiterals => {
663                write!(f, "unit-propagation-with-pure-literals")
664            }
665        }
666    }
667}
668
669impl PropagatorType {
670    /// Converts the `PropagatorType` to a specific propagator implementation.
671    #[must_use]
672    pub fn to_impl<L: Literal, S: LiteralStorage<L>, A: Assignment>(
673        self,
674        cnf: &Cnf<L, S>,
675    ) -> PropagatorImpls<L, S, A> {
676        match self {
677            Self::WatchedLiterals => PropagatorImpls::WatchedLiterals(WatchedLiterals::new(cnf)),
678            Self::UnitSearch => PropagatorImpls::UnitSearch(UnitSearch::new(cnf)),
679            Self::UnitPropagationWithPureLiterals => {
680                PropagatorImpls::UnitPropagationWithPureLiterals(
681                    UnitPropagationWithPureLiterals::new(cnf),
682                )
683            }
684        }
685    }
686}
687
688#[cfg(test)]
689mod tests {
690    use super::*;
691    use crate::sat::assignment::VecAssignment;
692    use crate::sat::literal::PackedLiteral;
693
694    type TestLiteral = PackedLiteral;
695    type TestClauseStorage = SmallVec<[TestLiteral; 8]>;
696    type TestCnf = Cnf<TestLiteral, TestClauseStorage>;
697    type TestAssignment = VecAssignment;
698    type TestTrail = Trail<TestLiteral, TestClauseStorage>;
699
700    fn lit(val: i32) -> TestLiteral {
701        TestLiteral::from_i32(val)
702    }
703
704    fn setup_test_environment(
705        clauses_dimacs: Vec<Vec<i32>>,
706        num_total_vars: usize,
707    ) -> (TestCnf, TestTrail, TestAssignment) {
708        let mut cnf = TestCnf::new(clauses_dimacs);
709        let effective_num_vars = cnf.num_vars.max(num_total_vars);
710        cnf.num_vars = effective_num_vars;
711
712        let trail = TestTrail::new(&cnf.clauses, effective_num_vars);
713        let assignment = TestAssignment::new(effective_num_vars);
714        (cnf, trail, assignment)
715    }
716
717    #[test]
718    fn test_watched_literals_new_and_add_clause() {
719        let (cnf, _trail, _assignment) =
720            setup_test_environment(vec![vec![1, 2, -3], vec![-1, 4]], 5);
721        let propagator = WatchedLiterals::<_, _, TestAssignment>::new(&cnf);
722
723        assert_eq!(propagator.watches.len(), cnf.num_vars * 2);
724
725        assert!(propagator[lit(1)].contains(&0));
726        assert!(propagator[lit(2)].contains(&0));
727        assert!(!propagator[lit(-3)].contains(&0));
728
729        assert!(propagator[lit(-1)].contains(&1));
730        assert!(propagator[lit(4)].contains(&1));
731    }
732
733    #[test]
734    fn test_watched_literals_simple_propagation() {
735        let (mut cnf, mut trail, mut assignment) =
736            setup_test_environment(vec![vec![-1, 2], vec![-2, 3]], 4);
737        let mut propagator = WatchedLiterals::<_, _, TestAssignment>::new(&cnf);
738
739        trail.push(lit(1), 1, Reason::Decision);
740
741        let conflict = propagator.propagate(&mut trail, &mut assignment, &mut cnf);
742        assert!(conflict.is_none());
743
744        assert_eq!(trail.len(), 3);
745        assert_eq!(trail.t[0].lit, lit(1));
746        assert_eq!(trail.t[1].lit, lit(2));
747        assert_eq!(trail.t[1].reason, Reason::Clause(0));
748        assert_eq!(trail.t[2].lit, lit(3));
749        assert_eq!(trail.t[2].reason, Reason::Clause(1));
750
751        assert_eq!(assignment.literal_value(lit(1)), Some(true));
752        assert_eq!(assignment.literal_value(lit(2)), Some(true));
753        assert_eq!(assignment.literal_value(lit(3)), Some(true));
754        assert_eq!(propagator.num_propagations(), 3);
755    }
756
757    #[test]
758    fn test_watched_literals_conflict() {
759        let (mut cnf, mut trail, mut assignment) =
760            setup_test_environment(vec![vec![-1, 2], vec![-1, -2]], 3);
761        let mut propagator = WatchedLiterals::<_, _, TestAssignment>::new(&cnf);
762
763        trail.push(lit(1), 1, Reason::Decision);
764
765        let conflict_idx = propagator.propagate(&mut trail, &mut assignment, &mut cnf);
766        assert!(conflict_idx.is_some());
767        assert_eq!(conflict_idx.unwrap(), 1);
768    }
769
770    #[test]
771    fn test_watched_literals_find_new_watch() {
772        let (mut cnf, mut trail, mut assignment) =
773            setup_test_environment(vec![vec![-1, 2, 3, -4]], 5);
774        let mut propagator = WatchedLiterals::<_, _, TestAssignment>::new(&cnf);
775
776        trail.push(lit(1), 1, Reason::Decision);
777
778        let conflict = propagator.propagate(&mut trail, &mut assignment, &mut cnf);
779        assert!(conflict.is_none());
780
781        assert!(propagator[lit(2)].contains(&0));
782        assert!(propagator[lit(3)].contains(&0));
783        assert!(!propagator[lit(-1)].contains(&0));
784        assert!(!propagator[lit(-4)].contains(&0));
785    }
786
787    #[test]
788    fn test_unit_search_simple_propagation() {
789        let (mut cnf, mut trail, mut assignment) =
790            setup_test_environment(vec![vec![-1, 2], vec![-2, 3]], 4);
791        let mut propagator = UnitSearch::new(&cnf);
792
793        trail.push(lit(1), 1, Reason::Decision);
794        let conflict = propagator.propagate(&mut trail, &mut assignment, &mut cnf);
795
796        assert!(conflict.is_none());
797        assert_eq!(trail.len(), 3);
798        assert_eq!(trail.t[0].lit, lit(1));
799        assert_eq!(trail.t[1].lit, lit(2));
800        assert_eq!(trail.t[2].lit, lit(3));
801        assert_eq!(assignment.var_value(lit(3).variable()), Some(true));
802        assert_eq!(propagator.num_propagations(), 3);
803    }
804
805    #[test]
806    fn test_unit_search_conflict() {
807        let (mut cnf, mut trail, mut assignment) =
808            setup_test_environment(vec![vec![-1, 2], vec![-1, -2]], 3);
809        let mut propagator = UnitSearch::new(&cnf);
810        trail.push(lit(1), 1, Reason::Decision);
811        let conflict_idx = propagator.propagate(&mut trail, &mut assignment, &mut cnf);
812        assert!(conflict_idx.is_some());
813        assert_eq!(conflict_idx.unwrap(), 1);
814    }
815
816    #[test]
817    fn test_unit_prop_with_pures() {
818        let (mut cnf, mut trail, mut assignment) =
819            setup_test_environment(vec![vec![-1, 2], vec![3]], 4);
820        let mut propagator = UnitPropagationWithPureLiterals::new(&cnf);
821
822        trail.push(lit(1), 1, Reason::Decision);
823        let conflict = propagator.propagate(&mut trail, &mut assignment, &mut cnf);
824
825        assert!(conflict.is_none());
826        assert_eq!(trail.len(), 3);
827
828        assert_eq!(assignment.var_value(lit(3).variable()), Some(true));
829    }
830
831    #[test]
832    fn test_watched_literals_empty_cnf() {
833        let (cnf, _trail, _assignment) = setup_test_environment(vec![], 1);
834        let propagator = WatchedLiterals::<_, _, TestAssignment>::new(&cnf);
835        assert_eq!(propagator.watches.len(), 2);
836    }
837
838    #[test]
839    fn test_watched_literals_unit_clause_in_cnf() {
840        let (cnf, _trail, _assignment) = setup_test_environment(vec![vec![1], vec![-2, 3]], 4);
841        let propagator = WatchedLiterals::<_, _, TestAssignment>::new(&cnf);
842        assert!(!propagator[lit(1)].contains(&0));
843        assert!(propagator[lit(-2)].contains(&1));
844        assert!(propagator[lit(3)].contains(&1));
845    }
846}
sat_solver/sat/propagation.rs

sat_solver/sat/
propagation.rs
