csp_solver/solver/
monotonic.rs

1//! Monotonic propagation for lattice domains.
2//!
3//! Specialized fixed-point loop that skips adjacency graph construction
4//! and undo-log overhead. Domains only grow (join/union), so no backtracking
5//! is needed — simple iteration until convergence.
6
7use crate::constraint::{ConstraintEnum, Revision};
8use crate::domain::Domain;
9use crate::variable::Variable;
10use crate::{SolveStats, Unsatisfiable};
11
12/// Propagate constraints over lattice domains to a fixed point.
13///
14/// Unlike AC-3, this doesn't build an adjacency graph or maintain a worklist
15/// with per-constraint membership tracking. Instead, it repeatedly sweeps all
16/// constraints until none produce changes — appropriate when domains are
17/// monotonic (only grow via join) and the constraint graph is small.
18///
19/// Returns `Err(Unsatisfiable)` if a constraint reports unsatisfiable
20/// (shouldn't happen for well-formed lattice CSPs).
21pub(crate) fn propagate_monotonic<D: Domain>(
22    variables: &mut [Variable<D>],
23    constraints: &[ConstraintEnum<D>],
24    stats: &mut SolveStats,
25) -> Result<(), Unsatisfiable>
26where
27    D::Value: PartialEq + 'static,
28{
29    loop {
30        let mut changed = false;
31        for c in constraints {
32            match c.revise(variables, 0) {
33                Revision::Unchanged => {}
34                Revision::Changed => {
35                    changed = true;
36                    stats.propagations += 1;
37                }
38                Revision::Unsatisfiable => return Err(Unsatisfiable),
39            }
40        }
41        if !changed {
42            break;
43        }
44    }
45    Ok(())
46}
csp_solver/solver/monotonic.rs

csp_solver/solver/
monotonic.rs
