csp_solver/solver/
ac3.rs

1//! AC-3 worklist propagation using the adjacency graph.
2//!
3//! Uses a bitset worklist for lower overhead than VecDeque + Vec<bool>.
4
5use crate::adjacency::Adjacency;
6use crate::constraint::{ConstraintEnum, Revision, VarId};
7use crate::domain::Domain;
8use crate::variable::Variable;
9use crate::{SolveStats, Unsatisfiable};
10
11/// A simple bitset worklist — O(1) insert/membership, O(words) scan for next.
12struct BitsetWorklist {
13    words: Vec<u64>,
14}
15
16impl BitsetWorklist {
17    fn new(capacity: usize) -> Self {
18        let num_words = capacity.div_ceil(64);
19        Self {
20            words: vec![0; num_words],
21        }
22    }
23
24    fn new_full(capacity: usize) -> Self {
25        let num_words = capacity.div_ceil(64);
26        let mut words = vec![u64::MAX; num_words];
27        let remainder = capacity % 64;
28        if remainder != 0 && !words.is_empty() {
29            *words.last_mut().unwrap() = (1u64 << remainder) - 1;
30        }
31        Self { words }
32    }
33
34    fn insert(&mut self, idx: usize) {
35        self.words[idx / 64] |= 1u64 << (idx % 64);
36    }
37
38    fn contains(&self, idx: usize) -> bool {
39        self.words[idx / 64] & (1u64 << (idx % 64)) != 0
40    }
41
42    fn pop(&mut self) -> Option<usize> {
43        for (wi, word) in self.words.iter_mut().enumerate() {
44            if *word != 0 {
45                let bit = word.trailing_zeros() as usize;
46                *word &= *word - 1;
47                return Some(wi * 64 + bit);
48            }
49        }
50        None
51    }
52}
53
54/// Run AC-3 propagation over all constraints.
55///
56/// Returns `Err(Unsatisfiable)` if a domain wipe-out is detected.
57pub fn ac3_full<D: Domain>(
58    variables: &mut [Variable<D>],
59    constraints: &[ConstraintEnum<D>],
60    adjacency: &Adjacency,
61    stats: &mut SolveStats,
62    depth: usize,
63) -> Result<(), Unsatisfiable>
64where
65    D::Value: PartialEq,
66{
67    let mut worklist = BitsetWorklist::new_full(constraints.len());
68
69    while let Some(idx) = worklist.pop() {
70        match constraints[idx].revise(variables, depth) {
71            Revision::Unchanged => {}
72            Revision::Changed => {
73                stats.propagations += 1;
74                for &neighbor in adjacency.neighbors_of_constraint(idx) {
75                    worklist.insert(neighbor as usize);
76                }
77            }
78            Revision::Unsatisfiable => return Err(Unsatisfiable),
79        }
80    }
81
82    Ok(())
83}
84
85/// Run AC-3 propagation seeded from a single variable assignment (MAC).
86pub fn ac3_from_variable<D: Domain>(
87    var: VarId,
88    variables: &mut [Variable<D>],
89    constraints: &[ConstraintEnum<D>],
90    adjacency: &Adjacency,
91    assignment: &[Option<D::Value>],
92    stats: &mut SolveStats,
93    depth: usize,
94) -> bool
95where
96    D::Value: PartialEq,
97{
98    let mut worklist = BitsetWorklist::new(constraints.len());
99
100    for &ci in adjacency.constraints_for(var) {
101        let ci = ci as usize;
102        let scope = constraints[ci].scope();
103        if scope.iter().any(|&v| v != var && assignment[v as usize].is_none()) {
104            worklist.insert(ci);
105        }
106    }
107
108    while let Some(idx) = worklist.pop() {
109        match constraints[idx].revise(variables, depth) {
110            Revision::Unchanged => {}
111            Revision::Changed => {
112                stats.propagations += 1;
113                for &v in constraints[idx].scope() {
114                    if variables[v as usize].domain.is_empty() {
115                        return true;
116                    }
117                }
118                for &neighbor in adjacency.neighbors_of_constraint(idx) {
119                    let n = neighbor as usize;
120                    if !worklist.contains(n) {
121                        let scope = constraints[n].scope();
122                        if scope.iter().any(|&v| assignment[v as usize].is_none()) {
123                            worklist.insert(n);
124                        }
125                    }
126                }
127            }
128            Revision::Unsatisfiable => return true,
129        }
130    }
131
132    false
133}
csp_solver/solver/ac3.rs

csp_solver/solver/
ac3.rs
