Remove RestartManager; rename feature 'just_used' to 'keep_just_used_…

…clauses'

Cargo.toml

@@ -29,8 +29,7 @@ default = [
         ### Heuristics
         # "bi_clause_completion",
         # "clause_rewarding",
-        # "dynamic_restart_threshold",
-        "just_used",
+        "keep_just_used_clauses",
         "LRB_rewarding",
         "reason_side_rewarding",
         # "rephase",
@@ -62,7 +61,6 @@ 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
 graph_view = [
@@ -73,7 +71,7 @@ graph_view = [
 ]
 incremental_solver = []         # for all solution SAT sover; requires no cluse_elimination
 interleave = []                 # switch to multi-step search IF
-just_used = []                  # Var and clause have 'just_used' flags
+keep_just_used_clauses = []     # Var and clause have 'just_used' flags
 LRB_rewarding = []              # Vearning Rate Based rewarding, a new var activity criteria
 no_IO = []                      # to embed Splr into non-std environments
 platform_wasm = [
@@ -84,7 +82,7 @@ rephase = [                     # search around the best-so-far candidate repeat
         "best_phases_tracking",
         ]
 reward_annealing = []           # use bigger and smaller decay rates cycliclly
-spin = []
+spin = []                       # [experimental] a sort of criteria for var categorization
 stochastic_local_search = [     # since 0.17
         # "reward_annealing",
         "rephase",

src/assign/propagate.rs

@@ -375,7 +375,7 @@ impl PropagateIF for AssignStack {
                                 .unwrap_or(self.root_level);
 
                             debug_assert_eq!(self.assigned(other), None);
-                            #[cfg(feature = "just_used")]
+                            #[cfg(feature = "keep_just_used_clauses")]
                             c.turn_on(FlagClause::USED);
                             self.assign_by_implication(
                                 other,

src/cdb/mod.rs

@@ -290,7 +290,7 @@ impl ClauseDBIF for ClauseDB {
             self.clause[ci].activity = 0.0;
             self.clause[ci].timestamp = self.tick;
         }
-        #[cfg(feature = "just_used")]
+        #[cfg(feature = "keep_just_used_clauses")]
         {
             self.clause[ci].turn_on(FlagClause::USED);
         }
@@ -518,7 +518,7 @@ impl ClauseDBIF for ClauseDB {
         let rank = c.update_lbd(asg, lbd_temp);
         let learnt = c.is(FlagClause::LEARNT);
         if learnt {
-            #[cfg(feature = "just_used")]
+            #[cfg(feature = "keep_just_used_clauses")]
             c.turn_on(FlagClause::USED);
             #[cfg(feature = "clause_rewarding")]
             self.reward_at_analysis(ci);
@@ -529,7 +529,7 @@ impl ClauseDBIF for ClauseDB {
         learnt
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    #[cfg(feature = "just_used")]
+    #[cfg(feature = "keep_just_used_clauses")]
     fn reduce(&mut self, asg: &mut impl AssignIF, _setting: ReductionType) {
         // let ClauseDB {
         //     ref mut clause,
@@ -586,7 +586,7 @@ impl ClauseDBIF for ClauseDB {
         //     self.delete_clause(i.to());
         // }
     }
-    #[cfg(not(feature = "just_used"))]
+    #[cfg(not(feature = "keep_just_used_clauses"))]
     #[allow(unreachable_code, unused_variables)]
     fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType) {
         impl Clause {
@@ -619,7 +619,7 @@ impl ClauseDBIF for ClauseDB {
             ReductionType::LBDonALL(_, _) => true,
             #[cfg(feature = "clause_rewarding")]
             ReductionType::ClauseActivity => false,
-            #[cfg(feature = "just_used")]
+            #[cfg(feature = "keep_just_used_clauses")]
             ReductionType::ClauseUsed => false,
         };
         for (ci, c) in clause
@@ -659,7 +659,7 @@ impl ClauseDBIF for ClauseDB {
                 }
                 #[cfg(feature = "clause_rewarding")]
                 ReductionType::ClauseActivity => perm.push(OrderedProxy::new(ci, -c.activity)),
-                #[cfg(feature = "just_used")]
+                #[cfg(feature = "keep_just_used_clauses")]
                 ReductionType::ClauseUsed => unreachable!(),
             }
         }
@@ -670,7 +670,7 @@ impl ClauseDBIF for ClauseDB {
             ReductionType::LBDonALL(_, scale) => (perm.len() as f64).powf(1.0 - scale) as usize,
             #[cfg(feature = "clause_rewarding")]
             ReductionType::ClauseActivity => (perm.len() as f64).powf(0.75) as usize,
-            #[cfg(feature = "just_used")]
+            #[cfg(feature = "keep_just_used_clauses")]
             ReductionType::ClauseUsed => unreachable!(),
         };
         if perm.is_empty() {
@@ -685,7 +685,7 @@ impl ClauseDBIF for ClauseDB {
             }
             #[cfg(feature = "clause_rewarding")]
             ReductionType::ClauseActivity => keep as f64 / alives as f64,
-            #[cfg(feature = "just_used")]
+            #[cfg(feature = "keep_just_used_clauses")]
             ReductionType::ClauseUsed => unreachable!(),
         };
         perm.sort();
@@ -1242,7 +1242,7 @@ pub enum ReductionType {
     LBDonALL(u16, f64),
     #[cfg(feature = "clause_rewarding")]
     ClauseActivity,
-    #[cfg(feature = "just_used")]
+    #[cfg(feature = "keep_just_used_clauses")]
     ClauseUsed,
 }
 
@@ -1373,15 +1373,15 @@ mod tests {
 
         assert!(!c.is_dead());
         assert!(!c.is(FlagClause::LEARNT));
-        #[cfg(feature = "just_used")]
+        #[cfg(feature = "keep_just_used_clauses")]
         assert!(c.is(FlagClause::USED));
         let c2 = cdb
             .new_clause(&mut asg, &mut vec![lit(-1), lit(2), lit(3)], true)
             .as_ci();
         let c = &cdb[c2];
         assert!(!c.is_dead());
         assert!(c.is(FlagClause::LEARNT));
-        #[cfg(feature = "just_used")]
+        #[cfg(feature = "keep_just_used_clauses")]
         assert!(c.is(FlagClause::USED));
     }
     #[test]

src/cdb/vivify.rs

@@ -102,7 +102,7 @@ impl VivifyIF for ClauseDB {
                             }
                             AssignReason::Implication(wli) => {
                                 if wli.as_ci() == ci && clits.len() == decisions.len() {
-                                    #[cfg(feature = "just_used")]
+                                    #[cfg(feature = "keep_just_used_clauses")]
                                     self.clause[wli.as_ci()].turn_on(FlagClause::USED);
                                     asg.backtrack_sandbox();
                                     continue 'next_clause;
@@ -280,7 +280,7 @@ impl AssignStack {
                     seen[bil.vi()] = key;
                 }
                 AssignReason::Implication(wli) => {
-                    #[cfg(feature = "just_used")]
+                    #[cfg(feature = "keep_just_used_clauses")]
                     cdb.clause[wli.as_ci()].turn_on(FlagClause::USED);
                     for (i, r) in cdb[wli.as_ci()].iter().enumerate() {
                         if i == wli.as_wi() {

src/config.rs

@@ -267,8 +267,6 @@ impl Config {
                 "stage-based clause elimination",
                 #[cfg(feature = "clause_vivification")]
                 "stage-based clause vivification",
-                #[cfg(feature = "dynamic_restart_threshold")]
-                "stage-based dynamic restart threshold",
                 #[cfg(feature = "EMA_calibration")]
                 "EMA calibration",
                 #[cfg(feature = "EVSIDS")]
@@ -277,8 +275,8 @@ impl Config {
                 "incremental solver",
                 #[cfg(feature = "interleave")]
                 "interleaving slover",
-                #[cfg(feature = "just_used")]
-                "use 'just used' flag",
+                #[cfg(feature = "keep_just_used_clauses")]
+                "keep clauses used in the last cycle",
                 #[cfg(feature = "LRB_rewarding")]
                 "Learning-Rate Based rewarding",
                 #[cfg(feature = "reason_side_rewarding")]

src/processor/eliminate.rs

@@ -158,7 +158,6 @@ pub fn eliminate_var(
     */
     elim[vi].clear();
     asg.handle(SolverEvent::Eliminate(vi));
-    state.restart.handle(SolverEvent::Eliminate(vi));
     elim.backward_subsumption_check(asg, cdb)
 }
 

src/solver/conflict.rs

@@ -113,7 +113,6 @@ pub fn handle_conflict(
                     unreachable!("handle_conflict::root_level_conflict_by_assertion");
                 }
                 let vi = l0.vi();
-                state.restart.handle(SolverEvent::Assert(vi));
                 state.stm.handle(SolverEvent::Assert(vi));
                 cdb.handle(SolverEvent::Assert(vi));
                 return Ok(0);
@@ -150,7 +149,7 @@ pub fn handle_conflict(
                 }
             }
             AssignReason::Implication(r) => {
-                #[cfg(feature = "just_used")]
+                #[cfg(feature = "keep_just_used_clauses")]
                 cdb[r.as_ci()].turn_on(FlagClause::USED);
                 for l in cdb[r.as_ci()].iter() {
                     let vi = l.vi();
@@ -353,7 +352,7 @@ fn conflict_analyze(
                 if !cdb[ci].is(FlagClause::LEARNT) {
                     state.derive20.push(ci);
                 } else {
-                    #[cfg(feature = "just_used")]
+                    #[cfg(feature = "keep_just_used_clauses")]
                     cdb[ci].turn_on(FlagClause::USED);
                 }
                 if max_lbd < cdb[ci].rank {

src/solver/mod.rs

@@ -3,8 +3,6 @@
 mod build;
 /// Module 'conflict' handles conflicts.
 mod conflict;
-/// Module `restart` provides restart heuristics.
-pub mod restart;
 /// CDCL search engine
 mod search;
 /// Stage manger (was Stabilizer)
@@ -14,7 +12,6 @@ mod validate;
 
 pub use self::{
     build::SatSolverIF,
-    restart::{RestartIF, RestartManager},
     search::{SearchState, SolveIF},
     stage::StageManager,
     validate::ValidateIF,

src/solver/search.rs

@@ -1,9 +1,6 @@
 //! Conflict-Driven Clause Learning Search engine
 use {
-    super::{
-        conflict::handle_conflict, restart::RestartIF, Certificate, Solver, SolverEvent,
-        SolverResult,
-    },
+    super::{conflict::handle_conflict, Certificate, Solver, SolverEvent, SolverResult},
     crate::{
         assign::{self, AssignIF, AssignStack, PropagateIF, VarManipulateIF, VarSelectIF},
         cdb::{self, ClauseDB, ClauseDBIF, ReductionType, VivifyIF},
@@ -485,7 +482,6 @@ impl SolveIF for Solver {
                 ss.current_span = state.stm.current_span();
                 let scale = state.stm.current_scale();
                 asg.handle(SolverEvent::Stage(scale));
-                let max_scale = state.stm.max_scale();
                 if let Some(new_segment) = next_stage {
                     // a beginning of a new cycle
                     if cfg!(feature = "reward_annealing") {
@@ -534,9 +530,6 @@ impl SolveIF for Solver {
                             state[Stat::Simplify] += 1;
                             state[Stat::SubsumedClause] = elim.num_subsumed;
                         }
-                        if cfg!(feature = "dynamic_restart_threshold") {
-                            state.restart.set_segment_parameters(max_scale);
-                        }
                     }
                     if new_segment {
                         state.exploration_rate_ema.update(1.0);
@@ -547,7 +540,6 @@ impl SolveIF for Solver {
                                 return Err(SolverError::TimeOut);
                             }
                             state.progress(asg, cdb);
-                            state.restart.set_stage_parameters(scale);
                             ss.previous_stage = next_stage;
                             ss.elapsed_time = p;
                             return Ok(None);
@@ -654,26 +646,20 @@ impl SolveIF for Solver {
 
 /// display the current stats. before updating stabiliation parameters
 fn dump_stage(asg: &AssignStack, cdb: &mut ClauseDB, state: &mut State, shift: &Option<bool>) {
-    let active = true; // state.rst.enable;
     let cycle = state.stm.current_cycle();
     let span = state.stm.current_span();
     let stage = state.stm.current_stage();
     let segment = state.stm.current_segment();
     let cpr = asg.refer(assign::property::TEma::ConflictPerRestart).get();
     let vdr = asg.derefer(assign::property::Tf64::VarDecayRate);
     let cdt = cdb.derefer(cdb::property::Tf64::ReductionThreshold);
-    let fuel = if active {
-        state.restart.penetration_energy_charged
-    } else {
-        f64::NAN
-    };
     state.log(
         match shift {
             None => Some((None, None, stage)),
             Some(false) => Some((None, Some(cycle), stage)),
             Some(true) => Some((Some(segment), Some(cycle), stage)),
         },
-        format!("{span:>7}, fuel:{fuel:>9.2}, cpr:{cpr:>8.2}, vdr:{vdr:>3.2}, cdt:{cdt:>5.2}"),
+        format!("{span:>7}, cpr:{cpr:>8.2}, vdr:{vdr:>3.2}, cdt:{cdt:>5.2}"),
     );
 }