SLS

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.17.0-alpha.2"
+version = "0.17.0-alpha.3"
 authors = ["Narazaki Shuji <shujinarazaki@protonmail.com>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -17,49 +17,64 @@ bitflags = "^1.3"
 
 [features]
 default = [
-        # "boundary_check", # for DEBUG
-        # "bi_clause_completion", # increase memory pressure
-        # "no_clause_elimination",
-        # "clause_rewarding",
-        "clause_vivification",
-        "dynamic_restart_threshold",
+        ### Essential
         # "incremental_solver",
         "LRB_rewarding",
-        # "maintain_watch_cache", # for DEBUG
         "reason_side_rewarding",
+        "unsafe_access",
+        "trail_saving",
+
+        ### heuristics
+        # "bi_clause_completion",
+        # "clause_rewarding",
+        "dynamic_restart_threshold",
         "rephase",
-        # "reward_annealing", # for big problems since 0.17(need to evalate with larger timeout)
+        # "reward_annealing",
+        "stochastic_local_search",
         # "suppress_reason_chain",
-        "trail_saving",
-        "unsafe_access"
+
+        ### proceccor
+        # "no_clause_elimination",
+        "clause_vivification",
+
+        ### for DEBUG
+        # "boundary_check",
+        # "maintain_watch_cache",
+        ]
+assign_rate = []                # for debug and study
+best_phases_tracking = []       # save the best-so-far assignment, used by 'rephase'
+bi_clause_completion = []       # increase memory pressure
+boundary_check = []             # for debug
+chrono_BT = []                  # NOT WORK
+no_clause_elimination = []      # pre(in)-processor setting
+clause_rewarding = []           # clauses have activities w/ decay rate
+clause_vivification = []        # pre(in)-processor setting
+debug_propagation = []          # for debug
+dynamic_restart_threshold = []  # control restart spans like Glucose
+EMA_calibration = []            # each exponential moving average has a calbration value
+EVSIDS = []                     # Eponential Variable State Independent Decaying Sum
+incremental_solver = [          # for all solution SAT sover
+        "no_clause_elimination"
+        ]
+just_used = []                  # Var and clause have 'just_used' flags
+LRB_rewarding = []              # Vearning Rate Based rewarding, a new var activity criteria
+maintain_watch_cache = []       # for DEBUG
+no_IO = []                      # to embed Splr into non-std environments
+reason_side_rewarding = []      # an idea used in Learning-rate based rewarding
+rephase = [                     # search around the best-so-far candidate repeatedly
+        "best_phases_tracking"
+        ]
+reward_annealing = []           # use bigger and smaller decay rates cycliclly
+stochastic_local_search = [     # since 0.17
+        "reward_annealing"
         ]
-assign_rate = []
-best_phases_tracking = []
-bi_clause_completion = []
-boundary_check = []
-chrono_BT = []
-no_clause_elimination = []
-clause_rewarding = []
-clause_vivification = []
-debug_propagation = []
-dynamic_restart_threshold = []
-EMA_calibration = []
-EVSIDS = []
-incremental_solver = ["no_clause_elimination"]
-just_used = []
-LRB_rewarding = []
-maintain_watch_cache = []
-no_IO = []
-reason_side_rewarding = []
-rephase = ["best_phases_tracking"]
-reward_annealing = []
-support_user_assumption = []
-suppress_reason_chain = []
-trace_analysis = []
-trace_elimination = []
-trace_equivalency = []
-trail_saving = []
-unsafe_access = []
+support_user_assumption = []    # NOT WORK (defined in Glucose)
+suppress_reason_chain = []      # make direct links between a dicision var and its implications
+trace_analysis = []             # for debug
+trace_elimination = []          # for debug
+trace_equivalency = []          # for debug
+trail_saving = []               # reduce propagation cost by reusing propagation chain
+unsafe_access = []              # access elements of vectors without boundary checking
 
 [profile.release]
 lto = "fat"

src/assign/mod.rs

@@ -76,6 +76,8 @@ pub trait AssignIF:
     /// return a reference to `level`.
     fn level_ref(&self) -> &[DecisionLevel];
     fn best_assigned(&mut self) -> Option<usize>;
+    /// return true if no best_phases
+    fn best_phases_invalid(&self) -> bool;
     /// inject assignments for eliminated vars.
     fn extend_model(&mut self, c: &mut impl ClauseDBIF) -> Vec<Option<bool>>;
     /// return `true` if the set of literals is satisfiable under the current assignment.

src/assign/select.rs

@@ -6,6 +6,7 @@ use super::property;
 use {
     super::{AssignStack, VarHeapIF},
     crate::types::*,
+    std::collections::HashMap,
 };
 
 /// ```ignore
@@ -26,6 +27,10 @@ macro_rules! var_assign {
 
 /// API for var selection, depending on an internal heap.
 pub trait VarSelectIF {
+    /// return best phases
+    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool>;
+    /// force an assignment obtained by SLS
+    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize;
     #[cfg(feature = "rephase")]
     /// select rephasing target
     fn select_rephasing_target(&mut self);
@@ -41,6 +46,44 @@ pub trait VarSelectIF {
 }
 
 impl VarSelectIF for AssignStack {
+    fn best_phases_ref(&mut self, default_value: Option<bool>) -> HashMap<VarId, bool> {
+        self.var
+            .iter()
+            .enumerate()
+            .filter_map(|(vi, v)| {
+                if self.level[vi] == self.root_level || self.var[vi].is(FlagVar::ELIMINATED) {
+                    default_value.map(|b| (vi, b))
+                } else {
+                    Some((
+                        vi,
+                        self.best_phases.get(&vi).map_or(
+                            self.assign[vi].unwrap_or_else(|| v.is(FlagVar::PHASE)),
+                            |(b, _)| *b,
+                        ),
+                    ))
+                }
+            })
+            .collect::<HashMap<VarId, bool>>()
+    }
+    fn override_rephasing_target(&mut self, assignment: &HashMap<VarId, bool>) -> usize {
+        let mut num_flipped = 0;
+        for (vi, b) in assignment.iter() {
+            // let v = &mut self.var[*vi];
+            // if v.is(FlagVar::PHASE) != *b {
+            //     num_flipped += 1;
+            //     v.set(FlagVar::PHASE, *b);
+            //     // v.reward *= self.activity_decay;
+            //     // v.reward += self.activity_anti_decay;
+            //     // self.update_heap(*vi);
+            // }
+            if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) {
+                num_flipped += 1;
+                self.best_phases.insert(*vi, (*b, AssignReason::None));
+            }
+        }
+        // self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars;
+        num_flipped
+    }
     #[cfg(feature = "rephase")]
     fn select_rephasing_target(&mut self) {
         if self.best_phases.is_empty() {

src/assign/stack.rs

@@ -196,6 +196,9 @@ impl AssignIF for AssignStack {
     fn best_assigned(&mut self) -> Option<usize> {
         (self.build_best_at == self.num_propagation).then_some(self.num_vars - self.num_best_assign)
     }
+    fn best_phases_invalid(&self) -> bool {
+        self.best_phases.is_empty()
+    }
     #[allow(unused_variables)]
     fn extend_model(&mut self, cdb: &mut impl ClauseDBIF) -> Vec<Option<bool>> {
         let lits = &self.eliminated;

src/cdb/activity.rs

@@ -20,6 +20,10 @@ impl ActivityIF<ClauseId> for ClauseDB {
     fn update_activity_tick(&mut self) {
         self.tick += 1;
     }
+    fn update_activity_decay(&mut self, decay: f64) {
+        self.activity_decay = decay;
+        self.activity_anti_decay = 1.0 - decay;
+    }
 }
 
 impl Clause {

src/cdb/db.rs

@@ -48,6 +48,7 @@ impl Default for ClauseDB {
             num_reduction: 0,
             num_reregistration: 0,
             lb_entanglement: Ema2::new(1_000).with_slow(80_000).with_value(2.0),
+            last_reduction_threshold: 0,
             eliminated_permanent: Vec::new(),
         }
     }
@@ -1022,16 +1023,21 @@ impl ClauseDBIF for ClauseDB {
         }
         perm.sort();
         // Worse half of `perm` should be discarded now. But many people thought
-        // there're exception. Since this is the pre-stage of clause vivification,
+        // there're exceptions. Since this is the pre-stage of clause vivification,
         // we want keep usefull clauses as many as possible.
         // Therefore I save the clauses which will become vivification targets.
-        let thr = (self.lb_entanglement.get_slow() + 1.0).min(self.lbd.get_fast().max(5.0)) as u16;
+        // And since the current Splr adopts stage-based GC policy, I drop this simple halve'em if doubled,
+        // based on memomy pressure and clause sizes used in conflict analysis.
+        let entanglement = 1.75 * (self.lb_entanglement.get_slow() + self.lbd.get_slow()).powf(0.5);
+        let memory_pressure = 2000.0 * (self.num_learnt as f64).powf(-0.5);
+        let thr = (entanglement + memory_pressure).min(entanglement) as u16;
         for i in &perm[keep..] {
             let c = &self.clause[i.to()];
             if !c.is_vivify_target() || thr < c.rank {
                 self.remove_clause(ClauseId::from(i.to()));
             }
         }
+        self.last_reduction_threshold = thr as usize;
     }
     fn reset(&mut self) {
         debug_assert!(1 < self.clause.len());

src/cdb/mod.rs

@@ -10,6 +10,8 @@ mod clause;
 mod db;
 /// EMA
 mod ema;
+/// methods for Stochastic Local Search
+mod sls;
 /// methods for UNSAT certification
 mod unsat_certificate;
 /// implementation of clause vivification
@@ -21,9 +23,11 @@ pub use self::{
     binary::{BinaryLinkDB, BinaryLinkList},
     cid::ClauseIdIF,
     property::*,
+    sls::StochasticLocalSearchIF,
     unsat_certificate::CertificationStore,
     vivify::VivifyIF,
 };
+
 use {
     self::ema::ProgressLBD,
     crate::{assign::AssignIF, types::*},
@@ -285,7 +289,9 @@ pub struct ClauseDB {
     num_reregistration: usize,
     /// Literal Block Entanglement
     /// EMA of LBD of clauses used in conflict analysis (dependency graph)
-    pub lb_entanglement: Ema2,
+    lb_entanglement: Ema2,
+    /// the decision level used in th last invocation of `reduce`
+    last_reduction_threshold: usize,
 
     //
     //## incremental solving
@@ -307,10 +313,11 @@ pub mod property {
         NumLearnt,
         NumReduction,
         NumReRegistration,
+        ReductionThreshold,
         Timestamp,
     }
 
-    pub const USIZES: [Tusize; 9] = [
+    pub const USIZES: [Tusize; 10] = [
         Tusize::NumBiClause,
         Tusize::NumBiClauseCompletion,
         Tusize::NumBiLearnt,
@@ -319,6 +326,7 @@ pub mod property {
         Tusize::NumLearnt,
         Tusize::NumReduction,
         Tusize::NumReRegistration,
+        Tusize::ReductionThreshold,
         Tusize::Timestamp,
     ];
 
@@ -334,6 +342,7 @@ pub mod property {
                 Tusize::NumLearnt => self.num_learnt,
                 Tusize::NumReduction => self.num_reduction,
                 Tusize::NumReRegistration => self.num_reregistration,
+                Tusize::ReductionThreshold => self.last_reduction_threshold,
 
                 #[cfg(feature = "clause_rewarding")]
                 Tusize::Timestamp => self.tick,