oxiz_sat/
dynamic_lbd.rs

1//! Dynamic LBD (Literal Block Distance) Updates
2//!
3//! This module implements dynamic LBD updates for learned clauses during search.
4//! LBD is a key metric for clause quality - clauses with lower LBD are more likely
5//! to be useful for future conflicts.
6//!
7//! The dynamic LBD update strategy:
8//! - Periodically recompute LBD of learned clauses
9//! - If LBD decreases, the clause is becoming more "glue-like" and should be kept
10//! - Update clause tier based on improved LBD
11//!
12//! Reference: "Glucose" SAT solver by Gilles Audemard and Laurent Simon
13
14use crate::clause::{ClauseDatabase, ClauseId, ClauseTier};
15use crate::literal::Lit;
16#[allow(unused_imports)]
17use crate::prelude::*;
18
19/// Statistics for dynamic LBD updates
20#[derive(Debug, Default, Clone)]
21pub struct DynamicLbdStats {
22    /// Number of LBD updates performed
23    pub updates_performed: u64,
24    /// Number of clauses with improved LBD
25    pub lbd_improved: u64,
26    /// Number of clauses promoted to higher tier due to LBD improvement
27    pub tier_promotions: u64,
28}
29
30/// Dynamic LBD manager
31pub struct DynamicLbdManager {
32    /// Interval between LBD updates (in conflicts)
33    update_interval: u64,
34    /// Conflict counter
35    conflicts: u64,
36    /// Statistics
37    stats: DynamicLbdStats,
38    /// Temporary set for LBD computation
39    seen_levels: HashSet<u32>,
40}
41
42impl DynamicLbdManager {
43    /// Create a new dynamic LBD manager
44    pub fn new(update_interval: u64) -> Self {
45        Self {
46            update_interval,
47            conflicts: 0,
48            stats: DynamicLbdStats::default(),
49            seen_levels: HashSet::new(),
50        }
51    }
52
53    /// Get statistics
54    #[must_use]
55    pub fn stats(&self) -> &DynamicLbdStats {
56        &self.stats
57    }
58
59    /// Increment conflict counter
60    pub fn on_conflict(&mut self) {
61        self.conflicts += 1;
62    }
63
64    /// Check if it's time to update LBDs
65    #[must_use]
66    pub fn should_update(&self) -> bool {
67        self.conflicts.is_multiple_of(self.update_interval)
68    }
69
70    /// Compute LBD for a clause given variable decision levels
71    ///
72    /// LBD (Literal Block Distance) is the number of distinct decision levels
73    /// in the clause. Lower LBD means the clause is more "glue-like" and
74    /// connects more decision levels.
75    fn compute_lbd(&mut self, lits: &[Lit], level: &[u32]) -> u32 {
76        self.seen_levels.clear();
77
78        for &lit in lits {
79            let var_level = level[lit.var().index()];
80            if var_level > 0 {
81                self.seen_levels.insert(var_level);
82            }
83        }
84
85        self.seen_levels.len() as u32
86    }
87
88    /// Update LBD for a single clause
89    ///
90    /// Returns true if the LBD was improved
91    pub fn update_clause_lbd(
92        &mut self,
93        clause_id: ClauseId,
94        clauses: &mut ClauseDatabase,
95        level: &[u32],
96    ) -> bool {
97        let Some(clause) = clauses.get(clause_id) else {
98            return false;
99        };
100
101        // Only update learned clauses
102        if !clause.learned || clause.deleted {
103            return false;
104        }
105
106        let old_lbd = clause.lbd;
107        let lits: Vec<Lit> = clause.lits.iter().copied().collect();
108
109        // Compute new LBD
110        let new_lbd = self.compute_lbd(&lits, level);
111
112        // Update if improved
113        if new_lbd < old_lbd
114            && let Some(clause) = clauses.get_mut(clause_id)
115        {
116            clause.lbd = new_lbd;
117
118            // Promote to Core tier if LBD is very low (glue clause)
119            if new_lbd <= 2 && clause.tier != ClauseTier::Core {
120                clause.promote_to_core();
121                self.stats.tier_promotions += 1;
122            }
123            // Promote from Local to Mid if LBD improved significantly
124            else if new_lbd < old_lbd && clause.tier == ClauseTier::Local {
125                clause.tier = ClauseTier::Mid;
126                self.stats.tier_promotions += 1;
127            }
128
129            self.stats.lbd_improved += 1;
130            return true;
131        }
132
133        false
134    }
135
136    /// Update LBDs for all learned clauses
137    ///
138    /// Returns the number of clauses with improved LBD
139    pub fn update_all_lbds(&mut self, clauses: &mut ClauseDatabase, level: &[u32]) -> u64 {
140        let mut improved = 0;
141
142        // Collect clause IDs first to avoid borrow checker issues
143        let clause_ids: Vec<ClauseId> = clauses
144            .iter_ids()
145            .filter(|&id| {
146                if let Some(clause) = clauses.get(id) {
147                    clause.learned && !clause.deleted
148                } else {
149                    false
150                }
151            })
152            .collect();
153
154        for clause_id in clause_ids {
155            if self.update_clause_lbd(clause_id, clauses, level) {
156                improved += 1;
157            }
158        }
159
160        self.stats.updates_performed += 1;
161        improved
162    }
163
164    /// Update LBDs if it's time to do so
165    ///
166    /// Returns the number of clauses with improved LBD, or 0 if not time to update
167    pub fn maybe_update(&mut self, clauses: &mut ClauseDatabase, level: &[u32]) -> u64 {
168        if self.should_update() {
169            self.update_all_lbds(clauses, level)
170        } else {
171            0
172        }
173    }
174
175    /// Reset conflict counter
176    pub fn reset_conflicts(&mut self) {
177        self.conflicts = 0;
178    }
179}
180
181#[cfg(test)]
182mod tests {
183    use super::*;
184    use crate::literal::Var;
185
186    #[test]
187    fn test_dynamic_lbd_creation() {
188        let manager = DynamicLbdManager::new(1000);
189        assert_eq!(manager.update_interval, 1000);
190        assert_eq!(manager.conflicts, 0);
191    }
192
193    #[test]
194    fn test_conflict_counter() {
195        let mut manager = DynamicLbdManager::new(100);
196        manager.on_conflict();
197        manager.on_conflict();
198        assert_eq!(manager.conflicts, 2);
199    }
200
201    #[test]
202    fn test_should_update() {
203        let mut manager = DynamicLbdManager::new(10);
204        assert!(manager.should_update()); // 0 % 10 == 0
205
206        for _ in 0..9 {
207            manager.on_conflict();
208            assert!(!manager.should_update());
209        }
210
211        manager.on_conflict();
212        assert!(manager.should_update()); // 10 % 10 == 0
213    }
214
215    #[test]
216    fn test_compute_lbd() {
217        let mut manager = DynamicLbdManager::new(100);
218        let lits = vec![
219            Lit::pos(Var::new(0)),
220            Lit::neg(Var::new(1)),
221            Lit::pos(Var::new(2)),
222        ];
223        let level = vec![0, 1, 2]; // var 0 at level 0, var 1 at level 1, var 2 at level 2
224
225        let lbd = manager.compute_lbd(&lits, &level);
226        // Should count levels 1 and 2 (level 0 is not counted)
227        assert_eq!(lbd, 2);
228    }
229
230    #[test]
231    fn test_stats() {
232        let manager = DynamicLbdManager::new(100);
233        let stats = manager.stats();
234        assert_eq!(stats.updates_performed, 0);
235        assert_eq!(stats.lbd_improved, 0);
236        assert_eq!(stats.tier_promotions, 0);
237    }
238
239    #[test]
240    fn test_reset_conflicts() {
241        let mut manager = DynamicLbdManager::new(100);
242        manager.on_conflict();
243        manager.on_conflict();
244        assert_eq!(manager.conflicts, 2);
245
246        manager.reset_conflicts();
247        assert_eq!(manager.conflicts, 0);
248    }
249}
oxiz_sat/dynamic_lbd.rs

oxiz_sat/
dynamic_lbd.rs
