csp_solver/constraint/
all_different_except.rs

1//! N-ary all-different constraint with a sentinel escape value.
2//!
3//! Tests: `tests/all_different_except.rs`.
4//!
5//! Parallel to [`AllDifferent`](super::all_different::AllDifferent) but permits
6//! arbitrarily many variables to share a single *sentinel* value — useful for
7//! modelling partial bipartite assignment, where a dedicated "unmatched" token
8//! may be selected by any number of sources simultaneously while every other
9//! (real) target must still be picked at most once.
10//!
11//! ```no_run
12//! use csp_solver::constraint::AllDifferentExcept;
13//! use csp_solver::domain::BitsetDomain;
14//! use csp_solver::Csp;
15//!
16//! // Four variables, each picking a target in 0..4. Value `0` is the
17//! // "unmatched" sentinel — any number of variables may land on it.
18//! let mut csp: Csp<BitsetDomain> = Csp::new();
19//! let vars = csp.add_variables(&BitsetDomain::range(4), 4);
20//! csp.add_constraint_enum(
21//!     csp_solver::constraint::ConstraintEnum::AllDifferentExcept(
22//!         AllDifferentExcept::new(vars, 0),
23//!     ),
24//! );
25//! csp.finalize();
26//! ```
27
28use crate::domain::Domain;
29use crate::variable::Variable;
30
31use super::traits::{Constraint, Revision, VarId};
32
33/// All-different over the scope, *except* that the configured `sentinel`
34/// value may be assigned to any number of variables.
35///
36/// Non-sentinel assignments must remain pairwise distinct.
37#[derive(Debug)]
38pub struct AllDifferentExcept<V: Clone + PartialEq + std::fmt::Debug> {
39    pub(crate) scope: Vec<VarId>,
40    pub(crate) sentinel: V,
41    /// Stable per-constraint id keying the GAC matching warm-start cache.
42    gac_id: u32,
43}
44
45impl<V: Clone + PartialEq + std::fmt::Debug> AllDifferentExcept<V> {
46    /// Create a new all-different-except constraint over `vars`, treating
47    /// `sentinel` as the escape value that may be reused without conflict.
48    pub fn new(vars: Vec<VarId>, sentinel: V) -> Self {
49        Self {
50            scope: vars,
51            sentinel,
52            gac_id: crate::solver::gac::next_gac_id(),
53        }
54    }
55
56    pub(crate) fn check_impl(&self, assignment: &[Option<V>]) -> bool {
57        // Collect non-sentinel assigned values; sentinel assignments are
58        // elided entirely so they never participate in the pairwise test.
59        let assigned: Vec<&V> = self
60            .scope
61            .iter()
62            .filter_map(|&v| assignment[v as usize].as_ref())
63            .filter(|val| **val != self.sentinel)
64            .collect();
65        for i in 0..assigned.len() {
66            for j in (i + 1)..assigned.len() {
67                if assigned[i] == assigned[j] {
68                    return false;
69                }
70            }
71        }
72        true
73    }
74
75    /// Prune non-sentinel values from peer domains.
76    ///
77    /// For small scopes (< 4 variables), uses fast singleton removal:
78    /// a variable pinned to the sentinel does not forbid peers from
79    /// choosing the sentinel themselves, while non-sentinel singletons
80    /// behave exactly like [`AllDifferent`](super::all_different::AllDifferent).
81    ///
82    /// For larger scopes (≥ 4), delegates to Régin's GAC algorithm
83    /// ([`propagate_gac_core`](crate::solver::gac::propagate_gac_core) with
84    /// the sentinel supplied), which achieves generalized arc consistency by
85    /// building a bipartite matching graph over non-sentinel values and
86    /// pruning values that cannot participate in any maximum matching.
87    pub(crate) fn revise_impl<D>(&self, vars: &mut [Variable<D>], depth: usize) -> Revision
88    where
89        D: Domain<Value = V>,
90        V: 'static,
91    {
92        // For larger scopes, GAC provides strictly stronger pruning than
93        // singleton removal — it detects Hall sets and matching failures
94        // that pairwise checks miss. The matching is warm-started across calls
95        // via the constraint's cache id.
96        if self.scope.len() >= 4 {
97            return crate::solver::gac::propagate_gac_core(
98                &self.scope,
99                Some(&self.sentinel),
100                vars,
101                depth,
102                Some(self.gac_id),
103            );
104        }
105
106        // Small scope: singleton removal is fast and sufficient.
107        let mut changed = false;
108        let singletons: Vec<(VarId, D::Value)> = self
109            .scope
110            .iter()
111            .filter_map(|&v| {
112                vars[v as usize]
113                    .domain
114                    .singleton_value()
115                    .map(|val| (v, val))
116            })
117            .filter(|(_, val)| *val != self.sentinel)
118            .collect();
119
120        for (sv, sval) in &singletons {
121            for &other in &self.scope {
122                if other == *sv {
123                    continue;
124                }
125                if vars[other as usize].prune(sval, depth) {
126                    changed = true;
127                }
128                if vars[other as usize].domain.is_empty() {
129                    return Revision::Unsatisfiable;
130                }
131            }
132        }
133
134        if changed {
135            Revision::Changed
136        } else {
137            Revision::Unchanged
138        }
139    }
140}
141
142impl<D> Constraint<D> for AllDifferentExcept<D::Value>
143where
144    D: Domain,
145    D::Value: PartialEq + 'static + Send + Sync,
146{
147    fn scope(&self) -> &[VarId] {
148        &self.scope
149    }
150    fn check(&self, assignment: &[Option<D::Value>]) -> bool {
151        self.check_impl(assignment)
152    }
153    fn revise(&self, vars: &mut [Variable<D>], depth: usize) -> Revision {
154        self.revise_impl(vars, depth)
155    }
156}
csp_solver/constraint/all_different_except.rs

csp_solver/constraint/
all_different_except.rs
