oxiz_sat/
rephasing.rs

1//! Rephasing strategies for SAT solving
2//!
3//! Rephasing periodically resets or modifies phase saving information to help
4//! the solver escape local minima. This module implements various rephasing
5//! strategies used in modern SAT solvers like CaDiCaL and Kissat.
6//!
7//! References:
8//! - "CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling at SAT Race 2019"
9//! - "Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)"
10
11#[allow(unused_imports)]
12use crate::prelude::*;
13
14/// Rephasing strategy
15#[derive(Debug, Clone, Copy, PartialEq, Eq)]
16pub enum RephasingStrategy {
17    /// Use original polarity from formula (positive literals)
18    Original,
19    /// Invert all current phases
20    Inverted,
21    /// Assign random phases
22    Random,
23    /// Set all phases to false
24    False,
25    /// Set all phases to true
26    True,
27    /// Use phases from best assignment found so far
28    Best,
29    /// Use phases from local search or random walk
30    Walk,
31}
32
33/// Statistics for rephasing operations
34#[derive(Debug, Clone, Default)]
35pub struct RephasingStats {
36    /// Number of rephasing operations performed
37    pub rephase_count: usize,
38    /// Count of each strategy used
39    pub strategy_counts: [usize; 7],
40    /// Total conflicts at last rephase
41    pub last_rephase_conflicts: u64,
42}
43
44impl RephasingStats {
45    /// Display statistics
46    pub fn display(&self) {
47        println!("Rephasing Statistics:");
48        println!("  Total rephases: {}", self.rephase_count);
49        println!("  Strategy usage:");
50        println!("    Original:  {}", self.strategy_counts[0]);
51        println!("    Inverted:  {}", self.strategy_counts[1]);
52        println!("    Random:    {}", self.strategy_counts[2]);
53        println!("    False:     {}", self.strategy_counts[3]);
54        println!("    True:      {}", self.strategy_counts[4]);
55        println!("    Best:      {}", self.strategy_counts[5]);
56        println!("    Walk:      {}", self.strategy_counts[6]);
57    }
58}
59
60/// Rephasing manager
61///
62/// Manages periodic rephasing of variable polarities to help escape local minima
63/// and improve overall solver performance.
64#[derive(Debug)]
65pub struct RephasingManager {
66    /// Current rephasing interval (in conflicts)
67    interval: u64,
68    /// Initial interval
69    initial_interval: u64,
70    /// Interval multiplier for geometric increase
71    interval_multiplier: f64,
72    /// Maximum interval
73    max_interval: u64,
74    /// Best assignment found so far (for Best strategy)
75    best_assignment: Vec<bool>,
76    /// Statistics
77    stats: RephasingStats,
78    /// RNG state for random rephasing
79    rng_state: u64,
80}
81
82impl Default for RephasingManager {
83    fn default() -> Self {
84        Self::new()
85    }
86}
87
88impl RephasingManager {
89    /// Create a new rephasing manager with default settings
90    ///
91    /// Default settings:
92    /// - Initial interval: 1000 conflicts
93    /// - Multiplier: 1.1 (geometric increase)
94    /// - Max interval: 1_000_000 conflicts
95    #[must_use]
96    pub fn new() -> Self {
97        Self {
98            interval: 1000,
99            initial_interval: 1000,
100            interval_multiplier: 1.1,
101            max_interval: 1_000_000,
102            best_assignment: Vec::new(),
103            stats: RephasingStats::default(),
104            rng_state: 0x853c_49e6_748f_ea9b, // Random seed
105        }
106    }
107
108    /// Create with custom interval settings
109    #[must_use]
110    pub fn with_interval(initial: u64, multiplier: f64, max: u64) -> Self {
111        Self {
112            interval: initial,
113            initial_interval: initial,
114            interval_multiplier: multiplier,
115            max_interval: max,
116            best_assignment: Vec::new(),
117            stats: RephasingStats::default(),
118            rng_state: 0x853c_49e6_748f_ea9b,
119        }
120    }
121
122    /// Get statistics
123    #[must_use]
124    pub fn stats(&self) -> &RephasingStats {
125        &self.stats
126    }
127
128    /// Check if rephasing should occur at this conflict count
129    #[must_use]
130    pub fn should_rephase(&self, conflicts: u64) -> bool {
131        if self.stats.last_rephase_conflicts == 0 {
132            return conflicts >= self.interval;
133        }
134        conflicts - self.stats.last_rephase_conflicts >= self.interval
135    }
136
137    /// Update best assignment for Best strategy
138    pub fn update_best_assignment(&mut self, assignment: &[bool]) {
139        self.best_assignment = assignment.to_vec();
140    }
141
142    /// Perform rephasing with the given strategy
143    ///
144    /// Returns new phase values for all variables
145    pub fn rephase(
146        &mut self,
147        strategy: RephasingStrategy,
148        num_vars: usize,
149        current_phases: &[bool],
150        conflicts: u64,
151    ) -> Vec<bool> {
152        self.stats.rephase_count += 1;
153        self.stats.last_rephase_conflicts = conflicts;
154
155        // Update strategy count
156        let strategy_idx = match strategy {
157            RephasingStrategy::Original => 0,
158            RephasingStrategy::Inverted => 1,
159            RephasingStrategy::Random => 2,
160            RephasingStrategy::False => 3,
161            RephasingStrategy::True => 4,
162            RephasingStrategy::Best => 5,
163            RephasingStrategy::Walk => 6,
164        };
165        self.stats.strategy_counts[strategy_idx] += 1;
166
167        // Increase interval for next rephasing
168        self.interval =
169            ((self.interval as f64 * self.interval_multiplier) as u64).min(self.max_interval);
170
171        match strategy {
172            RephasingStrategy::Original => {
173                // Use positive polarity (false for all variables)
174                vec![false; num_vars]
175            }
176            RephasingStrategy::Inverted => {
177                // Invert all current phases
178                current_phases.iter().map(|&p| !p).collect()
179            }
180            RephasingStrategy::Random => {
181                // Random phases
182                (0..num_vars).map(|_| self.random_bool()).collect()
183            }
184            RephasingStrategy::False => {
185                // All false
186                vec![false; num_vars]
187            }
188            RephasingStrategy::True => {
189                // All true
190                vec![true; num_vars]
191            }
192            RephasingStrategy::Best => {
193                // Use best assignment if available, otherwise keep current
194                if self.best_assignment.len() >= num_vars {
195                    self.best_assignment[..num_vars].to_vec()
196                } else {
197                    current_phases.to_vec()
198                }
199            }
200            RephasingStrategy::Walk => {
201                // Random walk: mostly random with some bias toward current
202                (0..num_vars)
203                    .map(|i| {
204                        if self.random_bool() {
205                            // 50% keep current
206                            current_phases.get(i).copied().unwrap_or(false)
207                        } else {
208                            // 50% random
209                            self.random_bool()
210                        }
211                    })
212                    .collect()
213            }
214        }
215    }
216
217    /// Get the next recommended rephasing strategy
218    ///
219    /// Uses a cyclic pattern: Original -> Inverted -> Random -> False -> Best
220    #[must_use]
221    pub fn next_strategy(&self) -> RephasingStrategy {
222        let cycle = self.stats.rephase_count % 5;
223        match cycle {
224            0 => RephasingStrategy::Original,
225            1 => RephasingStrategy::Inverted,
226            2 => RephasingStrategy::Random,
227            3 => RephasingStrategy::False,
228            _ => RephasingStrategy::Best,
229        }
230    }
231
232    /// Reset to initial interval
233    pub fn reset(&mut self) {
234        self.interval = self.initial_interval;
235        self.stats = RephasingStats::default();
236    }
237
238    /// Simple xorshift64 random number generator
239    fn random_u64(&mut self) -> u64 {
240        self.rng_state ^= self.rng_state << 13;
241        self.rng_state ^= self.rng_state >> 7;
242        self.rng_state ^= self.rng_state << 17;
243        self.rng_state
244    }
245
246    /// Generate random boolean
247    fn random_bool(&mut self) -> bool {
248        (self.random_u64() & 1) == 1
249    }
250}
251
252#[cfg(test)]
253mod tests {
254    use super::*;
255
256    #[test]
257    fn test_rephasing_manager_creation() {
258        let manager = RephasingManager::new();
259        assert_eq!(manager.stats.rephase_count, 0);
260        assert_eq!(manager.interval, 1000);
261    }
262
263    #[test]
264    fn test_should_rephase() {
265        let manager = RephasingManager::new();
266        assert!(!manager.should_rephase(500));
267        assert!(manager.should_rephase(1000));
268        assert!(manager.should_rephase(1500));
269    }
270
271    #[test]
272    fn test_rephase_original() {
273        let mut manager = RephasingManager::new();
274        let current = vec![true, false, true, false];
275        let result = manager.rephase(RephasingStrategy::Original, 4, &current, 1000);
276
277        assert_eq!(result, vec![false, false, false, false]);
278        assert_eq!(manager.stats.rephase_count, 1);
279    }
280
281    #[test]
282    fn test_rephase_inverted() {
283        let mut manager = RephasingManager::new();
284        let current = vec![true, false, true, false];
285        let result = manager.rephase(RephasingStrategy::Inverted, 4, &current, 1000);
286
287        assert_eq!(result, vec![false, true, false, true]);
288    }
289
290    #[test]
291    fn test_rephase_false() {
292        let mut manager = RephasingManager::new();
293        let current = vec![true, false, true, false];
294        let result = manager.rephase(RephasingStrategy::False, 4, &current, 1000);
295
296        assert_eq!(result, vec![false, false, false, false]);
297    }
298
299    #[test]
300    fn test_rephase_true() {
301        let mut manager = RephasingManager::new();
302        let current = vec![true, false, true, false];
303        let result = manager.rephase(RephasingStrategy::True, 4, &current, 1000);
304
305        assert_eq!(result, vec![true, true, true, true]);
306    }
307
308    #[test]
309    fn test_rephase_best() {
310        let mut manager = RephasingManager::new();
311        manager.update_best_assignment(&[true, true, false, false]);
312
313        let current = vec![false, false, false, false];
314        let result = manager.rephase(RephasingStrategy::Best, 4, &current, 1000);
315
316        assert_eq!(result, vec![true, true, false, false]);
317    }
318
319    #[test]
320    fn test_next_strategy() {
321        let mut manager = RephasingManager::new();
322
323        assert_eq!(manager.next_strategy(), RephasingStrategy::Original);
324        manager.rephase(RephasingStrategy::Original, 1, &[false], 1000);
325
326        assert_eq!(manager.next_strategy(), RephasingStrategy::Inverted);
327        manager.rephase(RephasingStrategy::Inverted, 1, &[false], 2000);
328
329        assert_eq!(manager.next_strategy(), RephasingStrategy::Random);
330    }
331
332    #[test]
333    fn test_interval_increase() {
334        let mut manager = RephasingManager::with_interval(100, 2.0, 10000);
335
336        manager.rephase(RephasingStrategy::Original, 1, &[false], 100);
337        assert_eq!(manager.interval, 200);
338
339        manager.rephase(RephasingStrategy::Original, 1, &[false], 300);
340        assert_eq!(manager.interval, 400);
341    }
342
343    #[test]
344    fn test_stats_display() {
345        let mut manager = RephasingManager::new();
346        manager.rephase(RephasingStrategy::Original, 1, &[false], 1000);
347        manager.rephase(RephasingStrategy::Inverted, 1, &[false], 2000);
348
349        let stats = manager.stats();
350        assert_eq!(stats.rephase_count, 2);
351        assert_eq!(stats.strategy_counts[0], 1); // Original
352        assert_eq!(stats.strategy_counts[1], 1); // Inverted
353    }
354}
oxiz_sat/rephasing.rs

oxiz_sat/
rephasing.rs
