csp_solver/constraint/
all_different.rs

1//! N-ary all-different constraint.
2//!
3//! Tests: `tests/solver.rs` (live path via `Csp::add_all_different`);
4//! `tests/sudoku.rs`, `tests/futoshiki.rs` exercise the GAC core end-to-end.
5
6use crate::domain::Domain;
7use crate::variable::Variable;
8
9use super::traits::{Constraint, Revision, VarId};
10
11#[derive(Debug)]
12pub struct AllDifferent {
13    pub(crate) scope: Vec<VarId>,
14    /// Stable per-constraint id keying the GAC matching warm-start cache.
15    gac_id: u32,
16}
17
18impl AllDifferent {
19    pub fn new(vars: Vec<VarId>) -> Self {
20        Self {
21            scope: vars,
22            gac_id: crate::solver::gac::next_gac_id(),
23        }
24    }
25
26    pub(crate) fn check_impl<V: PartialEq>(&self, assignment: &[Option<V>]) -> bool {
27        let assigned: Vec<&V> = self
28            .scope
29            .iter()
30            .filter_map(|&v| assignment[v as usize].as_ref())
31            .collect();
32        for i in 0..assigned.len() {
33            for j in (i + 1)..assigned.len() {
34                if assigned[i] == assigned[j] {
35                    return false;
36                }
37            }
38        }
39        true
40    }
41
42    /// Singleton removal followed by GAC when enough participants remain live.
43    ///
44    /// Singleton removal always runs (it is the only step that detects two
45    /// *assigned* variables sharing a value — GAC skips assigned vars). Above a
46    /// dynamic live-unassigned-count gate, Régin GAC then adds the Hall-set
47    /// pruning arc consistency misses; below it, GAC would find nothing more, so
48    /// it is skipped. The gate is on the *live* count, not the constraint's
49    /// original arity, so deep search nodes with few free variables pay nothing.
50    pub(crate) fn revise_impl<D: Domain>(&self, vars: &mut [Variable<D>], depth: usize) -> Revision
51    where
52        D::Value: PartialEq + 'static,
53    {
54        let mut changed = false;
55        // Snapshot-then-prune over a pooled thread-local buffer (Beat 2). The
56        // borrow is released before the GAC core call below — that path borrows
57        // its own thread-local scratch, and holding this one across it would
58        // risk a `RefCell` double-borrow. Semantics are byte-identical to the
59        // prior per-call `Vec`: collect every singleton first, then prune peers.
60        let unsat = super::scratch::with_singleton_buf::<D::Value, _>(|singletons| {
61            for &v in &self.scope {
62                if let Some(val) = vars[v as usize].domain.singleton_value() {
63                    singletons.push((v, val));
64                }
65            }
66            for (sv, sval) in singletons.iter() {
67                for &other in &self.scope {
68                    if other == *sv {
69                        continue;
70                    }
71                    if vars[other as usize].prune(sval, depth) {
72                        changed = true;
73                    }
74                    if vars[other as usize].domain.is_empty() {
75                        return true;
76                    }
77                }
78            }
79            false
80        });
81        if unsat {
82            return Revision::Unsatisfiable;
83        }
84
85        // Dynamic gate: count live (non-singleton, non-empty) variables.
86        let live = self
87            .scope
88            .iter()
89            .filter(|&&v| {
90                let d = &vars[v as usize].domain;
91                !d.is_singleton() && !d.is_empty()
92            })
93            .count();
94
95        if live >= crate::solver::gac::GAC_MIN_PARTICIPANTS
96            && crate::solver::gac::GAC_IN_ALLDIFF_ENABLED.load(std::sync::atomic::Ordering::Relaxed)
97        {
98            match crate::solver::gac::propagate_gac_core(
99                &self.scope,
100                None,
101                vars,
102                depth,
103                Some(self.gac_id),
104            ) {
105                Revision::Unsatisfiable => return Revision::Unsatisfiable,
106                Revision::Changed => changed = true,
107                Revision::Unchanged => {}
108            }
109        }
110
111        if changed {
112            Revision::Changed
113        } else {
114            Revision::Unchanged
115        }
116    }
117}
118
119impl<D: Domain> Constraint<D> for AllDifferent
120where
121    D::Value: PartialEq + 'static,
122{
123    fn scope(&self) -> &[VarId] {
124        &self.scope
125    }
126    fn check(&self, assignment: &[Option<D::Value>]) -> bool {
127        self.check_impl(assignment)
128    }
129    fn revise(&self, vars: &mut [Variable<D>], depth: usize) -> Revision {
130        self.revise_impl(vars, depth)
131    }
132}
csp_solver/constraint/all_different.rs

csp_solver/constraint/
all_different.rs
