a snapshot after some simplification

src/cdb/mod.rs

@@ -543,7 +543,10 @@ impl ClauseDBIF for ClauseDB {
             }
             // alives += 1;
             // keep += 1;
-            self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
+            if self.clause[ci].is(FlagClause::NEW_CLAUSE) {
+                self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
+                // continue;
+            }
             // if self.clause[ci].is(FlagClause::FORWD_LINK)
             //     || self.clause[ci].is(FlagClause::BCKWD_LINK)
             // {

src/solver/search.rs

@@ -497,48 +497,58 @@ impl SolveIF for Solver {
                     #[cfg(feature = "trace_equivalency")]
                     cdb.check_consistency(asg, "before simplify");
                 }
-                ss.current_span = state.stm.current_span() as usize;
+                let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
+                let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow();
+                ss.current_span = ent.max(lbd) as usize;
+                // ss.current_span = state.stm.current_span() as usize;
                 let scale = state.stm.current_scale();
                 asg.handle(SolverEvent::Stage(scale));
                 if let Some(new_segment) = next_stage {
                     // a beginning of a new cycle
                     {
-                        let stm = &state.stm;
-                        let b: f64 = stm.segment_starting_cycle() as f64;
-                        let n: f64 = stm.current_cycle() as f64 - b;
+                        // let stm = &state.stm;
+                        // let b: f64 = stm.segment_starting_cycle() as f64;
+                        // let n: f64 = stm.current_cycle() as f64 - b;
 
                         if cfg!(feature = "reward_annealing") {
+                            // const_R: (f64, f64) = (0.94, 0.99);
+                            // let k = stm.current_segment().ilog2() as f64;
+                            // let ratio = k / (k + 1.0);
+                            // let _ratio: f64 = stm.segment_progress_ratio();
+
+                            // let _r = R.0 + ratio * (R.1 - R.0);
+                            /*
                             let k: f64 = (stm.current_segment() as f64).log2();
-                            let ratio: f64 = stm.segment_progress_ratio();
                             const SLOP: f64 = 8.0;
-                            const R: (f64, f64) = (0.84, 0.995);
                             let d: f64 = R.1 - (R.1 - R.0) * SLOP / (k + SLOP);
                             let x: f64 = k * (2.0 * ratio - 1.0);
                             let r = {
                                 let sgm = |x: f64| 1.0 / (1.0 + (-x).exp());
                                 d + sgm(x) * (1.0 - d)
                             };
-                            asg.update_activity_decay(r);
+                            */
+                            asg.update_activity_decay(0.98);
                         }
 
                         let num_restart = asg.derefer(assign::Tusize::NumRestart);
                         if ss.next_reduce <= num_restart {
-                            let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
-                            let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow();
-                            // Note: val can be inf. It got better results.
-                            let val: f64 = 0.5 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2();
+                            // let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
+                            // let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow();
+                            // // Note: val can be inf. It got better results.
+                            // let val: f64 = 0.75 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2();
+                            let val = 5.0;
                             state.reduction_threshold = val;
                             cdb.reduce(asg, val);
                             ss.num_reduction += 1;
                             ss.reduce_step += 1;
                             ss.next_reduce = ss.reduce_step + num_restart;
 
-                            if cfg!(feature = "clause_vivification") {
+                            if cfg!(feature = "clause_vivification") && ss.num_reduction % 8 == 0 {
                                 cdb.vivify(asg, state)?;
                             }
                             if cfg!(feature = "clause_elimination")
                                 && !cfg!(feature = "incremental_solver")
-                                && ss.num_reduction % 8 == 0
+                                && ss.num_reduction % 15 == 0
                             {
                                 let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
                                 state.flush("clause subsumption, ");

src/solver/stage.rs

@@ -45,7 +45,7 @@ impl Instantiate for StageManager {
             scale: 1,
             end_of_stage: unit_size,
             next_is_new_segment: false,
-            span_ema: Ema::new(4).with_value(1.0),
+            span_ema: Ema::new(64).with_value(1.0),
             ..StageManager::default()
         }
     }
@@ -71,7 +71,7 @@ impl StageManager {
             segment_starting_stage: 0,
             segment_starting_cycle: 0,
             span_base: 0.0,
-            span_ema: Ema::new(4).with_value(1.0),
+            span_ema: Ema::new(64).with_value(1.0),
         }
     }
     pub fn initialize(&mut self, _unit_size: usize) {
@@ -103,7 +103,8 @@ impl StageManager {
         let mut new_cycle = false;
         let mut new_segment = false;
         self.scale = self.generator.next_number();
-        self.span_ema.update(4.0 + (self.scale as f64).powf(0.4));
+        // self.span_ema.update(4.0 + (self.scale as f64).powf(0.4));
+        self.span_ema.update(self.scale as f64);
         self.stage += 1;
         if self.scale == 1 {
             self.cycle += 1;
@@ -131,22 +132,29 @@ impl StageManager {
         self.end_of_stage as i32 - now as i32
     }
     /// returns the number of conflicts in the current stage
+    /// that was used as the number of conflicts that corresponds to the current stage
     /// Note: we need not to make a strong correlation between this value and
     /// scale defined by Luby series. So this is fine.
+    /// stage -> cycle -> segment
     pub fn current_span(&self) -> f64 {
         self.span_ema.get()
     }
+    /// returns the scaling factor, or length corresponding to the current stage
+    /// stage -> cycle -> segment
+    pub fn current_scale(&self) -> usize {
+        self.scale
+    }
+    /// return the index of the current stage    /// stage -> cycle -> segment
     pub fn current_stage(&self) -> usize {
         self.stage
     }
+    /// return the index of the current cycle
+    /// stage -> cycle -> segment
     pub fn current_cycle(&self) -> usize {
         self.cycle
     }
-    /// returns the scaling factor used in the current span
-    pub fn current_scale(&self) -> usize {
-        self.scale
-    }
     /// returns the current index for the level 2 segments
+    /// stage -> cycle -> segment
     pub fn current_segment(&self) -> usize {
         self.segment
     }