20240728 rewrite conflict_analyze (#259)

* bump to 0.18.0-dev5

* conflict-side-rewarding + just_used (non)reduction

* cargo: update rust-verion; cargo update

* (conflict_analyze) Switch from `loop` to `for`

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "splr"
-version = "0.18.0-dev4"
+version = "0.18.0-dev5"
 authors = ["Narazaki Shuji <[email protected]>"]
 description = "A modern CDCL SAT solver in Rust"
 edition = "2021"
@@ -11,7 +11,10 @@ homepage = "https://github.com/shnarazk/splr"
 keywords = ["SAT", "SAT-solver", "logic", "satisfiability"]
 categories = ["science", "mathematics"]
 default-run = "splr"
-rust-version = "1.79"
+rust-version = "1.80"
+
+[build]
+rustflags = ["-C", "target-cpu=native"]
 
 [dependencies]
 bitflags = "^2.6"
@@ -30,7 +33,7 @@ default = [
         # "bi_clause_completion",
         # "clause_rewarding",
         # "dynamic_restart_threshold",
-        # "just_used",
+        "just_used",
         "LRB_rewarding",
         "reason_side_rewarding",
         "rephase",

ChangeLog.md

@@ -100,9 +100,9 @@
 ## 0.10.0, 2021-07-10
 
 ### Fix critical bugs
-- fix bugs on chronoBT implementation, which have affected Splr from version 0.3.1 to 0.7.0.
-   - `AssignStack::q_head` had a wrong index after backtrack if chronoBT was used.
-   - Non-chronoBT was broken if the number of the highest literal in conflicting clauses is one.
+- fix bugs on chrono_BT implementation, which have affected Splr from version 0.3.1 to 0.7.0.
+   - `AssignStack::q_head` had a wrong index after backtrack if chrono_BT was used.
+   - Non-chrono_BT was broken if the number of the highest literal in conflicting clauses is one.
 - fix a bug which has been rarely occurred by eliminator.
    - `AssignIF::propagate` skipped clause-level satisfiability checking,
      if its `blocker` held an eliminated var, which was never falsified.
@@ -226,7 +226,7 @@ functions more rigidly.
 - delete dependencies on 'libc' and 'structopt'
 - make Splr deterministic or *monotonous*, by removing timer based decision makers. Monotonous means that if a solver solves a problem within T timeout, it solves the problem within any timeout longer than T.
 - Solver::restart provides both of `restart` and `stabilize`
-- fix a bug in chronoBT, that occurred if a conflicting clause has just a single literal at the conflicting level.
+- fix a bug in chrono_BT, that occurred if a conflicting clause has just a single literal at the conflicting level.
 - revise command line option parser to handle the last option better
 - stabilization span and restart blocking levels are controlled with Luby sequence
 - add an extra reward to vars involved in best phase

src/assign/propagate.rs

@@ -95,7 +95,7 @@ impl PropagateIF for AssignStack {
     ) {
         debug_assert!(usize::from(l) != 0, "Null literal is about to be enqueued");
         debug_assert!(l.vi() < self.var.len());
-        // The following doesn't hold anymore by using chronoBT.
+        // The following doesn't hold anymore by using chrono_BT.
         // assert!(self.trail_lim.is_empty() || !cid.is_none());
         let vi = l.vi();
         // debug_assert!([Some(bool::from(l)), None].contains(&self.var[vi].assign));
@@ -224,7 +224,7 @@ impl PropagateIF for AssignStack {
         // debug_assert!(self.trail.iter().all(|l| self.var[l.vi()].assign.is_some()));
         // debug_assert!(self.trail.iter().all(|k| !self.trail.contains(&!*k)));
         self.trail_lim.truncate(lv as usize);
-        // assert!(lim < self.q_head) doesn't hold sometimes in chronoBT.
+        // assert!(lim < self.q_head) doesn't hold sometimes in chrono_BT.
         if lv == self.root_level {
             self.num_restart += 1;
             self.cpr_ema.update(self.num_conflict);

src/assign/stack.rs

@@ -204,7 +204,7 @@ impl Instantiate for AssignStack {
     #[inline]
     fn handle(&mut self, e: SolverEvent) {
         match e {
-            // called only by assertion on chronoBT
+            // called only by assertion on chrono_BT
             // So execute everything of `assign_by_unitclause` but cancel_until(root_level)
             SolverEvent::Conflict => (),
             SolverEvent::Eliminate(vi) => {

src/cdb/mod.rs

@@ -495,7 +495,7 @@ impl ClauseDBIF for ClauseDB {
             }
         }
     }
-    // used in `propagate`, `propagate_sandbox`, and `handle_conflict` for chronoBT
+    // used in `propagate`, `propagate_sandbox`, and `handle_conflict` for chrono_BT
     #[inline]
     fn transform_by_updating_watch(
         &mut self,
@@ -519,7 +519,7 @@ impl ClauseDBIF for ClauseDB {
         if learnt {
             #[cfg(feature = "just_used")]
             c.turn_on(FlagClause::USED);
-            #[cfg(feature = "clause_rewading")]
+            #[cfg(feature = "clause_rewarding")]
             self.reward_at_analysis(ci);
         }
         if 1 < rank {
@@ -1328,15 +1328,15 @@ mod tests {
         assert!(!c.is_dead());
         assert!(!c.is(FlagClause::LEARNT));
         #[cfg(feature = "just_used")]
-        assert!(!c.is(FlagClause::USED));
+        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")]
-        assert!(!c.is(FlagClause::USED));
+        assert!(c.is(FlagClause::USED));
     }
     #[test]
     fn test_clause_equality() {

src/config.rs

@@ -9,7 +9,7 @@ pub struct Config {
     //
     //## solver configuration
     //
-    /// Dec. lvl to use chronoBT
+    /// Dec. lvl to use chrono_BT
     pub c_cbt_thr: DecisionLevel,
 
     /// Soft limit of #clauses (6MC/GB)
@@ -428,21 +428,21 @@ pub mod property {
 
     #[derive(Clone, Copy, Debug, Eq, PartialEq)]
     pub enum Tf64 {
-        #[cfg(feature = "clase_rewarding")]
+        #[cfg(feature = "clause_rewarding")]
         ClauseRewardDecayRate,
         VarRewardDecayRate,
     }
 
-    #[cfg(not(feature = "clase_rewarding"))]
+    #[cfg(not(feature = "clause_rewarding"))]
     pub const F64S: [Tf64; 1] = [Tf64::VarRewardDecayRate];
-    #[cfg(feature = "clase_rewarding")]
+    #[cfg(feature = "clause_rewarding")]
     pub const F64S: [Tf64; 2] = [Tf64::ClauseRewardDecayRate, Tf64::VarRewardDecayRate];
 
     impl PropertyDereference<Tf64, f64> for Config {
         #[inline]
         fn derefer(&self, k: Tf64) -> f64 {
             match k {
-                #[cfg(feature = "clase_rewarding")]
+                #[cfg(feature = "clause_rewarding")]
                 Tf64::ClauseRewardDecayRate => self.crw_dcy_rat,
                 Tf64::VarRewardDecayRate => self.vrw_dcy_rat,
             }

src/processor/mod.rs

@@ -55,8 +55,10 @@ pub trait EliminateIF: Instantiate {
     /// enqueue a var into eliminator's var queue.
     fn enqueue_var(&mut self, asg: &mut impl AssignIF, vi: VarId, upward: bool);
     /// simplify database by:
+    ///
     /// * removing satisfiable clauses
     /// * calling exhaustive simplifier that tries **clause subsumption** and **variable elimination**.
+    ///
     /// Note: `force_run` is used only at the beginning of `solve' for simple satisfiability check
     ///
     /// # Errors