20241115 orthogonal restart

src/assign/mod.rs

@@ -1,6 +1,6 @@
 /// Module `assign` implements Boolean Constraint Propagation and decision var selection.
 /// This version can handle Chronological and Non Chronological Backtrack.
-
+///
 /// Ema
 mod ema;
 /// Heap
@@ -54,7 +54,7 @@ pub trait AssignIF:
 {
     /// return root level.
     fn root_level(&self) -> DecisionLevel;
-    /// return a literal in the stack.
+    /// return the `i`-th literal in the stack.
     fn stack(&self, i: usize) -> Lit;
     /// return literals in the range of stack.
     fn stack_range(&self, r: Range<usize>) -> &[Lit];

src/assign/stack.rs

@@ -212,6 +212,10 @@ impl Instantiate for AssignStack {
             SolverEvent::Eliminate(vi) => {
                 self.make_var_eliminated(vi);
             }
+            SolverEvent::Restart => {
+                #[cfg(feature = "trail_saving")]
+                self.clear_saved_trail();
+            }
             SolverEvent::Stage(scale) => {
                 self.stage_scale = scale;
                 #[cfg(feature = "trail_saving")]

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();
+            }
             _ => (),
         }
     }

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);
     }

src/cdb/mod.rs

@@ -87,12 +87,14 @@ pub trait ClauseDBIF:
     /// reduce learnt clauses
     /// # CAVEAT
     /// *precondition*: decision level == 0.
-    fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64);
+    fn reduce(&mut self, asg: &impl AssignIF, threshold: f64, new_assertion: bool);
     /// remove all learnt clauses.
     fn reset(&mut self);
     /// update flags.
     /// return `true` if it's learnt.
     fn update_entanglement(&mut self, asg: &impl AssignIF, ci: ClauseIndex);
+    /// update LBD and return the new value
+    fn update_lbd(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> DecisionLevel;
     /// record an asserted literal to unsat certification.
     fn certificate_add_assertion(&mut self, lit: Lit);
     /// save the certification record to a file.
@@ -518,21 +520,29 @@ impl ClauseDBIF for ClauseDB {
         let rank: DecisionLevel = c.update_lbd(asg, lbd_temp);
         self.lb_entanglement.update(rank as f64);
     }
+    fn update_lbd(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> DecisionLevel {
+        let ClauseDB {
+            ref mut clause,
+            ref mut lbd_temp,
+            ..
+        } = self;
+        let c = &mut clause[ci];
+        c.update_lbd(asg, lbd_temp)
+    }
     /// reduce the number of 'learnt' or *removable* clauses.
     #[cfg(feature = "keep_just_used_clauses")]
-    fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64) {
-        impl Clause {
-            fn extended_lbd(&self) -> f64 {
-                let l: f64 = self.len() as f64;
-                let r: f64 = self.rank as f64;
-                r + (l - r) / (l - r + 1.0)
-            }
-        }
+    fn reduce(&mut self, asg: &impl AssignIF, threshold: f64, new_assertion: bool) {
+        // impl Clause {
+        //     fn extended_lbd(&self) -> f64 {
+        //         let l: f64 = self.len() as f64;
+        //         let r: f64 = self.rank as f64;
+        //         r + (l - r) / (l - r + 1.0)
+        //     }
+        // }
         // let ClauseDB {
         //     ref mut clause,
         //     ref mut lbd_temp,
         //     ref mut num_reduction,
-
         //     #[cfg(feature = "clause_rewarding")]
         //     ref tick,
         //     #[cfg(feature = "clause_rewarding")]
@@ -542,71 +552,42 @@ impl ClauseDBIF for ClauseDB {
         self.num_reduction += 1;
         // let mut keep: usize = 0;
         // let mut alives: usize = 0;
-        // let mut perm: Vec<OrderedProxy<ClauseIndex>> = Vec::with_capacity(clause.len());
         // let reduction_threshold = self.reduction_threshold + 4;
         for ci in 1..self.clause.len() {
             if self.clause[ci].is_dead() {
                 continue;
             }
-            // alives += 1;
-            // keep += 1;
-            self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
-            // if self.clause[ci].is(FlagClause::FORWD_LINK)
-            //     || self.clause[ci].is(FlagClause::BCKWD_LINK)
-            // {
-            //     self.clause[ci].turn_off(FlagClause::FORWD_LINK);
-            //     self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
-            //     continue;
-            // }
-            /* let fwd: bool = self.clause[ci].is(FlagClause::FORWD_LINK);
-            self.clause[ci].turn_off(FlagClause::FORWD_LINK);
-            if self.clause[ci].is(FlagClause::BCKWD_LINK) {
-                self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
-                continue;
-            } */
-            if self.clause[ci].is(FlagClause::FORWD_LINK)
-                || self.clause[ci].is(FlagClause::BCKWD_LINK)
-            {
+            let fwd = self.clause[ci].is(FlagClause::FORWD_LINK);
+            if fwd {
                 self.clause[ci].turn_off(FlagClause::FORWD_LINK);
+            }
+            let bck = self.clause[ci].is(FlagClause::BCKWD_LINK);
+            if bck {
                 self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
+            }
+            let new = self.clause[ci].is(FlagClause::NEW_CLAUSE);
+            if new {
+                self.clause[ci].turn_off(FlagClause::NEW_CLAUSE);
+            }
+            if bck && new && self.clause[ci].rank <= (2 * threshold as DecisionLevel) / 3 {
                 continue;
             }
-            /* let bwd: bool = self.clause[ci].is(FlagClause::BCKWD_LINK);
-            if bwd {
-                self.clause[ci].turn_off(FlagClause::BCKWD_LINK);
-            } */
-            if self.clause[ci].is(FlagClause::LEARNT) {
-                let ClauseDB {
-                    ref mut clause,
-                    ref mut lbd_temp,
-                    ..
-                } = self;
-                if clause[ci].rank < threshold as DecisionLevel {
-                    continue;
-                }
-                clause[ci].update_lbd(asg, lbd_temp);
-                if threshold < clause[ci].extended_lbd() {
-                    // keep -= 1;
-                    // perm.push(OrderedProxy::new(ci, c.rank as f64));
-                    self.delete_clause(ci);
-                    continue;
-                }
+            if new_assertion && self.clause[ci].is_satisfied_under(asg) {
+                self.delete_clause(ci);
+                continue;
+            }
+            if !self.clause[ci].is(FlagClause::LEARNT) {
+                continue;
+            }
+            // alives += 1;
+            // keep += 1;
+            if (threshold as DecisionLevel) < self.clause[ci].rank
+            /* extended_lbd() */
+            {
+                // keep -= 1;
+                self.delete_clause(ci);
             }
         }
-        // let keep = perm.len().max(alives);
-        // if perm.is_empty() {
-        //     return;
-        // }
-        // perm.sort();
-        // let threshold = perm[keep.min(perm.len() - 1)].value();
-        // for i in perm.iter().skip(keep) {
-        //     // Being clause-position-independent, we keep or delete
-        //     // all clauses that have a same value as a unit.
-        //     if i.value() == threshold {
-        //         continue;
-        //     }
-        //     self.delete_clause(i.to());
-        // }
     }
     #[cfg(not(feature = "keep_just_used_clauses"))]
     #[allow(unreachable_code, unused_variables)]