A snapshot

shnarazk · Nov 26, 2024 · de566a2 · de566a2
1 parent b447cd6
commit de566a2
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 24 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
@@ -569,7 +569,7 @@ impl ClauseDBIF for ClauseDB {
             if new {
                 self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
             }
-            if bck {
+            if fwd {
                 continue;
             }
             if new_assertion && self.clause[ci].is_satisfied_under(asg) {

diff --git a/src/solver/search.rs b/src/solver/search.rs
@@ -17,7 +17,6 @@ pub struct SearchState {
     num_reduction: usize,
     new_assertion: bool,
     reduce_step: usize,
-    restart_span: usize,
     next_restart: usize,
     next_reduce: usize,
     current_core: usize,
@@ -428,7 +427,6 @@ impl SolveIF for Solver {
             num_reduction: 0,
             new_assertion: false,
             reduce_step: (nv + nc) as usize,
-            restart_span: 4,
             next_reduce: 64,
             next_restart: 1024,
             from_segment_beginning: 0,
@@ -479,26 +477,17 @@ impl SolveIF for Solver {
             }
             let num_conflict = asg.derefer(assign::Tusize::NumConflict);
             let with_restart = ss.next_restart <= num_conflict
-                && 0.8 <= cdb.refer(cdb::property::TEma::LBD).trend();
+                && 1.0 <= cdb.refer(cdb::property::TEma::LBD).trend();
             if with_restart {
                 RESTART!(asg, cdb, state);
                 asg.clear_asserted_literals(cdb)?;
-                // let lbd = cdb.refer(cdb::property::TEma::LBD).get();
-                // let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow();
-                // let k: f64 = (state.stm.current_segment() as f64).log2();
-                // let ratio: f64 = state.stm.segment_progress_ratio();
-                // let x: f64 = k * (2.0 * ratio - 1.0);
-                // let sgm = |x: f64| 1.0 / (1.0 + (-x).exp());
-                // ss.next_restart = num_conflict + (((ent + lbd) * sgm(x)) as usize).max(6);
-                ss.restart_span = 8;
-                ss.next_restart = num_conflict + ss.restart_span;
+                ss.next_restart = num_conflict + 12;
                 #[cfg(feature = "trace_equivalency")]
                 cdb.check_consistency(asg, "before simplify");
             } else if ss.next_restart <= num_conflict
-                && cdb.refer(cdb::property::TEma::LBD).trend() <= 0.5
+                && cdb.refer(cdb::property::TEma::LBD).trend() <= 0.75
             {
-                ss.restart_span *= 2;
-                ss.next_restart = num_conflict + ss.restart_span;
+                // ss.next_restart = num_conflict + 4;
             }
             ss.from_segment_beginning += 1;
             if ss.current_span <= ss.from_segment_beginning {
@@ -551,9 +540,10 @@ impl SolveIF for Solver {
                     // a beginning of a new cycle
                     let stm = &state.stm;
                     if cfg!(feature = "reward_annealing") {
-                        let k: f64 = (stm.current_segment() as f64).log2();
+                        // let k: f64 = (stm.current_segment() as f64).log2();
+                        let k: f64 = (stm.current_segment() as f64).sqrt();
                         let ratio: f64 = stm.segment_progress_ratio();
-                        const R: (f64, f64) = (0.9, 0.98);
+                        const R: (f64, f64) = (0.94, 0.97);
                         let x: f64 = k * (2.0 * ratio - 1.0);
                         let r = {
                             let sgm = 1.0 / (1.0 + (-x).exp());