propaga_core/
nogood.rs

1use crate::{ChangeReason, Explanation, VariableId};
2
3/// Branch literal: `variable` must equal `value` for this nogood to apply.
4#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
5pub struct NogoodLiteral {
6    /// Decision variable.
7    pub variable: VariableId,
8    /// Assigned value.
9    pub value: i32,
10}
11
12/// Learned nogood: the conjunction of literals cannot all hold simultaneously.
13#[derive(Clone, Debug, PartialEq, Eq)]
14pub struct Nogood {
15    literals: Vec<NogoodLiteral>,
16}
17
18impl Nogood {
19    /// Creates a nogood from branch literals.
20    #[must_use]
21    pub fn new(literals: Vec<NogoodLiteral>) -> Self {
22        Self { literals }
23    }
24
25    /// Returns the nogood literals.
26    #[must_use]
27    pub fn literals(&self) -> &[NogoodLiteral] {
28        &self.literals
29    }
30
31    /// Returns `true` when every literal matches `assignment`.
32    #[must_use]
33    pub fn is_satisfied_by(&self, assignment: &[(VariableId, i32)]) -> bool {
34        self.literals.iter().all(|literal| {
35            assignment
36                .iter()
37                .any(|&(var, value)| var == literal.variable && value == literal.value)
38        })
39    }
40
41    /// Returns `true` when extending `assignment` with `(var, value)` satisfies every literal.
42    #[must_use]
43    pub fn would_be_satisfied_by(
44        &self,
45        assignment: &[(VariableId, i32)],
46        var: VariableId,
47        value: i32,
48    ) -> bool {
49        self.literals.iter().all(|literal| {
50            if literal.variable == var {
51                literal.value == value
52            } else {
53                assignment
54                    .iter()
55                    .any(|&(v, val)| v == literal.variable && val == literal.value)
56            }
57        })
58    }
59}
60
61impl Explanation {
62    /// Returns branch literals in chronological order.
63    pub fn branch_literals(&self) -> impl Iterator<Item = NogoodLiteral> + '_ {
64        self.entries().iter().filter_map(|entry| match entry {
65            ChangeReason::Branch { variable, value } => Some(NogoodLiteral {
66                variable: *variable,
67                value: *value,
68            }),
69            ChangeReason::Propagator { .. } | ChangeReason::PropagatorConflict { .. } => None,
70        })
71    }
72
73    /// Returns literals from the most recent propagator-recorded conflict, if any.
74    #[must_use]
75    pub fn propagator_conflict_literals(&self) -> Option<Vec<NogoodLiteral>> {
76        self.entries().iter().rev().find_map(|entry| match entry {
77            ChangeReason::PropagatorConflict { literals } => Some(
78                literals
79                    .iter()
80                    .map(|&(variable, value)| NogoodLiteral { variable, value })
81                    .collect(),
82            ),
83            _ => None,
84        })
85    }
86
87    /// Returns unique branch literals, keeping the latest assignment per variable.
88    #[must_use]
89    pub fn unique_branch_literals(&self) -> Vec<NogoodLiteral> {
90        let mut literals = Vec::new();
91        for literal in self.branch_literals() {
92            if let Some(existing) = literals
93                .iter_mut()
94                .find(|l: &&mut NogoodLiteral| l.variable == literal.variable)
95            {
96                *existing = literal;
97            } else {
98                literals.push(literal);
99            }
100        }
101        literals
102    }
103}
104
105#[cfg(test)]
106mod tests {
107    use super::*;
108    use crate::{ChangeReason, Explanation, VariableId};
109    use slotmap::SlotMap;
110
111    fn make_var() -> VariableId {
112        let mut sm: SlotMap<crate::VariableKey, ()> = SlotMap::with_key();
113        VariableId::from_key(sm.insert(()))
114    }
115
116    #[test]
117    fn nogood_satisfied_by_matching_assignment() {
118        let v0 = make_var();
119        let v1 = make_var();
120        let nogood = Nogood::new(vec![
121            NogoodLiteral {
122                variable: v0,
123                value: 1,
124            },
125            NogoodLiteral {
126                variable: v1,
127                value: 2,
128            },
129        ]);
130        assert!(nogood.is_satisfied_by(&[(v0, 1), (v1, 2)]));
131        assert!(!nogood.is_satisfied_by(&[(v0, 1), (v1, 3)]));
132    }
133
134    #[test]
135    fn nogood_would_be_satisfied_by_extension() {
136        let v0 = make_var();
137        let nogood = Nogood::new(vec![NogoodLiteral {
138            variable: v0,
139            value: 5,
140        }]);
141        assert!(nogood.would_be_satisfied_by(&[], v0, 5));
142        assert!(!nogood.would_be_satisfied_by(&[], v0, 4));
143    }
144
145    #[test]
146    fn branch_literals_skip_propagator_entries() {
147        let v0 = make_var();
148        let mut explanation = Explanation::new();
149        explanation.record(ChangeReason::Branch {
150            variable: v0,
151            value: 3,
152        });
153        explanation.record(ChangeReason::Propagator {
154            propagator: crate::PropagatorId::from_key({
155                let mut sm: SlotMap<crate::PropagatorKey, ()> = SlotMap::with_key();
156                sm.insert(())
157            }),
158            variable: v0,
159            removed_value: Some(2),
160            bound: None,
161        });
162        let literals: Vec<_> = explanation.branch_literals().collect();
163        assert_eq!(literals.len(), 1);
164        assert_eq!(literals[0].value, 3);
165    }
166
167    #[test]
168    fn unique_branch_literals_keep_latest_per_variable() {
169        let v0 = make_var();
170        let mut explanation = Explanation::new();
171        explanation.record(ChangeReason::Branch {
172            variable: v0,
173            value: 1,
174        });
175        explanation.record(ChangeReason::Branch {
176            variable: v0,
177            value: 2,
178        });
179        let literals = explanation.unique_branch_literals();
180        assert_eq!(literals.len(), 1);
181        assert_eq!(literals[0].value, 2);
182    }
183
184    #[test]
185    fn propagator_conflict_literals_from_latest_conflict() {
186        let v0 = make_var();
187        let v1 = make_var();
188        let mut explanation = Explanation::new();
189        explanation.record(ChangeReason::PropagatorConflict {
190            literals: vec![(v0, 1), (v1, 2)],
191        });
192        let literals = explanation
193            .propagator_conflict_literals()
194            .expect("conflict literals");
195        assert_eq!(literals.len(), 2);
196    }
197}
propaga_core/nogood.rs

propaga_core/
nogood.rs
