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
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
//! Clause Distillation
//!
//! Distillation is a clause strengthening technique that tries to remove
//! literals from clauses through a limited form of search. It's more
//! aggressive than vivification but still efficient.
//!
//! The basic idea:
//! - For each literal L in a clause C
//! - Temporarily assign ~L (trying to falsify L)
//! - Perform limited unit propagation
//! - If we can derive C\{L} (clause without L), then L is redundant
//! - Remove L from C
use crate::clause::{ClauseDatabase, ClauseId};
use crate::literal::{LBool, Lit};
#[allow(unused_imports)]
use crate::prelude::*;
use crate::trail::Trail;
use crate::watched::WatchLists;
/// Statistics for distillation
#[derive(Debug, Default, Clone)]
pub struct DistillationStats {
/// Number of clauses distilled
pub clauses_distilled: u64,
/// Number of literals removed
pub literals_removed: u64,
/// Number of clauses deleted (became unit/empty)
pub clauses_deleted: u64,
}
/// Clause distillation manager
pub struct Distillation {
/// Maximum propagation depth
#[allow(dead_code)]
max_depth: u32,
/// Statistics
stats: DistillationStats,
}
impl Distillation {
/// Create a new distillation manager
pub fn new(max_depth: u32) -> Self {
Self {
max_depth,
stats: DistillationStats::default(),
}
}
/// Get statistics
#[must_use]
pub fn stats(&self) -> &DistillationStats {
&self.stats
}
/// Try to distill a single clause
///
/// Returns true if the clause was strengthened or deleted
#[allow(clippy::too_many_arguments)]
pub fn distill_clause(
&mut self,
clause_id: ClauseId,
clauses: &mut ClauseDatabase,
trail: &mut Trail,
watches: &mut WatchLists,
assignment: &[LBool],
) -> bool {
let Some(clause) = clauses.get(clause_id) else {
return false;
};
if clause.deleted || clause.len() <= 2 {
// Don't distill binary or smaller clauses
return false;
}
let original_lits: Vec<Lit> = clause.lits.iter().copied().collect();
let mut strengthened = false;
// Try to remove each literal
for &lit in &original_lits {
// Skip if already assigned
if assignment[lit.var().index()] != LBool::Undef {
continue;
}
// Try assigning ~lit and see if we can derive the clause without lit
if self.try_remove_literal(lit, clause_id, clauses, trail, watches, assignment) {
strengthened = true;
self.stats.literals_removed += 1;
}
}
if strengthened {
self.stats.clauses_distilled += 1;
// Check if clause became unit or empty
if let Some(clause) = clauses.get(clause_id)
&& clause.len() <= 1
{
self.stats.clauses_deleted += 1;
return true;
}
}
strengthened
}
/// Try to remove a literal from a clause through limited propagation
#[allow(clippy::too_many_arguments)]
fn try_remove_literal(
&self,
lit: Lit,
clause_id: ClauseId,
clauses: &mut ClauseDatabase,
trail: &mut Trail,
_watches: &mut WatchLists,
assignment: &[LBool],
) -> bool {
// Save current trail level
let saved_level = trail.decision_level();
// Make a new decision level for this test
trail.new_decision_level();
// Assign ~lit
let _test_lit = lit.negate();
// Check if this causes immediate conflict with other literals in the clause
let Some(clause) = clauses.get(clause_id) else {
trail.backtrack_to(saved_level);
return false;
};
for &other_lit in &clause.lits {
if other_lit == lit {
continue;
}
// If other literal is already false under ~lit, we can't remove lit
if assignment[other_lit.var().index()] == LBool::from(!other_lit.sign()) {
trail.backtrack_to(saved_level);
return false;
}
// Simple check: if assigning ~lit would make another literal in the
// clause become true, then lit is potentially redundant
if assignment[other_lit.var().index()] == LBool::from(other_lit.sign()) {
// Other literal is already true, so lit is redundant
if let Some(clause) = clauses.get_mut(clause_id) {
clause.lits.retain(|l| *l != lit);
}
trail.backtrack_to(saved_level);
return true;
}
}
// For now, just do a simple check
// A full implementation would do limited BCP here
trail.backtrack_to(saved_level);
// Conservative: don't remove unless we're certain
false
}
/// Distill all learned clauses in the database
pub fn distill_all(
&mut self,
clauses: &mut ClauseDatabase,
trail: &mut Trail,
watches: &mut WatchLists,
assignment: &[LBool],
) -> u64 {
let mut total_strengthened = 0;
// Only distill learned clauses
let clause_ids: Vec<ClauseId> = clauses
.iter_ids()
.filter(|&id| {
if let Some(clause) = clauses.get(id) {
clause.learned && !clause.deleted
} else {
false
}
})
.collect();
for clause_id in clause_ids {
if self.distill_clause(clause_id, clauses, trail, watches, assignment) {
total_strengthened += 1;
}
}
total_strengthened
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::literal::Var;
#[test]
fn test_distillation_stats() {
let distill = Distillation::new(10);
let stats = distill.stats();
assert_eq!(stats.clauses_distilled, 0);
assert_eq!(stats.literals_removed, 0);
}
#[test]
fn test_distillation_creation() {
let distill = Distillation::new(5);
assert_eq!(distill.max_depth, 5);
}
#[test]
fn test_distillation_binary_clause() {
let mut distill = Distillation::new(10);
let mut db = ClauseDatabase::new();
let mut trail = Trail::new(10);
let mut watches = WatchLists::new(10);
let assignment = vec![LBool::Undef; 10];
// Add a binary clause - should not be distilled
let clause_id = db.add_learned([Lit::pos(Var::new(0)), Lit::neg(Var::new(1))]);
let result =
distill.distill_clause(clause_id, &mut db, &mut trail, &mut watches, &assignment);
assert!(!result); // Binary clauses are not distilled
}
}