1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
//! Unit propagation (BCP) and binary implication graph
use super::*;
#[cfg(feature = "profiling")]
use crate::profiling::{ProfilingCategory, ScopedTimer};
impl Solver {
/// Unit propagation using two-watched literals
///
/// Updates the current watch list in place so propagation does not rebuild
/// the list through repeated pushes into a freshly emptied buffer.
pub(super) fn propagate(&mut self) -> Option<ClauseId> {
#[cfg(feature = "profiling")]
let _timer = ScopedTimer::new(ProfilingCategory::SatPropagation);
while let Some(lit) = self.trail.next_to_propagate() {
self.stats.propagations += 1;
// First, propagate binary implications (faster)
let binary_len = self.binary_graph.get(lit).len();
for idx in 0..binary_len {
let (implied_lit, clause_id) = self.binary_graph.get(lit)[idx];
let value = self.trail.lit_value(implied_lit);
if value.is_false() {
// Conflict in binary clause
return Some(clause_id);
} else if !value.is_defined() {
// Propagate
self.trail.assign_propagation(implied_lit, clause_id);
// Lazy hyper-binary resolution: check if we can learn a binary clause
if self.config.enable_lazy_hyper_binary {
self.check_hyper_binary_resolution(lit, implied_lit, clause_id);
}
}
}
// Take the current watch list, mutate it in place, then move it
// back once propagation for this literal is finished.
let mut watches = core::mem::take(self.watches.get_mut(lit));
let mut conflict_found: Option<ClauseId> = None;
let mut watch_idx = 0;
while watch_idx < watches.len() {
let watcher = watches[watch_idx];
if self.trail.lit_value(watcher.blocker).is_true() {
watch_idx += 1;
continue;
}
let clause = match self.clauses.get_mut(watcher.clause) {
Some(c) if !c.deleted => c,
_ => {
// Deleted clause - remove its watcher in place.
watches.swap_remove(watch_idx);
continue;
}
};
// Make sure the false literal is at position 1
if clause.lits[0] == lit.negate() {
clause.swap(0, 1);
}
// If first watch is true, clause is satisfied
let first = clause.lits[0];
if self.trail.lit_value(first).is_true() {
watches[watch_idx] = Watcher::new(watcher.clause, first);
watch_idx += 1;
continue;
}
// Look for a new watch
let mut found = false;
for j in 2..clause.lits.len() {
let l = clause.lits[j];
if !self.trail.lit_value(l).is_false() {
clause.swap(1, j);
self.watches
.add(clause.lits[1].negate(), Watcher::new(watcher.clause, first));
watches.swap_remove(watch_idx);
found = true;
break;
}
}
if found {
continue;
}
// No new watch found - clause is unit or conflicting
watches[watch_idx] = Watcher::new(watcher.clause, first);
if self.trail.lit_value(first).is_false() {
conflict_found = Some(watcher.clause);
break;
} else {
// Unit propagation
self.trail.assign_propagation(first, watcher.clause);
// Lazy hyper-binary resolution
if self.config.enable_lazy_hyper_binary {
self.check_hyper_binary_resolution(lit, first, watcher.clause);
}
watch_idx += 1;
}
}
*self.watches.get_mut(lit) = watches;
if let Some(conflict) = conflict_found {
return Some(conflict);
}
}
None
}
/// Check for hyper-binary resolution opportunity
/// When propagating `implied` due to `lit` being assigned, check if we can
/// learn a binary clause by resolving the reason clauses
pub(super) fn check_hyper_binary_resolution(
&mut self,
_lit: Lit,
implied: Lit,
reason_id: ClauseId,
) {
// Only check at higher decision levels to avoid overhead
if self.trail.decision_level() < 2 {
return;
}
// Get the reason clause
let reason_clause = match self.clauses.get(reason_id) {
Some(c) if c.lits.len() >= 2 && c.lits.len() <= 4 => c.lits.clone(),
_ => return,
};
// Check if we can derive a binary clause
// Look for literals in the reason clause that are assigned at the current level
let current_level = self.trail.decision_level();
let mut current_level_lits = SmallVec::<[Lit; 4]>::new();
let mut has_non_zero_level_other = false;
for &reason_lit in &reason_clause {
if reason_lit != implied {
let var = reason_lit.var();
let level = self.trail.level(var);
if level == current_level {
current_level_lits.push(reason_lit);
} else if level > 0 {
// There's a literal at a non-zero level other than current
// This means the learned clause would depend on that assignment
// which is not safe for incremental solving
has_non_zero_level_other = true;
}
}
}
// If there's exactly one literal from the current level besides the implied one,
// and all others are at level 0, we can safely learn a binary clause.
// IMPORTANT: We must ensure ALL other literals are at level 0 for the learned
// clause to be valid when new constraints are added incrementally.
if current_level_lits.len() == 1 && !has_non_zero_level_other {
let other_lit = current_level_lits[0];
// Check if we can create a useful binary clause
// The reason clause had other_lit FALSE and implied it. So we learn:
// other_lit | implied (if other_lit is false, implied must be true)
let binary_clause_lits = [other_lit, implied];
// Check if this binary clause is new and useful
// The binary clause is: other_lit | implied
// This means: ~other_lit -> implied, and ~implied -> other_lit
if !self.has_binary_implication(other_lit.negate(), implied) {
// Learn this binary clause on-the-fly
let clause_id = self.clauses.add_learned(binary_clause_lits.iter().copied());
// Add correct implications: ~A -> B and ~B -> A for clause (A | B)
self.binary_graph
.add(other_lit.negate(), implied, clause_id);
self.binary_graph
.add(implied.negate(), other_lit, clause_id);
self.stats.learned_clauses += 1;
}
}
}
/// Check if a binary implication already exists
pub(super) fn has_binary_implication(&self, from_lit: Lit, to_lit: Lit) -> bool {
self.binary_graph
.get(from_lit)
.iter()
.any(|(lit, _)| *lit == to_lit)
}
}