Reset lbd short after restart; more vivificataions; no cool down to r…

…estart
shnarazk · Nov 28, 2024 · cf28124 · cf28124
1 parent de566a2
commit cf28124
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 12 deletions.
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
@@ -164,7 +164,9 @@ impl Instantiate for ClauseDB {
                 self.watch.push(WatchLiteralIndexRef::default());
                 self.lbd_temp.push(0);
             }
-            SolverEvent::Restart => (),
+            SolverEvent::Restart => {
+                self.lbd.reset_fast();
+            }
             _ => (),
         }
     }

diff --git a/src/cdb/ema.rs b/src/cdb/ema.rs
@@ -49,6 +49,9 @@ impl EmaMutIF for ProgressLBD {
         self.sum += d as usize;
         self.ema.update(d as f64);
     }
+    fn reset_fast(&mut self) {
+        self.ema.reset_fast();
+    }
     fn reset_to(&mut self, val: f64) {
         self.ema.reset_to(val);
     }

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 fwd {
+            if bck {
                 continue;
             }
             if new_assertion && self.clause[ci].is_satisfied_under(asg) {

diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
@@ -36,7 +36,7 @@ impl VivifyIF for ClauseDB {
         let display_step: usize = 1000;
         let mut num_checked: usize = 0;
         let mut num_shrink: usize = 0;
-        let mut num_subsumed: usize = 0;
+        // let mut num_subsumed: usize = 0;
         let mut num_assert: usize = 0;
         let mut to_display: usize = 0;
         'next_clause: while let Some(cp) = clauses.pop() {
@@ -60,7 +60,7 @@ impl VivifyIF for ClauseDB {
             if to_display <= num_checked {
                 state.flush("");
                 state.flush(format!(
-                    "vivifying(assert:{num_assert} subsume:{num_subsumed}, shorten:{num_shrink}, check:{num_checked}/{num_target})..."
+                    "vivifying(assert:{num_assert}, shorten:{num_shrink}, check:{num_checked}/{num_target})..."
                 ));
                 to_display = num_checked + display_step;
             }
@@ -104,7 +104,7 @@ impl VivifyIF for ClauseDB {
                             AssignReason::Implication(wli) => {
                                 if wli.as_ci() != ci {
                                     asg.backtrack_sandbox();
-                                    if decisions.len() < clits.len()
+                                    /* if decisions.len() < clits.len()
                                         && self.clause[wli.as_ci()]
                                             .iter()
                                             .all(|l| decisions.contains(l))
@@ -116,7 +116,7 @@ impl VivifyIF for ClauseDB {
                                             self.clause[wli.as_ci()].turn_off(FlagClause::LEARNT);
                                         }
                                         num_subsumed += 1;
-                                    }
+                                    } */
                                     continue 'next_clause;
                                 }
                                 if wli.as_ci() == ci && clits.len() == decisions.len() {
@@ -182,7 +182,7 @@ impl VivifyIF for ClauseDB {
         debug_assert!(asg.stack_is_empty() || !asg.remains());
         state.flush("");
         state.flush(format!(
-            "vivified(assert:{num_assert}, subsume:{num_subsumed}, shorten:{num_shrink}), "
+            "vivified(assert:{num_assert}, shorten:{num_shrink}), "
         ));
         // state.log(
         //     asg.num_conflict,

diff --git a/src/solver/search.rs b/src/solver/search.rs
@@ -476,12 +476,12 @@ impl SolveIF for Solver {
                 _ => (),
             }
             let num_conflict = asg.derefer(assign::Tusize::NumConflict);
-            let with_restart = ss.next_restart <= num_conflict
-                && 1.0 <= cdb.refer(cdb::property::TEma::LBD).trend();
+            let with_restart = /* ss.next_restart <= num_conflict
+                && */ 1.2 <= cdb.refer(cdb::property::TEma::LBD).trend();
             if with_restart {
                 RESTART!(asg, cdb, state);
                 asg.clear_asserted_literals(cdb)?;
-                ss.next_restart = num_conflict + 12;
+                // ss.next_restart = num_conflict + 12;
                 #[cfg(feature = "trace_equivalency")]
                 cdb.check_consistency(asg, "before simplify");
             } else if ss.next_restart <= num_conflict
@@ -519,7 +519,7 @@ impl SolveIF for Solver {
                         ss.num_reduction += 1;
                         ss.reduce_step += ss.current_core.ilog2() as usize;
                         ss.next_reduce = ss.reduce_step + num_restart;
-                        if cfg!(feature = "clause_vivification") && ss.num_reduction % 8 == 0 {
+                        if cfg!(feature = "clause_vivification") && ss.num_reduction % 6 == 0 {
                             cdb.vivify(asg, state)?;
                         }
                         if cfg!(feature = "clause_elimination")
@@ -543,7 +543,7 @@ impl SolveIF for Solver {
                         // 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.94, 0.97);
+                        const R: (f64, f64) = (0.95, 0.99);
                         let x: f64 = k * (2.0 * ratio - 1.0);
                         let r = {
                             let sgm = 1.0 / (1.0 + (-x).exp());