And revise vivification 20260304

Cargo.toml

@@ -21,7 +21,9 @@ instant = { version = "0.1", features = ["wasm-bindgen"], optional = true }
 default = [
     ### Essential
     "unsafe_access",
-    "chrono_BT",
+    # "chrono_BT",
+    "trail_saving",
+    "BT_drift",
 
     ### Heuristics
     # "bi_clause_completion",
@@ -34,7 +36,6 @@ default = [
     # "stochastic_local_search",
     # "suppress_reason_chain",
     "two_mode_reduction",
-    # "trail_saving",
 
     ### Logic formula processor
     "clause_elimination",
@@ -51,6 +52,7 @@ assign_rate = []                # for debug and study
 best_phases_tracking = []       # save the best-so-far assignment, used by 'rephase'
 bi_clause_completion = []       # this will increase memory pressure
 boundary_check = []             # for debug
+BT_drift = []                   # backtrack drift
 chrono_BT = []                  # NOT WORK
 clause_elimination = []         # pre(in)-processor setting
 clause_rewarding = []           # clauses have activities w/ decay rate

src/assign/mod.rs

@@ -57,6 +57,7 @@ pub trait AssignIF:
     /// ## Caveat
     /// - it emits a panic by out of index range.
     /// - it emits a panic if the level is 0.
+    ///
     /// CAVEAT: this return a wrong value under chrono_BT
     fn len_upto(&self, n: DecisionLevel) -> usize;
     /// return `true` if there's no assignment.

src/assign/propagate.rs

@@ -599,6 +599,7 @@ impl PropagateIF for AssignStack {
                 //             .collect::<Vec<_>>()
                 //     );
                 // }
+                cdb[cid].used = cdb[cid].used.saturating_add(1);
                 self.assign_by_implication(
                     cached,
                     AssignReason::Implication(cid),

src/assign/trail_saving.rs

@@ -54,11 +54,7 @@ impl TrailSavingIF for AssignStack {
         let q = self.stage_scale.trailing_zeros() as u16
             + (cdb.derefer(crate::cdb::property::Tf64::LiteralBlockEntanglement) as u16) / 2;
 
-        let dl = if cfg!(feature = "chrono_BT") {
-            self.decision_level()
-        } else {
-            0
-        };
+        let dl = self.decision_level();
 
         for i in (0..self.trail_saved.len()).rev() {
             let lit = self.trail_saved[i];

src/cdb/db.rs

@@ -354,6 +354,7 @@ impl ClauseDBIF for ClauseDB {
             // }
             // assert!(c.is_dead());
             c.flags = FlagClause::empty();
+            c.used = 0;
 
             #[cfg(feature = "clause_rewarding")]
             {
@@ -392,14 +393,14 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
+        c.used = 0;
         #[cfg(feature = "clause_rewarding")]
         {
             c.timestamp = *tick;
         }
         let len2 = c.lits.len() == 2;
         if len2 {
             c.rank = 1;
-            c.rank_old = 1;
 
             #[cfg(feature = "bi_clause_completion")]
             if learnt {
@@ -411,7 +412,6 @@ impl ClauseDBIF for ClauseDB {
             }
         } else {
             c.update_lbd(asg, lbd_temp);
-            c.rank_old = c.rank;
         }
         self.lbd.update(c.rank);
         *num_clause += 1;
@@ -449,6 +449,7 @@ impl ClauseDBIF for ClauseDB {
             cid = cid_used;
             let c = &mut self[cid];
             c.flags = FlagClause::empty();
+            c.used = 0;
             std::mem::swap(&mut c.lits, vec);
             c.search_from = 2;
         } else {
@@ -471,6 +472,7 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
+        c.used = 0;
 
         #[cfg(feature = "clause_rewarding")]
         {
@@ -480,10 +482,8 @@ impl ClauseDBIF for ClauseDB {
         let len2 = c.lits.len() == 2;
         if len2 {
             c.rank = 1;
-            c.rank_old = 1;
         } else {
             c.update_lbd(asg, lbd_temp);
-            c.rank_old = c.rank;
             c.turn_on(FlagClause::LEARNT);
         }
         let l0 = c.lits[0];
@@ -1062,21 +1062,24 @@ impl ClauseDBIF for ClauseDB {
                 continue;
             }
             alives += 1;
+            if c.rank <= 4 {
+                continue;
+            }
             match setting {
                 ReductionType::RASonADD(_) => {
                     perm.push(OrderedProxy::new(i, c.reverse_activity_sum(asg)));
                 }
                 ReductionType::RASonALL(cutoff, _) => {
                     let value = c.reverse_activity_sum(asg);
-                    if cutoff < value.min(c.rank_old as f64) {
+                    if cutoff < value.min(c.rank as f64) {
                         perm.push(OrderedProxy::new(i, value));
                     }
                 }
                 ReductionType::LBDonADD(_) => {
                     perm.push(OrderedProxy::new(i, c.lbd()));
                 }
                 ReductionType::LBDonALL(cutoff, _) => {
-                    let value = c.rank.min(c.rank_old);
+                    let value = c.rank;
                     if cutoff < value {
                         perm.push(OrderedProxy::new(i, value as f64));
                     }

src/cdb/vivify.rs

@@ -7,7 +7,7 @@ use crate::{
     types::*,
 };
 
-const VIVIFY_LIMIT: usize = 80_000;
+const VIVIFY_LIMIT: usize = 20_000;
 
 pub trait VivifyIF {
     fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent;
@@ -24,12 +24,12 @@ impl VivifyIF for ClauseDB {
             })?;
         }
         let mut clauses: Vec<OrderedProxy<ClauseId>> =
-            select_targets(asg, self, state[Stat::Restart] == 0, NUM_TARGETS);
+            select_targets(asg, self, state, state[Stat::Restart] == 0, NUM_TARGETS);
+        state[Stat::Vivification] += 1;
         if clauses.is_empty() {
             return Ok(());
         }
         let num_target = clauses.len();
-        state[Stat::Vivification] += 1;
         // This is a reusable vector to reduce memory consumption,
         // the key is the number of invocation
         let mut seen: Vec<usize> = vec![0; asg.num_vars + 1];
@@ -183,13 +183,14 @@ impl VivifyIF for ClauseDB {
 fn select_targets(
     asg: &mut AssignStack,
     cdb: &mut ClauseDB,
+    state: &State,
     initial_stage: bool,
     len: Option<usize>,
 ) -> Vec<OrderedProxy<ClauseId>> {
     if initial_stage {
         let mut seen: Vec<Option<OrderedProxy<ClauseId>>> = vec![None; 2 * (asg.num_vars + 1)];
         for (i, c) in cdb.iter().enumerate().skip(1) {
-            if let Some(rank) = c.to_vivify(true) {
+            if let Some(rank) = c.to_vivify(None) {
                 let p = &mut seen[usize::from(c.lit0())];
                 if p.as_ref().map_or(0.0, |r| r.value()) < rank {
                     *p = Some(OrderedProxy::new(ClauseId::from(i), rank));
@@ -205,15 +206,26 @@ fn select_targets(
         }
         clauses
     } else {
+        let n = state[Stat::Vivification] % 32;
+        let mut skips = 0;
         let mut clauses: Vec<OrderedProxy<ClauseId>> = cdb
             .iter()
             .enumerate()
             .skip(1)
             .filter_map(|(i, c)| {
-                c.to_vivify(false)
-                    .map(|r| OrderedProxy::new_invert(ClauseId::from(i), r))
+                c.to_vivify(Some(n as u16)).and_then(|r| {
+                    if r == 0.0 {
+                        skips += 1;
+                        None
+                    } else {
+                        Some(OrderedProxy::new_invert(ClauseId::from(i), r))
+                    }
+                })
             })
             .collect::<Vec<_>>();
+        // if skips < clauses.len() {
+        //     return vec![];
+        // }
         if let Some(max_len) = len {
             if max_len < clauses.len() {
                 clauses.sort();
@@ -342,21 +354,30 @@ impl Clause {
         }
     }
     #[cfg(not(feature = "clause_rewarding"))]
-    fn to_vivify(&self, initial_stage: bool) -> Option<f64> {
-        if initial_stage {
-            (!self.is_dead()).then(|| self.len() as f64)
+    fn to_vivify(&self, initial_stage: Option<u16>) -> Option<f64> {
+        if let Some(n) = initial_stage {
+            if n == 0 {
+                (
+                    !self.is_dead() && self.rank < 2
+                    // && (self.rank as usize) * 2 <= self.len()
+                    // && (self.is(FlagClause::LEARNT) || self.is(FlagClause::DERIVE20))
+                )
+                .then(|| -((self.len() as f64 - self.rank as f64) / self.rank as f64))
+            } else {
+                (!self.is_dead() && self.rank == n && self.used >= 4).then(|| {
+                    if (self.rank as usize) < self.len() {
+                        -(self.len() as f64) / self.rank as f64
+                    } else {
+                        0.0
+                    }
+                })
+            }
         } else {
-            (!self.is_dead()
-                && self.rank * 2 <= self.rank_old
-                && (self.is(FlagClause::LEARNT) || self.is(FlagClause::DERIVE20)))
-            .then(|| -((self.rank_old - self.rank) as f64 / self.rank as f64))
+            (!self.is_dead()).then(|| self.len() as f64)
         }
     }
     /// clear flags about vivification
     fn vivified(&mut self) {
-        self.rank_old = self.rank;
-        if !self.is(FlagClause::LEARNT) {
-            self.turn_off(FlagClause::DERIVE20);
-        }
+        self.used = 0;
     }
 }

src/solver/conflict.rs

@@ -2,6 +2,8 @@
 
 #[cfg(feature = "boundary_check")]
 use crate::assign::DebugReportIF;
+#[cfg(feature = "trail_saving")]
+use crate::assign::TrailSavingIF;
 
 use {
     super::State,
@@ -75,7 +77,6 @@ pub fn handle_conflict(
     asg.cancel_until(conflicting_level);
     asg.handle(SolverEvent::Conflict);
 
-    state.derive20.clear();
     let assign_level = conflict_analyze(asg, cdb, state, cc).max(asg.root_level());
     let new_learnt = &mut state.new_learnt;
     let learnt_len = new_learnt.len();
@@ -163,36 +164,40 @@ pub fn handle_conflict(
     // learnt clause quality based backtrack strategy switching
     // Idea: If the learned clause is low quality, don’t trust it to justify a large backjump; use CBT/limited-backjump instead.
     let bt_drift: Option<bool> = if cfg!(feature = "chrono_BT")
-    /* && 100_000 < asg.num_conflict */
-    {
-        if asg
+        && assign_level > 0
+        && asg
             .len_upto(conflicting_level)
             .saturating_sub(asg.len_upto(assign_level))
             >= 40
-        {
-            Some(true)
-        } else if new_learnt
+    {
+        Some(true)
+    } else if cfg!(feature = "BT_drift")
+        && assign_level > 0
+        && new_learnt
             .iter()
             .map(|l| asg.level(l.vi()))
             .collect::<HashSet<_>>()
             .len() as f64
             >= 2.5 * cdb.lbd.get().max(3.0)
-            && assign_level > 0
-        {
-            Some(false)
-        } else {
-            None
-        }
+    {
+        Some(false)
     } else {
         None
     };
     asg.cancel_until(match bt_drift {
         None => assign_level,
-        Some(false) => assign_level.saturating_sub(1),
+        Some(false) => assign_level - 1,
         Some(true) => conflicting_level - 1,
     });
     if bt_drift.is_some() {
-        state.num_chrono_bt += 1;
+        #[cfg(feature = "trail_saving")]
+        {
+            asg.clear_saved_trail();
+        }
+        #[cfg(feature = "chrono_BT")]
+        {
+            state.num_chrono_bt += 1;
+        }
     }
     // debug_assert_eq!(asg.assigned(l0), None);
     // debug_assert_eq!(
@@ -212,9 +217,7 @@ pub fn handle_conflict(
 
             if bt_drift.is_none() {
                 asg.assign_by_implication(l0, AssignReason::BinaryLink(!l1), assign_level);
-            }
-            for cid in &state.derive20 {
-                cdb[cid].turn_on(FlagClause::DERIVE20);
+                cdb[cid].used = cdb[cid].used.saturating_add(1);
             }
             rank = 1;
             #[cfg(feature = "bi_clause_completion")]
@@ -227,13 +230,9 @@ pub fn handle_conflict(
             debug_assert_eq!(cdb[cid].lit0(), l0);
             if bt_drift.is_none_or(|up1| up1 && cdb[cid].is_unit_under(&*asg)) {
                 asg.assign_by_implication(l0, AssignReason::Implication(cid), assign_level);
+                cdb[cid].used = cdb[cid].used.saturating_add(1);
             }
             rank = cdb[cid].rank;
-            if rank <= 20 {
-                for cid in &state.derive20 {
-                    cdb[cid].turn_on(FlagClause::DERIVE20);
-                }
-            }
         }
         RefClause::RegisteredClause(cid) => {
             debug_assert_eq!(learnt_len, 2);
@@ -255,6 +254,7 @@ pub fn handle_conflict(
             rank = 1;
             if bt_drift.is_none_or(|up1| up1 && cdb[cid].is_unit_under(&*asg)) {
                 asg.assign_by_implication(l0, AssignReason::BinaryLink(!l1), assign_level);
+                cdb[cid].used = cdb[cid].used.saturating_add(1);
             }
         }
         RefClause::Dead => unreachable!("handle_conflict::RefClause::Dead"),
@@ -266,7 +266,6 @@ pub fn handle_conflict(
     state
         .e_mode
         .update(conflicting_level as f64 - assign_level as f64);
-    state.derive20.clear();
     Ok(rank)
 }
 
@@ -422,7 +421,7 @@ fn conflict_analyze(
                 debug_assert!(!cdb[cid].is_dead() && 2 < cdb[cid].len());
                 // if !cdb.update_at_analysis(asg, cid) {
                 if !cdb[cid].is(FlagClause::LEARNT) {
-                    state.derive20.push(cid);
+                    cdb[cid].used = cdb[cid].used.saturating_add(1);
                 }
                 if max_lbd < cdb[cid].rank {
                     max_lbd = cdb[cid].rank;

src/state.rs

@@ -129,8 +129,6 @@ pub struct State {
     pub last_asg: usize,
     /// working place to build learnt clauses
     pub new_learnt: Vec<Lit>,
-    /// working place to store given clauses' ids which is used to derive a good learnt
-    pub derive20: Vec<ClauseId>,
     /// `progress` invocation counter
     pub progress_cnt: usize,
     /// keep the previous statistics values
@@ -171,7 +169,6 @@ impl Default for State {
 
             last_asg: 0,
             new_learnt: Vec::new(),
-            derive20: Vec::new(),
             progress_cnt: 0,
             record: ProgressRecord::default(),
             sls_index: 0,