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. Snapshot into
107 // the pooled thread-local buffer (Beat 2), preserving the exact prior
108 // semantics — non-sentinel singletons only, collected before pruning.
109 let mut changed = false;
110 let sentinel = &self.sentinel;
111 let unsat = super::scratch::with_singleton_buf::<D::Value, _>(|singletons| {
112 for &v in &self.scope {
113 if let Some(val) = vars[v as usize].domain.singleton_value()
114 && val != *sentinel
115 {
116 singletons.push((v, val));
117 }
118 }
119 for (sv, sval) in singletons.iter() {
120 for &other in &self.scope {
121 if other == *sv {
122 continue;
123 }
124 if vars[other as usize].prune(sval, depth) {
125 changed = true;
126 }
127 if vars[other as usize].domain.is_empty() {
128 return true;
129 }
130 }
131 }
132 false
133 });
134 if unsat {
135 return Revision::Unsatisfiable;
136 }
137
138 if changed {
139 Revision::Changed
140 } else {
141 Revision::Unchanged
142 }
143 }
144}
145
146impl<D> Constraint<D> for AllDifferentExcept<D::Value>
147where
148 D: Domain,
149 D::Value: PartialEq + 'static + Send + Sync,
150{
151 fn scope(&self) -> &[VarId] {
152 &self.scope
153 }
154 fn check(&self, assignment: &[Option<D::Value>]) -> bool {
155 self.check_impl(assignment)
156 }
157 fn revise(&self, vars: &mut [Variable<D>], depth: usize) -> Revision {
158 self.revise_impl(vars, depth)
159 }
160}