From f023c0682f90fb944aa10f2b65a7cc03397f9604 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Wed, 17 Jun 2026 18:34:48 +0900
Subject: [PATCH 01/26] chore: open PR


From bc2eb6c8b728eb0adf85633ce109027d7d8d55df Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Wed, 17 Jun 2026 18:38:50 +0900
Subject: [PATCH 02/26] feat: add types/rng

---
 src/types/mod.rs |  6 +++-
 src/types/rng.rs | 87 ++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 92 insertions(+), 1 deletion(-)
 create mode 100644 src/types/rng.rs

diff --git a/src/types/mod.rs b/src/types/mod.rs
index 0b55adc61..f7b91bc43 100644
--- a/src/types/mod.rs
+++ b/src/types/mod.rs
@@ -15,12 +15,16 @@ pub mod idx;
 pub mod lit;
 /// methods on binary link, namely binary clause
 pub mod luby;
+/// a deterministic pseudo-random number generator
+pub mod rng;
 /// methods on f64 sort
 pub mod sort_key;
 /// methods on Var
 pub mod var;
 
-pub use self::{clause::*, cnf::*, ema::*, flags::*, idx::*, lit::*, luby::*, sort_key::*, var::*};
+pub use self::{
+    clause::*, cnf::*, ema::*, flags::*, idx::*, lit::*, luby::*, rng::*, sort_key::*, var::*,
+};
 
 pub use crate::{assign::AssignReason, config::Config, solver::SolverEvent};
 
diff --git a/src/types/rng.rs b/src/types/rng.rs
new file mode 100644
index 000000000..8a8b301f3
--- /dev/null
+++ b/src/types/rng.rs
@@ -0,0 +1,87 @@
+//! A deterministic, dependency-free pseudo-random number generator.
+//!
+//! The standard library does not provide a general-purpose RNG, so this is a
+//! small [SplitMix64](https://prng.di.unimi.it/splitmix64.c) generator. It is
+//! fully deterministic (the same seed always yields the same sequence), fast,
+//! and of high statistical quality, which makes it suitable for reproducible
+//! randomization inside the solver.
+
+/// A SplitMix64 pseudo-random number generator.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct SplitMix64 {
+    state: u64,
+}
+
+impl Default for SplitMix64 {
+    fn default() -> Self {
+        SplitMix64::new(0)
+    }
+}
+
+impl SplitMix64 {
+    /// Create a generator from a seed. Any seed (including `0`) is valid.
+    pub const fn new(seed: u64) -> Self {
+        SplitMix64 { state: seed }
+    }
+    /// Return the next 64-bit pseudo-random value and advance the state.
+    pub fn next_u64(&mut self) -> u64 {
+        self.state = self.state.wrapping_add(0x9E37_79B9_7F4A_7C15);
+        let mut z = self.state;
+        z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
+        z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB);
+        z ^ (z >> 31)
+    }
+    /// Return a pseudo-random `f64` in the half-open range `[0.0, 1.0)`.
+    pub fn next_f64(&mut self) -> f64 {
+        // Use the top 53 bits to fill the mantissa of an f64.
+        (self.next_u64() >> 11) as f64 / ((1u64 << 53) as f64)
+    }
+    /// Return a pseudo-random `usize` in the half-open range `[0, bound)`.
+    /// Returns `0` when `bound` is `0`.
+    pub fn below(&mut self, bound: usize) -> usize {
+        if bound == 0 {
+            0
+        } else {
+            (self.next_u64() % bound as u64) as usize
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_deterministic() {
+        let mut a = SplitMix64::new(12345);
+        let mut b = SplitMix64::new(12345);
+        for _ in 0..1000 {
+            assert_eq!(a.next_u64(), b.next_u64());
+        }
+    }
+
+    #[test]
+    fn test_distinct_seeds_diverge() {
+        let mut a = SplitMix64::new(1);
+        let mut b = SplitMix64::new(2);
+        assert_ne!(a.next_u64(), b.next_u64());
+    }
+
+    #[test]
+    fn test_next_f64_in_range() {
+        let mut r = SplitMix64::new(42);
+        for _ in 0..10_000 {
+            let x = r.next_f64();
+            assert!((0.0..1.0).contains(&x));
+        }
+    }
+
+    #[test]
+    fn test_below_bound() {
+        let mut r = SplitMix64::new(7);
+        for _ in 0..10_000 {
+            assert!(r.below(10) < 10);
+        }
+        assert_eq!(r.below(0), 0);
+    }
+}

From 922c3c13942f168b2a964703d6cfb734fd4b16bc Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Wed, 17 Jun 2026 22:49:48 +0900
Subject: [PATCH 03/26] feat(polarity): implement

---
 src/assign/propagate.rs |  7 +++++++
 src/assign/select.rs    |  5 +++++
 src/assign/stack.rs     |  5 +++++
 src/solver/search.rs    | 14 ++++++--------
 src/types/var.rs        |  6 ++++++
 5 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index deec2f027..918f3fbe7 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -250,6 +250,13 @@ impl PropagateIF for AssignStack {
                                 (v.last_conflict + i + self.num_propagation).is_multiple_of(2)
                             }
                             RephaseTarget::Inverted => !v.assign.unwrap(),
+                            RephaseTarget::Polarity => {
+                                if self.rng.next_f64() < v.polarity.abs().min(0.95) {
+                                    v.polarity > 0.0
+                                } else {
+                                    self.rng.next_f64() >= 0.5
+                                }
+                            }
                         },
                     );
                 } else {
diff --git a/src/assign/select.rs b/src/assign/select.rs
index 27befb9f8..df093e2a0 100644
--- a/src/assign/select.rs
+++ b/src/assign/select.rs
@@ -14,6 +14,7 @@ pub enum RephaseTarget {
     True,
     Random,
     Inverted,
+    Polarity,
 }
 
 impl RephaseTarget {
@@ -26,6 +27,7 @@ impl RephaseTarget {
             RephaseTarget::True => "⊤",
             RephaseTarget::Random => "∼",
             RephaseTarget::Inverted => "¬",
+            RephaseTarget::Polarity => "φ",
         }
     }
 }
@@ -110,9 +112,12 @@ impl VarSelectIF for AssignStack {
                 && v.level > self.root_level
             {
                 self.best_phases[vi] = (Some(b), v.level);
+                v.polarity *= 0.8;
+                v.polarity *= 0.2 * if b { 1.0 } else { -1.0 };
                 alives += 1;
             } else {
                 self.best_phases[vi] = (None, DecisionLevel::MAX);
+                v.polarity *= 0.8;
             }
         }
         self.num_vars - alives - self.num_asserted_vars - self.num_eliminated_vars
diff --git a/src/assign/stack.rs b/src/assign/stack.rs
index 8855e0db5..98472884e 100644
--- a/src/assign/stack.rs
+++ b/src/assign/stack.rs
@@ -89,6 +89,9 @@ pub struct AssignStack {
     pub(super) activity_stay_rate: f64,
     /// its diff
     pub(super) activity_learning_rate: f64,
+
+    //## Misc
+    pub(super) rng: SplitMix64,
 }
 
 impl Default for AssignStack {
@@ -133,6 +136,7 @@ impl Default for AssignStack {
 
             activity_scheme: VarActivityScheme::default(),
             activity_learning_rate: 0.06,
+            rng: SplitMix64::new(0),
         }
     }
 }
@@ -171,6 +175,7 @@ impl Instantiate for AssignStack {
             activity_stay_rate: 1.0 - config.vrw_learning_rate,
 
             activity_learning_rate: config.vrw_learning_rate,
+            rng: SplitMix64::new((cnf.num_of_variables + cnf.num_of_clauses) as u64),
 
             ..AssignStack::default()
         }
diff --git a/src/solver/search.rs b/src/solver/search.rs
index 0ef569efa..5ef186374 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -224,13 +224,9 @@ impl SolveIF for Solver {
 }
 
 /// table of (RephaseTarget, span length, next index)
-const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 6] = [
-    (RephaseTarget::False, 20, 1),
-    (RephaseTarget::Walk, 60, 2),
-    (RephaseTarget::True, 20, 3),
-    (RephaseTarget::Best, 80, 4),
-    (RephaseTarget::Inverted, 20, 5),
-    (RephaseTarget::Walk, 60, 0),
+const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 2] = [
+    (RephaseTarget::Walk, 80, 1),
+    (RephaseTarget::Polarity, 80, 0),
 ];
 
 /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT.
@@ -378,7 +374,9 @@ fn search(
             let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar);
             RESTART!(asg, cdb, state)?;
             if vivificatioen_pressure >= vivificatioen_interval {
-                if cfg!(feature = "clause_vivification") && current_phase.0 == RephaseTarget::Walk {
+                if cfg!(feature = "clause_vivification")
+                /* && current_phase.0 == RephaseTarget::Polarity */
+                {
                     reduce!();
                     cdb.vivify(asg, state)?;
                 }
diff --git a/src/types/var.rs b/src/types/var.rs
index fe79cd3bf..39b865abd 100644
--- a/src/types/var.rs
+++ b/src/types/var.rs
@@ -25,6 +25,11 @@ pub struct Var {
     pub(crate) reward: f64,
     /// the last conflict by this
     pub(crate) last_conflict: usize,
+    /// phase bias at the best assignments
+    /// -  1.0: `true` always
+    /// -  0.0: no bias
+    /// - -1.0: `false` always
+    pub(crate) polarity: f64,
 }
 
 impl Default for Var {
@@ -38,6 +43,7 @@ impl Default for Var {
             flags: FlagVar::empty(),
             reward: 0.0,
             last_conflict: 0,
+            polarity: 0.0,
         }
     }
 }

From a5cc3026893d7d25154272a853a05475f2aba715 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Thu, 18 Jun 2026 15:32:32 +0900
Subject: [PATCH 04/26] feit(vivify): add a mode to update reference_rate

---
 src/cdb/vivify.rs | 35 +++++++++++++++++++++++++----------
 1 file changed, 25 insertions(+), 10 deletions(-)

diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 4db521806..104f6bb41 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -8,18 +8,22 @@ use crate::{
 };
 
 pub trait VivifyIF {
-    fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent;
+    fn vivify(
+        &mut self,
+        asg: &mut AssignStack,
+        state: &mut State,
+        skip_evaluation: bool,
+    ) -> MaybeInconsistent;
 }
 
 impl VivifyIF for ClauseDB {
     /// vivify clauses under `asg`
-    fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent {
-        if asg.remains() {
-            asg.propagate_sandbox(self).map_err(|cc| {
-                state.log(None, "By vivifier");
-                SolverError::RootLevelConflict(cc)
-            })?;
-        }
+    fn vivify(
+        &mut self,
+        asg: &mut AssignStack,
+        state: &mut State,
+        skip_evaluation: bool,
+    ) -> MaybeInconsistent {
         // 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];
@@ -29,6 +33,12 @@ impl VivifyIF for ClauseDB {
         let mut num_assert = 0;
         let mut to_display = 0;
         state[Stat::Vivification] += 1;
+        if !skip_evaluation && asg.remains() {
+            asg.propagate_sandbox(self).map_err(|cc| {
+                state.log(None, "By vivifier");
+                SolverError::RootLevelConflict(cc)
+            })?;
+        }
         // Inlined target selection (formerly `select_targets`).
         // Pick clauses that haven't been vivified recently. We deliberately
         // do NOT sort the candidates: the per-clause filter in the loop below
@@ -39,7 +49,7 @@ impl VivifyIF for ClauseDB {
             if c.is_dead() {
                 continue;
             }
-            if c.referred_at + 20_000 * (1 + c.vivify_age) > asg.num_conflict || c.vivify_age >= 8 {
+            if c.referred_at + 20_000 * (1 + c.vivify_age) > asg.num_conflict {
                 continue;
             }
             let c = &mut self[cid];
@@ -49,7 +59,9 @@ impl VivifyIF for ClauseDB {
             // that are not too short and have a moderate LBD; outside this band
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
-            if c.len() < 9_usize.saturating_sub(c.vivify_age).max(3)
+            if skip_evaluation
+                || c.vivify_age >= 6
+                || c.len() < 9_usize.saturating_sub(c.vivify_age)
                 || 12 < asg.literal_block_distance_current(&c.lits)
             {
                 continue;
@@ -160,6 +172,9 @@ impl VivifyIF for ClauseDB {
                 }
             }
         }
+        if skip_evaluation {
+            return Ok(());
+        }
         asg.backtrack_sandbox();
         if asg.remains() {
             asg.propagate_sandbox(self)

From 1cd27583c41387171e3859d032e795c488f00379 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Thu, 18 Jun 2026 15:34:36 +0900
Subject: [PATCH 05/26] feat(select.rs): revise helper functions

---
 src/assign/select.rs | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/assign/select.rs b/src/assign/select.rs
index df093e2a0..2d9a2d759 100644
--- a/src/assign/select.rs
+++ b/src/assign/select.rs
@@ -61,7 +61,8 @@ pub trait VarSelectIF {
     fn rebuild_order(&mut self);
     /// save the current assignments as the best phases.
     /// return the core size.
-    fn save_best_phases(&mut self) -> usize;
+    fn save_best_phases(&mut self, new_best: bool) -> usize;
+    fn clear_best_phases(&mut self);
 }
 
 impl VarSelectIF for AssignStack {
@@ -105,23 +106,34 @@ impl VarSelectIF for AssignStack {
             }
         }
     }
-    fn save_best_phases(&mut self) -> usize {
+    fn save_best_phases(&mut self, new_best: bool) -> usize {
         let mut alives: usize = 0;
         for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
             if let Some(b) = v.assign
                 && v.level > self.root_level
+                && !v.is(FlagVar::ELIMINATED)
             {
-                self.best_phases[vi] = (Some(b), v.level);
-                v.polarity *= 0.8;
-                v.polarity *= 0.2 * if b { 1.0 } else { -1.0 };
+                if new_best {
+                    self.best_phases[vi] = (Some(b), v.level);
+                }
+                v.polarity *= 0.9;
+                v.polarity += 0.1 * if b { 1.0 } else { -1.0 };
                 alives += 1;
             } else {
-                self.best_phases[vi] = (None, DecisionLevel::MAX);
-                v.polarity *= 0.8;
+                if new_best {
+                    self.best_phases[vi] = (None, DecisionLevel::MAX);
+                }
             }
         }
         self.num_vars - alives - self.num_asserted_vars - self.num_eliminated_vars
     }
+    fn clear_best_phases(&mut self) {
+        for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
+            if v.level > self.root_level && !v.is(FlagVar::ELIMINATED) {
+                self.best_phases[vi] = (None, DecisionLevel::MAX);
+            }
+        }
+    }
 }
 
 impl AssignStack {

From 441140bfefca3939f4b347f1fee4366e259eb57b Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:00:43 +0900
Subject: [PATCH 06/26] chore(vivify): rename an arg

---
 src/cdb/vivify.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 104f6bb41..e4ab6f9d6 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -22,7 +22,7 @@ impl VivifyIF for ClauseDB {
         &mut self,
         asg: &mut AssignStack,
         state: &mut State,
-        skip_evaluation: bool,
+        eval: bool,
     ) -> MaybeInconsistent {
         // This is a reusable vector to reduce memory consumption,
         // the key is the number of invocation
@@ -33,7 +33,7 @@ impl VivifyIF for ClauseDB {
         let mut num_assert = 0;
         let mut to_display = 0;
         state[Stat::Vivification] += 1;
-        if !skip_evaluation && asg.remains() {
+        if eval && asg.remains() {
             asg.propagate_sandbox(self).map_err(|cc| {
                 state.log(None, "By vivifier");
                 SolverError::RootLevelConflict(cc)
@@ -59,7 +59,7 @@ impl VivifyIF for ClauseDB {
             // that are not too short and have a moderate LBD; outside this band
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
-            if skip_evaluation
+            if !eval
                 || c.vivify_age >= 6
                 || c.len() < 9_usize.saturating_sub(c.vivify_age)
                 || 12 < asg.literal_block_distance_current(&c.lits)
@@ -172,7 +172,7 @@ impl VivifyIF for ClauseDB {
                 }
             }
         }
-        if skip_evaluation {
+        if !eval {
             return Ok(());
         }
         asg.backtrack_sandbox();

From b8099af940ba99085b442b3e12cd09824f3b0990 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:02:40 +0900
Subject: [PATCH 07/26] feat(polarity): revise definition

---
 src/assign/propagate.rs | 9 ++++++---
 src/assign/select.rs    | 2 --
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 918f3fbe7..d08635271 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -237,6 +237,8 @@ impl PropagateIF for AssignStack {
                 if cfg!(feature = "rephase")
                 // && self.num_conflict - v.last_conflict <= 1000
                 {
+                    v.polarity *= 0.99;
+                    v.polarity += 0.01 * if v.assign.unwrap() { 1.0 } else { -1.0 };
                     v.set(
                         FlagVar::PHASE,
                         match self.phase_mode {
@@ -251,10 +253,11 @@ impl PropagateIF for AssignStack {
                             }
                             RephaseTarget::Inverted => !v.assign.unwrap(),
                             RephaseTarget::Polarity => {
-                                if self.rng.next_f64() < v.polarity.abs().min(0.95) {
-                                    v.polarity > 0.0
+                                if self.rng.next_f64() <= v.polarity.abs() * 0.9 {
+                                    v.assign.unwrap()
                                 } else {
-                                    self.rng.next_f64() >= 0.5
+                                    !v.assign.unwrap()
+                                    // self.rng.next_f64() >= 0.5
                                 }
                             }
                         },
diff --git a/src/assign/select.rs b/src/assign/select.rs
index 2d9a2d759..53c784d29 100644
--- a/src/assign/select.rs
+++ b/src/assign/select.rs
@@ -116,8 +116,6 @@ impl VarSelectIF for AssignStack {
                 if new_best {
                     self.best_phases[vi] = (Some(b), v.level);
                 }
-                v.polarity *= 0.9;
-                v.polarity += 0.1 * if b { 1.0 } else { -1.0 };
                 alives += 1;
             } else {
                 if new_best {

From 7811f329a9f8a6c95df46be71e9143df271b282f Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:03:47 +0900
Subject: [PATCH 08/26] chore(reduce): tiny changes

---
 src/cdb/db.rs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 3ae76c824..9a48bf0f4 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -878,7 +878,10 @@ impl ClauseDBIF for ClauseDB {
                     ntier2 += 1;
                     continue;
                 }
-                _ => {}
+                _ if c.reference_rate >= 16.0 => {
+                    continue;
+                }
+                _ => (),
             }
             if c.len() <= 3 {
                 ntier1 += 1;
@@ -887,7 +890,7 @@ impl ClauseDBIF for ClauseDB {
             if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) {
                 continue;
             }
-            if c.reference_rate >= 16.0 || c.referred_at >= last_restart {
+            if c.referred_at >= last_restart {
                 continue;
             }
             remove_clause_fn(

From 0f95717bdd91cdc692044a43d72770a2d66d7aab Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:05:18 +0900
Subject: [PATCH 09/26] feat(learning-rate): add `rescale_learning_rate`

---
 src/assign/learning_rate.rs | 4 ++++
 src/types/mod.rs            | 1 +
 2 files changed, 5 insertions(+)

diff --git a/src/assign/learning_rate.rs b/src/assign/learning_rate.rs
index 5bc781daa..da757ea85 100644
--- a/src/assign/learning_rate.rs
+++ b/src/assign/learning_rate.rs
@@ -58,6 +58,10 @@ impl ActivityIF<VarId> for AssignStack {
         self.activity_stay_rate = 1.0 - scaling;
         self.activity_learning_rate = scaling;
     }
+    fn rescale_learning_rate(&mut self, scaling: f64) {
+        self.activity_learning_rate *= scaling;
+        self.activity_stay_rate = 1.0 - self.activity_learning_rate;
+    }
     // Note: `update_rewards` should be called before `cancel_until`
     #[inline]
     fn update_activity_tick(&mut self) {
diff --git a/src/types/mod.rs b/src/types/mod.rs
index f7b91bc43..13a17ca93 100644
--- a/src/types/mod.rs
+++ b/src/types/mod.rs
@@ -62,6 +62,7 @@ pub trait ActivityIF<Ix> {
     fn set_learning_rate(&mut self, learning_rate: f64);
     /// update internal counter.
     fn update_activity_tick(&mut self);
+    fn rescale_learning_rate(&mut self, scaling: f64);
 }
 
 /// API for object instantiation based on `Configuration` and `CNFDescription`.

From 6df5adfd1d6dfae18dba49c1bdf5c89e9a6a32ef Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:07:37 +0900
Subject: [PATCH 10/26] exp(search): re-schedule rephasing, reduce, and vivify;
 dynamic rescaling learning rate

---
 src/solver/search.rs | 109 +++++++++++++++++++++++++++++--------------
 1 file changed, 75 insertions(+), 34 deletions(-)

diff --git a/src/solver/search.rs b/src/solver/search.rs
index 5ef186374..4d8e12aa8 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -76,7 +76,7 @@ impl SolveIF for Solver {
         #[cfg(feature = "clause_vivification")]
         {
             state.flush("vivifying...");
-            if cdb.vivify(asg, state).is_err() {
+            if cdb.vivify(asg, state, false).is_err() {
                 state.log(None, "By vivifier as a pre-possessor");
                 return Ok(Certificate::UNSAT);
             }
@@ -224,11 +224,26 @@ impl SolveIF for Solver {
 }
 
 /// table of (RephaseTarget, span length, next index)
-const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 2] = [
-    (RephaseTarget::Walk, 80, 1),
-    (RephaseTarget::Polarity, 80, 0),
+const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 8] = [
+    (RephaseTarget::True, 100, 1),
+    (RephaseTarget::False, 100, 2),
+    (RephaseTarget::Polarity, 4, 4),
+    (RephaseTarget::Polarity, 4, 4),
+    (RephaseTarget::Walk, 4, 2),
+    (RephaseTarget::Polarity, 4, 6),
+    (RephaseTarget::Best, 1, 0),
+    (RephaseTarget::Polarity, 4, 5),
+];
+const _REPHASE_ROTATION: [(RephaseTarget, usize, usize); 4] = [
+    // (RephaseTarget::False, 10, 1),
+    // (RephaseTarget::True, 10, 2),
+    (RephaseTarget::Walk, 40, 2),
+    (RephaseTarget::Polarity, 40, 2),
+    (RephaseTarget::Best, 10, 0),
+    (RephaseTarget::Walk, 80, 0),
+    // (RephaseTarget::Inverted, 20, 3),
+    // (RephaseTarget::Polarity, 10, 0),
 ];
-
 /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT.
 fn search(
     asg: &mut AssignStack,
@@ -236,26 +251,35 @@ fn search(
     state: &mut State,
 ) -> Result<bool, SolverError> {
     let mut span_len: usize = 1;
-    let mut vivificatioen_pressure: usize = 0;
-    let vivificatioen_interval: usize = 8_000;
     let mut elimination_pressure: usize = 0;
     let elimination_interval: usize = 80_000;
     let mut progress_pressure: usize = 0;
     let progress_interval: usize = 10_000;
     let mut reduction_pressure: usize = 0;
+    let reduction_interval: usize = 40_000;
     let mut rephase_rotation_pressure: usize = 0;
     let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0];
-    let vmtf_interval: usize = 20;
+    let vmtf_interval: usize = 10;
     let mut assign_peak: usize = 0;
     let luby_scale: usize = 64;
     let mut span_scale: usize = luby_scale;
 
     macro_rules! reduce {
-        () => {{
+        ($vivify: expr) => {{
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
-            cdb.reduce(asg, state.last_restart)
+            if cfg!(feature = "clause_vivification") {
+                cdb.vivify(asg, state, $vivify)?;
+            }
+            cdb.reduce(
+                asg,
+                if $vivify {
+                    state.last_restart
+                } else {
+                    asg.num_conflict.saturating_sub(reduction_interval)
+                },
+            );
         }};
     }
     macro_rules! to_lrb {
@@ -274,6 +298,7 @@ fn search(
         () => {
             if asg.activity_scheme != VarActivityScheme::VMTF {
                 asg.activity_scheme = VarActivityScheme::VMTF;
+                asg.phase_mode = RephaseTarget::Polarity;
                 // asg.phase_mode = RephaseTarget::Walk;
                 // asg.phase_mode = RephaseTarget::Best;
                 asg.set_learning_rate(0.0); // Don't change this
@@ -284,16 +309,19 @@ fn search(
     }
     macro_rules! rotate_rephase_mode {
         () => {
-            current_phase = &REPHASE_ROTATION[current_phase.2];
-            asg.phase_mode = current_phase.0;
-            rephase_rotation_pressure = 0;
-            // if current_phase.2 == 0 {
-            //     to_vmtf!();
-            // } else {
-            //     current_phase = &REPHASE_ROTATION[current_phase.2];
-            //     asg.phase_mode = current_phase.0;
-            //     rephase_rotation_pressure = 0;
-            // }
+            // current_phase = &REPHASE_ROTATION[current_phase.2];
+            // asg.phase_mode = current_phase.0;
+            // rephase_rotation_pressure = 0;
+            if current_phase.2 == 0 {
+                // asg.clear_best_phases();
+                // state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar);
+                // assign_peak = 0;
+                // to_vmtf!();
+            } else {
+                current_phase = &REPHASE_ROTATION[current_phase.2];
+                asg.phase_mode = current_phase.0;
+                rephase_rotation_pressure = 0;
+            }
         };
     }
     macro_rules! update_core {
@@ -302,6 +330,7 @@ fn search(
             if let Some(core) = asg.check_best_phases() {
                 assign_peak = assign_peak.saturating_sub(2 * $n);
                 state.core_size = core;
+                to_vmtf!();
             } else {
                 assign_peak = 0;
                 let pre = state.core_size;
@@ -347,25 +376,41 @@ fn search(
         match asg.stack_len().cmp(&assign_peak) {
             Ordering::Less => {}
             Ordering::Equal => {
-                // Do not update best_phases here to avoid an oscilation
+                // Do not update best_phases as new_best here to avoid an oscilation
+                state.core_size = asg.save_best_phases(false);
                 cdb.save_best_assign_reasons(asg, false);
             }
             Ordering::Greater => {
                 assign_peak = asg.stack_len();
-                state.core_size = asg.save_best_phases();
+                state.core_size = asg.save_best_phases(true);
                 cdb.save_best_assign_reasons(asg, false);
                 state.flush("");
                 state.flush(format!("core: {}", state.core_size));
+                // if state.core_size < 10 {
+                //     for (i, v) in asg.var_iter().enumerate().skip(1) {
+                //         if !v.is(FlagVar::ELIMINATED) && v.level > 0 {
+                //             println!(
+                //                 "{:>4}: {:>2}| {:>6.3}",
+                //                 i,
+                //                 match v.assign {
+                //                     None => 0,
+                //                     Some(false) => -1,
+                //                     Some(true) => 1,
+                //                 },
+                //                 v.polarity
+                //             );
+                //         }
+                //     }
+                // }
             }
         }
         elimination_pressure += 1;
-        vivificatioen_pressure += 1;
         progress_pressure += 1;
         reduction_pressure += 1;
         rephase_rotation_pressure += 1;
         span_len += 1;
-        if reduction_pressure >= 40_000 {
-            reduce!();
+        if reduction_pressure >= reduction_interval {
+            reduce!(false);
         }
         if state.span_manager.span_ended(span_len / span_scale) {
             span_len = 0;
@@ -373,14 +418,8 @@ fn search(
             dump_stage(asg, state, new_segment);
             let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar);
             RESTART!(asg, cdb, state)?;
-            if vivificatioen_pressure >= vivificatioen_interval {
-                if cfg!(feature = "clause_vivification")
-                /* && current_phase.0 == RephaseTarget::Polarity */
-                {
-                    reduce!();
-                    cdb.vivify(asg, state)?;
-                }
-                vivificatioen_pressure = 0;
+            if reduction_pressure >= reduction_interval {
+                reduce!(true);
             }
             if elimination_pressure >= elimination_interval {
                 if cfg!(feature = "clause_elimination") {
@@ -411,7 +450,7 @@ fn search(
                     _ => (),
                 }
             }
-            if new_segment == Some(true) {
+            if new_segment.is_some() {
                 span_scale = luby_scale * state.span_manager.envelop_index();
                 // Adapt LRB learning rate to the upcoming Luby envelope height:
                 // shorter spans → higher α (fast learning before the next restart),
@@ -419,6 +458,8 @@ fn search(
                 let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64;
                 let adaptive_lr: f64 = 1.0 / span.sqrt();
                 asg.set_learning_rate(adaptive_lr);
+            } else {
+                asg.rescale_learning_rate(0.9);
             }
         }
         if progress_pressure >= progress_interval {

From 8e2ae283e3b18d69d2a3903cdcc9ac8d252445c0 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:07:55 +0900
Subject: [PATCH 11/26] chore: update flake.lock

---
 flake.lock | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/flake.lock b/flake.lock
index 4e176efa1..bf0511ec2 100644
--- a/flake.lock
+++ b/flake.lock
@@ -181,11 +181,11 @@
     },
     "nixpkgs_11": {
       "locked": {
-        "lastModified": 1780002292,
-        "narHash": "sha256-O2k4sgDnoSSoZ5VgBfEwpso432pCpkLinkbTh7gswF4=",
+        "lastModified": 1781767213,
+        "narHash": "sha256-VeWB3PjXgFMU86hvpZXymfSAZv+T9+KgtEjaZGF1Ckk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "a840f3bfa7c71d222f07234bf357cb76c4cc6e57",
+        "rev": "746b8efb34046d34c265626788832b76b7699067",
         "type": "github"
       },
       "original": {
@@ -418,11 +418,11 @@
         "nixpkgs": "nixpkgs_12"
       },
       "locked": {
-        "lastModified": 1779920462,
-        "narHash": "sha256-c+h77EfDPZYplsRZKx2lJ+YtXg76iCQqiuOCgp5nfFs=",
+        "lastModified": 1781042363,
+        "narHash": "sha256-AwLy43zF8S1xUAWwOyuwPBOUSTEWOQ09y7yUPy2TjhA=",
         "owner": "shnarazk",
         "repo": "SAT-bench",
-        "rev": "c8b6217a2fe4472fb46531d94dd2e0cd37f4a519",
+        "rev": "8b750f2922dcc8228bd0fba23f4b0fb58f249599",
         "type": "github"
       },
       "original": {

From 2f4d2ab33902874a147a2f1a9ff78ef46ff8654a Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Fri, 19 Jun 2026 13:19:03 +0900
Subject: [PATCH 12/26] fix(vivify): cargo test

---
 src/solver/search.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/search.rs b/src/solver/search.rs
index 4d8e12aa8..2150a511c 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -76,7 +76,7 @@ impl SolveIF for Solver {
         #[cfg(feature = "clause_vivification")]
         {
             state.flush("vivifying...");
-            if cdb.vivify(asg, state, false).is_err() {
+            if cdb.vivify(asg, state, true).is_err() {
                 state.log(None, "By vivifier as a pre-possessor");
                 return Ok(Certificate::UNSAT);
             }

From dc3b901679011fa6613d50e3fa6a98baf50a3310 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 20 Jun 2026 13:38:53 +0900
Subject: [PATCH 13/26] feat(vivify): revise aging mechanism

---
 src/cdb/vivify.rs | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index e4ab6f9d6..e6b73b934 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -49,11 +49,15 @@ impl VivifyIF for ClauseDB {
             if c.is_dead() {
                 continue;
             }
-            if c.referred_at + 20_000 * (1 + c.vivify_age) > asg.num_conflict {
+            let span: f64 = 20_000.0 * (1.0 + c.vivify_age as f64);
+            if c.referred_at + span as usize > asg.num_conflict {
                 continue;
             }
             let c = &mut self[cid];
-            c.vivified();
+            c.update_reference_rate();
+            if eval {
+                c.vivify_age += 1;
+            }
             // Skip clauses that are unlikely to be improved by vivification.
             // Empirically success concentrates on clauses
             // that are not too short and have a moderate LBD; outside this band
@@ -66,6 +70,9 @@ impl VivifyIF for ClauseDB {
             {
                 continue;
             }
+            if !eval {
+                c.vivify_age += 1;
+            }
             let is_learnt = c.is(FlagClause::LEARNT);
             let vivify_age = c.vivify_age;
             let referred_at = c.referred_at;
@@ -307,8 +314,7 @@ impl AssignStack {
 
 impl Clause {
     /// clear flags about vivification
-    fn vivified(&mut self) {
-        self.vivify_age += 1;
+    fn update_reference_rate(&mut self) {
         self.reference_rate *= 0.8;
         self.reference_rate += 0.2 * self.referred as f64;
         self.referred = 0;

From a121a2ba7e7bdb2faeeb821181fa4b25ab275fd9 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 27 Jun 2026 14:05:07 +0900
Subject: [PATCH 14/26] Refine vivification and LBD tracking

- Add vivify_at and lbd fields to Clause; track LBD during conflict analysis
  and use vivify_at for timing vivification
- Extend ClauseDB with last_reduction_at and propagate it in reductions
- Gate vivification by LBD and preserve vivify_at across backtracks
- Introduce REFERRED flag and adapt reference-rate updates
- Simplify rephase rotation table and apply adaptive learning rate based on span
---
 src/assign/propagate.rs |   6 +--
 src/cdb/db.rs           | 111 ++++++++++++++++++++++++++++++----------
 src/cdb/vivify.rs       |  44 +++++-----------
 src/solver/conflict.rs  |   3 ++
 src/solver/search.rs    |  98 ++++++++++++++++-------------------
 src/types/clause.rs     |  19 +++++++
 src/types/flags.rs      |  14 ++---
 7 files changed, 175 insertions(+), 120 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index d08635271..3ef85be02 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -237,8 +237,8 @@ impl PropagateIF for AssignStack {
                 if cfg!(feature = "rephase")
                 // && self.num_conflict - v.last_conflict <= 1000
                 {
-                    v.polarity *= 0.99;
-                    v.polarity += 0.01 * if v.assign.unwrap() { 1.0 } else { -1.0 };
+                    v.polarity *= 0.999;
+                    v.polarity += 0.001 * if v.assign.unwrap() { 1.0 } else { -1.0 };
                     v.set(
                         FlagVar::PHASE,
                         match self.phase_mode {
@@ -253,7 +253,7 @@ impl PropagateIF for AssignStack {
                             }
                             RephaseTarget::Inverted => !v.assign.unwrap(),
                             RephaseTarget::Polarity => {
-                                if self.rng.next_f64() <= v.polarity.abs() * 0.9 {
+                                if self.rng.next_f64() <= v.polarity.abs().powf(1.1) {
                                     v.assign.unwrap()
                                 } else {
                                     !v.assign.unwrap()
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 9a48bf0f4..94bf8b484 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -1,3 +1,5 @@
+use crate::assign;
+
 use {
     super::{
         BinaryLinkDB, CertificationStore, ClauseDBIF, ClauseId, RefClause,
@@ -66,6 +68,7 @@ pub struct ClauseDB {
     pub(crate) tier1_clauses: Ema,
     /// the ratio of pretty good learnt clauses
     pub(crate) tier2_clauses: Ema,
+    pub(crate) last_reduction_at: usize,
 }
 
 impl Default for ClauseDB {
@@ -88,6 +91,7 @@ impl Default for ClauseDB {
             num_reregistration: 0,
             tier1_clauses: Ema::default(),
             tier2_clauses: Ema::default(),
+            last_reduction_at: 0,
         }
     }
 }
@@ -313,6 +317,7 @@ impl ClauseDBIF for ClauseDB {
             c.referred_at = 0;
             c.reference_rate = 1.0;
             c.vivify_age = 0;
+            c.vivify_at = 0;
         } else {
             cid = ClauseId::from(self.clause.len());
             let mut c = Clause {
@@ -841,11 +846,16 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         *num_lbd2 = 0;
+        let num_conflict = asg.derefer(assign::property::Tusize::NumConflict);
         let mut num_alives: usize = 0;
         // tier 1 group: the small clauses under the best assignment
         let mut ntier1: usize = 0;
         // tier 2 group: the small clauses under the best assignment
-        let mut ntier2: usize = 0;
+        let mut ntier2: usize = 10_000;
+        let mut cands: Vec<SortKey<usize>> = Vec::new();
+        let thr: f64 = 1.0;
+        let scale: f64 = 2.0;
+        let cutoff: DecisionLevel = 3;
         for (i, c) in clause
             .iter_mut()
             .enumerate()
@@ -853,46 +863,26 @@ impl ClauseDBIF for ClauseDB {
             .filter(|(_, c)| !c.is_dead())
         {
             num_alives += 1;
-            match asg.literal_block_distance_current(&c.lits) {
+            let _is_new = c.lbd == DecisionLevel::MAX;
+            let _referred = c.update_reference_rate(num_conflict);
+            match c.lbd {
                 0..=2 => {
                     *num_lbd2 += 1;
                     continue;
                 }
-                3 if c.reference_rate >= 0.01 => {
+                n @ (3..=5) if c.reference_rate >= scale.powf((n - cutoff) as f64) * thr => {
                     ntier1 += 1;
                     continue;
                 }
-                4 if c.reference_rate >= 0.1 => {
-                    ntier1 += 1;
-                    continue;
-                }
-                5 if c.reference_rate >= 2.0 => {
-                    ntier2 += 1;
-                    continue;
-                }
-                6 if c.reference_rate >= 4.0 => {
-                    ntier2 += 1;
-                    continue;
-                }
-                7 if c.reference_rate >= 8.0 => {
-                    ntier2 += 1;
+                _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => {
                     continue;
                 }
-                _ if c.reference_rate >= 16.0 => {
+                n @ (6..) if c.reference_rate >= scale.powf((n - cutoff) as f64) * thr => {
+                    cands.push(SortKey::new(i, c.len() as f64));
                     continue;
                 }
                 _ => (),
             }
-            if c.len() <= 3 {
-                ntier1 += 1;
-                continue;
-            }
-            if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) {
-                continue;
-            }
-            if c.referred_at >= last_restart {
-                continue;
-            }
             remove_clause_fn(
                 certification_store,
                 binary_link,
@@ -904,7 +894,72 @@ impl ClauseDBIF for ClauseDB {
                 c,
             );
             freelist.push(ClauseId::from(i));
+            /* match c.len() {
+                0..=5 => {
+                    *num_lbd2 += 1;
+                    continue;
+                }
+                6..=8 if c.reference_rate >= 0.0001 => {
+                    ntier1 += 1;
+                    continue;
+                }
+                9 | 10 if c.reference_rate >= 0.001 => {
+                    ntier2 += 1;
+                    continue;
+                }
+                11 | 12 if c.reference_rate >= 0.01 => {
+                    ntier2 += 1;
+                    continue;
+                }
+                _ if c.lbd <= 6 && c.reference_rate >= 1.0 => {
+                    continue;
+                }
+                _ if c.referred_at >= *last_reduction_at /* && referred */ => {
+                    continue;
+                }
+                _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => {
+                    continue;
+                }
+                _ => {
+                    remove_clause_fn(
+                        certification_store,
+                        binary_link,
+                        watch_cache,
+                        num_bi_clause,
+                        num_clause,
+                        num_learnt,
+                        ClauseId::from(i),
+                        c,
+                    );
+                    freelist.push(ClauseId::from(i));
+                }
+            }
+            */
+        }
+        if cands.len() > ntier2 {
+            cands.sort_unstable();
+            for cid in cands
+                .iter() // .skip(ntier1)
+                .skip(ntier2)
+            {
+                let c = &mut clause[cid.to()];
+                let cid = ClauseId::from(cid.to());
+                remove_clause_fn(
+                    certification_store,
+                    binary_link,
+                    watch_cache,
+                    num_bi_clause,
+                    num_clause,
+                    num_learnt,
+                    cid,
+                    c,
+                );
+                freelist.push(cid);
+            }
+        } else {
+            ntier2 = cands.len();
         }
+        self.last_reduction_at = num_conflict;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
     }
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index e6b73b934..345984a9f 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -22,7 +22,7 @@ impl VivifyIF for ClauseDB {
         &mut self,
         asg: &mut AssignStack,
         state: &mut State,
-        eval: bool,
+        _eval: bool,
     ) -> MaybeInconsistent {
         // This is a reusable vector to reduce memory consumption,
         // the key is the number of invocation
@@ -33,7 +33,7 @@ impl VivifyIF for ClauseDB {
         let mut num_assert = 0;
         let mut to_display = 0;
         state[Stat::Vivification] += 1;
-        if eval && asg.remains() {
+        if asg.remains() {
             asg.propagate_sandbox(self).map_err(|cc| {
                 state.log(None, "By vivifier");
                 SolverError::RootLevelConflict(cc)
@@ -49,32 +49,28 @@ impl VivifyIF for ClauseDB {
             if c.is_dead() {
                 continue;
             }
-            let span: f64 = 20_000.0 * (1.0 + c.vivify_age as f64);
-            if c.referred_at + span as usize > asg.num_conflict {
+            let span: usize = 4_000 * (c.vivify_age + 1);
+            if c.vivify_at + span > asg.num_conflict || c.vivify_age > 8 {
                 continue;
             }
             let c = &mut self[cid];
-            c.update_reference_rate();
-            if eval {
-                c.vivify_age += 1;
-            }
+            // c.update_reference_rate(asg.num_conflict);
             // Skip clauses that are unlikely to be improved by vivification.
             // Empirically success concentrates on clauses
             // that are not too short and have a moderate LBD; outside this band
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
-            if !eval
-                || c.vivify_age >= 6
-                || c.len() < 9_usize.saturating_sub(c.vivify_age)
-                || 12 < asg.literal_block_distance_current(&c.lits)
-            {
+            let lbd = asg.literal_block_distance_current(&c.lits);
+            if
+            // || !(lbd <= 6 && !c.is(FlagClause::REFERRED))
+            // || (c.vivify_age >= 8 && !c.is(FlagClause::REFERRED))
+            // || c.len() < 9_usize.saturating_sub(c.vivify_at)
+            6 < lbd {
                 continue;
             }
-            if !eval {
-                c.vivify_age += 1;
-            }
+            c.vivify_age += 1;
             let is_learnt = c.is(FlagClause::LEARNT);
-            let vivify_age = c.vivify_age;
+            let vivify_at = c.vivify_at;
             let referred_at = c.referred_at;
             let reference_rate = c.reference_rate;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
@@ -166,7 +162,7 @@ impl VivifyIF for ClauseDB {
                                     {
                                         self[cid].referred_at = referred_at;
                                         self[cid].reference_rate = reference_rate;
-                                        self[cid].vivify_age = vivify_age;
+                                        self[cid].vivify_at = vivify_at;
                                     }
                                     self.remove_clause(cid);
                                     num_shrink += 1;
@@ -179,9 +175,6 @@ impl VivifyIF for ClauseDB {
                 }
             }
         }
-        if !eval {
-            return Ok(());
-        }
         asg.backtrack_sandbox();
         if asg.remains() {
             asg.propagate_sandbox(self)
@@ -311,12 +304,3 @@ impl AssignStack {
         learnt
     }
 }
-
-impl Clause {
-    /// clear flags about vivification
-    fn update_reference_rate(&mut self) {
-        self.reference_rate *= 0.8;
-        self.reference_rate += 0.2 * self.referred as f64;
-        self.referred = 0;
-    }
-}
diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs
index c29a91ba1..e90fe9602 100644
--- a/src/solver/conflict.rs
+++ b/src/solver/conflict.rs
@@ -424,6 +424,9 @@ fn conflict_analyze(
                 }
                 cdb[cid].referred_at = asg.num_conflict;
                 cdb[cid].referred += 1;
+                cdb[cid].lbd = cdb[cid]
+                    .lbd
+                    .min(asg.literal_block_distance_current(&cdb[cid].lits));
             }
             AssignReason::Decision(_) | AssignReason::None => {}
         }
diff --git a/src/solver/search.rs b/src/solver/search.rs
index 2150a511c..4a0e3ac09 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -225,25 +225,16 @@ impl SolveIF for Solver {
 
 /// table of (RephaseTarget, span length, next index)
 const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 8] = [
-    (RephaseTarget::True, 100, 1),
-    (RephaseTarget::False, 100, 2),
-    (RephaseTarget::Polarity, 4, 4),
-    (RephaseTarget::Polarity, 4, 4),
-    (RephaseTarget::Walk, 4, 2),
-    (RephaseTarget::Polarity, 4, 6),
-    (RephaseTarget::Best, 1, 0),
-    (RephaseTarget::Polarity, 4, 5),
-];
-const _REPHASE_ROTATION: [(RephaseTarget, usize, usize); 4] = [
-    // (RephaseTarget::False, 10, 1),
-    // (RephaseTarget::True, 10, 2),
-    (RephaseTarget::Walk, 40, 2),
-    (RephaseTarget::Polarity, 40, 2),
-    (RephaseTarget::Best, 10, 0),
+    (RephaseTarget::Polarity, 80, 1),
+    (RephaseTarget::False, 20, 2),
+    (RephaseTarget::True, 20, 3),
+    (RephaseTarget::Best, 20, 4),
     (RephaseTarget::Walk, 80, 0),
-    // (RephaseTarget::Inverted, 20, 3),
-    // (RephaseTarget::Polarity, 10, 0),
+    (RephaseTarget::Walk, 0, 0),
+    (RephaseTarget::Polarity, 0, 0),
+    (RephaseTarget::Polarity, 0, 0),
 ];
+
 /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT.
 fn search(
     asg: &mut AssignStack,
@@ -259,34 +250,26 @@ fn search(
     let reduction_interval: usize = 40_000;
     let mut rephase_rotation_pressure: usize = 0;
     let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0];
-    let vmtf_interval: usize = 10;
+    let vmtf_interval: usize = 20;
     let mut assign_peak: usize = 0;
-    let luby_scale: usize = 64;
+    let luby_scale: usize = 256;
     let mut span_scale: usize = luby_scale;
 
     macro_rules! reduce {
-        ($vivify: expr) => {{
+        () => {{
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
-            if cfg!(feature = "clause_vivification") {
-                cdb.vivify(asg, state, $vivify)?;
-            }
-            cdb.reduce(
-                asg,
-                if $vivify {
-                    state.last_restart
-                } else {
-                    asg.num_conflict.saturating_sub(reduction_interval)
-                },
-            );
+            cdb.reduce(asg, state.last_restart);
         }};
     }
     macro_rules! to_lrb {
         () => {
             if asg.activity_scheme != VarActivityScheme::LRB {
                 asg.activity_scheme = VarActivityScheme::LRB;
-                asg.set_learning_rate(state.config.vrw_learning_rate);
+                let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64;
+                let adaptive_lr: f64 = 1.0 / span.sqrt();
+                asg.set_learning_rate(adaptive_lr);
                 asg.rebuild_order();
             }
             current_phase = &REPHASE_ROTATION[0];
@@ -298,9 +281,7 @@ fn search(
         () => {
             if asg.activity_scheme != VarActivityScheme::VMTF {
                 asg.activity_scheme = VarActivityScheme::VMTF;
-                asg.phase_mode = RephaseTarget::Polarity;
-                // asg.phase_mode = RephaseTarget::Walk;
-                // asg.phase_mode = RephaseTarget::Best;
+                asg.phase_mode = RephaseTarget::Walk;
                 asg.set_learning_rate(0.0); // Don't change this
                 asg.rebuild_order();
                 rephase_rotation_pressure = 0;
@@ -309,19 +290,22 @@ fn search(
     }
     macro_rules! rotate_rephase_mode {
         () => {
-            // current_phase = &REPHASE_ROTATION[current_phase.2];
-            // asg.phase_mode = current_phase.0;
-            // rephase_rotation_pressure = 0;
-            if current_phase.2 == 0 {
-                // asg.clear_best_phases();
-                // state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar);
-                // assign_peak = 0;
-                // to_vmtf!();
-            } else {
-                current_phase = &REPHASE_ROTATION[current_phase.2];
-                asg.phase_mode = current_phase.0;
-                rephase_rotation_pressure = 0;
-            }
+            current_phase = &REPHASE_ROTATION[current_phase.2];
+            asg.phase_mode = current_phase.0;
+            rephase_rotation_pressure = 0;
+            // if current_phase.2 == 0 {
+            //     current_phase = &REPHASE_ROTATION[current_phase.2];
+            //     asg.phase_mode = current_phase.0;
+            //     rephase_rotation_pressure = 0;
+            //     // asg.clear_best_phases();
+            //     // state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar);
+            //     // assign_peak = 0;
+            //     // to_vmtf!();
+            // } else {
+            //     current_phase = &REPHASE_ROTATION[current_phase.2];
+            //     asg.phase_mode = current_phase.0;
+            //     rephase_rotation_pressure = 0;
+            // }
         };
     }
     macro_rules! update_core {
@@ -372,6 +356,7 @@ fn search(
             update_core!(1);
         } else {
             cdb.lbd.update(lbd as f64);
+            cdb[cid].lbd = DecisionLevel::MAX;
         }
         match asg.stack_len().cmp(&assign_peak) {
             Ordering::Less => {}
@@ -409,8 +394,9 @@ fn search(
         reduction_pressure += 1;
         rephase_rotation_pressure += 1;
         span_len += 1;
-        if reduction_pressure >= reduction_interval {
-            reduce!(false);
+        // Don't check with `>= 1 * reduction_interval`. It prevents `reduce!(true)`.
+        if reduction_pressure > reduction_interval {
+            reduce!();
         }
         if state.span_manager.span_ended(span_len / span_scale) {
             span_len = 0;
@@ -418,10 +404,16 @@ fn search(
             dump_stage(asg, state, new_segment);
             let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar);
             RESTART!(asg, cdb, state)?;
-            if reduction_pressure >= reduction_interval {
-                reduce!(true);
-            }
+            // if reduction_pressure > reduction_interval {
+            //   reduce!();
+            // }
+            // if reduction_pressure >= reduction_interval {
+            //     reduce!();
+            // }
             if elimination_pressure >= elimination_interval {
+                if cfg!(feature = "clause_vivification") {
+                    cdb.vivify(asg, state, true)?;
+                }
                 if cfg!(feature = "clause_elimination") {
                     let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
                     state.flush("clause subsumption, ");
diff --git a/src/types/clause.rs b/src/types/clause.rs
index bc8fe5d63..ab0e8a241 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -23,8 +23,10 @@ pub struct Clause {
     pub(crate) reference_rate: f64,
     /// last vivified time in conflicts
     pub(crate) vivify_age: usize,
+    pub(crate) vivify_at: usize,
     /// The number of referrences in conflict analysis
     pub(crate) referred: usize,
+    pub(crate) lbd: DecisionLevel,
 }
 
 /// API for Clause, providing literal accessors.
@@ -47,6 +49,8 @@ pub trait ClauseIF {
     fn len(&self) -> usize;
     /// return true is this is a unit clause under `asg`.
     fn is_unit_under(&self, asg: &impl AssignIF) -> bool;
+    /// update reference_rate and return `true` if referred.
+    fn update_reference_rate(&mut self, base: usize) -> bool;
 }
 
 impl Default for Clause {
@@ -58,7 +62,9 @@ impl Default for Clause {
             referred_at: 0,
             reference_rate: 1.0,
             vivify_age: 0,
+            vivify_at: 0,
             referred: 0,
+            lbd: DecisionLevel::MAX,
         }
     }
 }
@@ -215,6 +221,19 @@ impl ClauseIF for Clause {
             .all(|l| asg.assigned(*l) == Some(false));
         unassigned == 1 && all_others_false
     }
+    fn update_reference_rate(&mut self, base: usize) -> bool {
+        let span: usize = 10_000; //  * (1.0 + self.vivify_age as f64).powf(1.0);
+        if self.referred_at + span <= base {
+            let referred = self.referred >= 1;
+            self.reference_rate *= 0.9;
+            self.reference_rate += 0.1 * self.referred as f64;
+            // self.set(FlagClause::REFERRED, referred);
+            self.referred = 0;
+            referred
+        } else {
+            true
+        }
+    }
 }
 
 impl FlagIF for Clause {
diff --git a/src/types/flags.rs b/src/types/flags.rs
index 816675d88..b7e8c2ef2 100644
--- a/src/types/flags.rs
+++ b/src/types/flags.rs
@@ -27,6 +27,8 @@ bitflags! {
         const ASSIGN_REASON   = 0b0000_1000;
         /// used in the best assignments
         const BEST_PROPAGATOR = 0b0010_0000;
+        /// a var is checked during in the current conflict analysis.
+        const REFERRED        = 0b0010_0000;
     }
 }
 
@@ -35,18 +37,18 @@ bitflags! {
     #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
     pub struct FlagVar: u8 {
         /// * the previous assigned value of a Var.
-        const PHASE        = 0b0000_0001;
+        const PHASE      = 0b0000_0001;
         /// used in conflict analyze
-        const USED         = 0b0000_0010;
+        const USED       = 0b0000_0010;
         /// a var is eliminated and managed by eliminator.
-        const ELIMINATED   = 0b0000_0100;
+        const ELIMINATED = 0b0000_0100;
         /// a clause or var is enqueued for eliminator.
-        const ENQUEUED     = 0b0000_1000;
+        const ENQUEUED   = 0b0000_1000;
         /// a var is checked during in the current conflict analysis.
-        const CA_SEEN      = 0b0001_0000;
+        const CA_SEEN    = 0b0001_0000;
 
         #[cfg(feature = "trace_propagation")]
         /// check propagation
-        const PROPAGATED   = 0b0010_0000;
+        const PROPAGATED = 0b0010_0000;
     }
 }

From 709093fca0f8d0c748fb3ebcd6543d6a2c690f06 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 27 Jun 2026 15:48:57 +0900
Subject: [PATCH 15/26] chore: clean up

---
 src/cdb/db.rs        | 27 +++++++++++++--------------
 src/cdb/mod.rs       |  2 +-
 src/cdb/vivify.rs    |  6 +-----
 src/solver/search.rs | 16 ++++++++--------
 src/types/clause.rs  |  9 +++++----
 src/types/flags.rs   |  6 ++----
 6 files changed, 30 insertions(+), 36 deletions(-)

diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 94bf8b484..2911f9c0c 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -831,7 +831,7 @@ impl ClauseDBIF for ClauseDB {
         c.is(FlagClause::LEARNT)
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    fn reduce(&mut self, asg: &mut impl AssignIF, last_restart: usize) {
+    fn reduce(&mut self, asg: &mut impl AssignIF) {
         self.num_reduction += 1;
         let ClauseDB {
             clause,
@@ -863,8 +863,7 @@ impl ClauseDBIF for ClauseDB {
             .filter(|(_, c)| !c.is_dead())
         {
             num_alives += 1;
-            let _is_new = c.lbd == DecisionLevel::MAX;
-            let _referred = c.update_reference_rate(num_conflict);
+            c.update_reference_rate(num_conflict);
             match c.lbd {
                 0..=2 => {
                     *num_lbd2 += 1;
@@ -963,17 +962,17 @@ impl ClauseDBIF for ClauseDB {
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
     }
-    fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool) {
-        if clear {
-            for c in self.clause.iter_mut().skip(1) {
-                c.turn_off(FlagClause::BEST_PROPAGATOR);
-            }
-        }
-        for l in asg.stack_iter() {
-            if let AssignReason::Implication(cid) = asg.reason(l.vi()) {
-                self[cid].turn_on(FlagClause::BEST_PROPAGATOR);
-            }
-        }
+    fn save_best_assign_reasons(&mut self, _asg: &impl AssignIF, _clear: bool) {
+        // if clear {
+        //     for c in self.clause.iter_mut().skip(1) {
+        //         c.turn_off(FlagClause::BEST_PROPAGATOR);
+        //     }
+        // }
+        // for l in asg.stack_iter() {
+        //     if let AssignReason::Implication(cid) = asg.reason(l.vi()) {
+        //         self[cid].turn_on(FlagClause::BEST_PROPAGATOR);
+        //     }
+        // }
     }
     fn certificate_add_assertion(&mut self, lit: Lit) {
         self.certification_store.add_clause(&[lit]);
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 4cd850450..399ee624a 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -103,7 +103,7 @@ pub trait ClauseDBIF:
     /// reduce learnt clauses
     /// # CAVEAT
     /// *precondition*: decision level == 0.
-    fn reduce(&mut self, asg: &mut impl AssignIF, last_restart: usize);
+    fn reduce(&mut self, asg: &mut impl AssignIF);
     /// turn `FlagClause::BEST_PROPAGATOR` of 'used clauses' on
     fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool);
     /// update flags.
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 345984a9f..2883bf838 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -61,11 +61,7 @@ impl VivifyIF for ClauseDB {
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
             let lbd = asg.literal_block_distance_current(&c.lits);
-            if
-            // || !(lbd <= 6 && !c.is(FlagClause::REFERRED))
-            // || (c.vivify_age >= 8 && !c.is(FlagClause::REFERRED))
-            // || c.len() < 9_usize.saturating_sub(c.vivify_at)
-            6 < lbd {
+            if 6 < lbd {
                 continue;
             }
             c.vivify_age += 1;
diff --git a/src/solver/search.rs b/src/solver/search.rs
index 4a0e3ac09..fc5e56b57 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -249,6 +249,8 @@ fn search(
     let mut reduction_pressure: usize = 0;
     let reduction_interval: usize = 40_000;
     let mut rephase_rotation_pressure: usize = 0;
+    let mut vivification_pressure: usize = 0;
+    let vivification_interval: usize = 80_000;
     let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0];
     let vmtf_interval: usize = 20;
     let mut assign_peak: usize = 0;
@@ -260,7 +262,7 @@ fn search(
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
-            cdb.reduce(asg, state.last_restart);
+            cdb.reduce(asg);
         }};
     }
     macro_rules! to_lrb {
@@ -393,6 +395,7 @@ fn search(
         progress_pressure += 1;
         reduction_pressure += 1;
         rephase_rotation_pressure += 1;
+        vivification_pressure += 1;
         span_len += 1;
         // Don't check with `>= 1 * reduction_interval`. It prevents `reduce!(true)`.
         if reduction_pressure > reduction_interval {
@@ -404,16 +407,13 @@ fn search(
             dump_stage(asg, state, new_segment);
             let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar);
             RESTART!(asg, cdb, state)?;
-            // if reduction_pressure > reduction_interval {
-            //   reduce!();
-            // }
-            // if reduction_pressure >= reduction_interval {
-            //     reduce!();
-            // }
-            if elimination_pressure >= elimination_interval {
+            if vivification_pressure >= vivification_interval {
                 if cfg!(feature = "clause_vivification") {
                     cdb.vivify(asg, state, true)?;
                 }
+                vivification_pressure = 0;
+            }
+            if elimination_pressure >= elimination_interval {
                 if cfg!(feature = "clause_elimination") {
                     let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
                     state.flush("clause subsumption, ");
diff --git a/src/types/clause.rs b/src/types/clause.rs
index ab0e8a241..868b743c1 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -17,15 +17,17 @@ pub struct Clause {
     /// the index from which `propagate` starts searching an un-falsified literal.
     /// Since it's just a hint, we don't need u32 or usize.
     pub search_from: u16,
+    /// The number of referrences in conflict analysis
+    pub(crate) referred: usize,
     /// Sum of activated (used as propagated) duration
     pub(crate) referred_at: usize,
     /// The average number of references in a vivification interval
     pub(crate) reference_rate: f64,
     /// last vivified time in conflicts
     pub(crate) vivify_age: usize,
+    // last vivified time in conflict
     pub(crate) vivify_at: usize,
-    /// The number of referrences in conflict analysis
-    pub(crate) referred: usize,
+    /// the minimal lbd of this clause so far
     pub(crate) lbd: DecisionLevel,
 }
 
@@ -59,11 +61,11 @@ impl Default for Clause {
             lits: vec![],
             flags: FlagClause::empty(),
             search_from: 2,
+            referred: 0,
             referred_at: 0,
             reference_rate: 1.0,
             vivify_age: 0,
             vivify_at: 0,
-            referred: 0,
             lbd: DecisionLevel::MAX,
         }
     }
@@ -227,7 +229,6 @@ impl ClauseIF for Clause {
             let referred = self.referred >= 1;
             self.reference_rate *= 0.9;
             self.reference_rate += 0.1 * self.referred as f64;
-            // self.set(FlagClause::REFERRED, referred);
             self.referred = 0;
             referred
         } else {
diff --git a/src/types/flags.rs b/src/types/flags.rs
index b7e8c2ef2..dffb36a45 100644
--- a/src/types/flags.rs
+++ b/src/types/flags.rs
@@ -25,10 +25,8 @@ bitflags! {
         const OCCUR_LINKED    = 0b0000_0100;
         /// a clause is registered in vars' assing list.
         const ASSIGN_REASON   = 0b0000_1000;
-        /// used in the best assignments
-        const BEST_PROPAGATOR = 0b0010_0000;
-        /// a var is checked during in the current conflict analysis.
-        const REFERRED        = 0b0010_0000;
+        // /// used in the best assignments
+        // const BEST_PROPAGATOR = 0b0010_0000;
     }
 }
 

From 8e4083358abb5615c5dccb5adff0b824b6980f41 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 28 Jun 2026 12:11:23 +0900
Subject: [PATCH 16/26] chore: clean up

---
 README.md            | 92 ++++++++++++++++++++++----------------------
 src/cdb/vivify.rs    |  6 +--
 src/solver/search.rs |  5 +--
 3 files changed, 50 insertions(+), 53 deletions(-)

diff --git a/README.md b/README.md
index fbfc31d16..9f036c748 100644
--- a/README.md
+++ b/README.md
@@ -22,52 +22,52 @@ Though Splr comes with **ABSOLUTELY NO WARRANTY**, I'd like to show some results
 
 #### Version 0.19.0
 
-- (0.19.0-rc7) @ 2026-06-16T17:15:17
-
-| # | target CNF solved by splr                            |time (s)|ret|val|
-|--:|:-----------------------------------------------------|-------:|:-:|---|
-|  1|`04648cef5bed430ab6429991fa9e107d-ramsey_3_6_19.norma`|        |124|   |
-|  2|`0c0430a68f147be18ab3fded07f30fdb-oddball_53_5_tto_zp`|   36.19| 10|   |
-|  3|`0ccb0f855352783a972be45188bf3164-SCPC-500-12.cnf`    |  117.39| 20|   |
-|  4|`0e1d562093d5f4fc9013cf4a14a03f70-Break_12_50.xml.cnf`|    6.58| 10|   |
-|  5|`110f8eb8b9b80204fe955ea0973bbb00-clqcl_30_7_6.normal`|        |124|   |
-|  6|`24bde22f729a988fb2394b644cb60d39-SC25_Timetable_C_48`|   28.10| 10|   |
-|  7|`2d0c041c0fe72dc32527bfbf34f63e61-170223547.cnf`      |        |124|   |
-|  8|`35b9091b90bd28a492c9556d6fc4348d-bp4_TCO_CSO_ZR.norm`|        |124|   |
-|  9|`35ec95b9b2398fb522db178855016ae0-MVRoundRobin_n14_d1`|        |124|   |
-| 10|`46a8727e27d848faafd83a990c2e01a7-case8.normalised.cn`|        |124|   |
-| 11|`482295be38dc1d63a16f3cf649ef7ef6-myciel6-cn.used-as.`|        |124|   |
-| 12|`53c21f3e78f060883026b5a12ba691d8-maximum_constrained`|   14.32| 10|   |
-| 13|`57b478982ee9aba245ba792452b18fe3-VanDerWaerden_pd_2-`| 1559.81| 10|   |
-| 14|`6147e666b75f603a4c4490d21ab654cd-hid-uns-enc-6-1-0-0`|  432.30| 20|   |
-| 15|`65f7145996bbec02b90bd0fa64a20502-test_v7_r12_vr10_c1`|        |124|   |
-| 16|`68e33d998466bbdd4bfb7249a5790e4f-arles_thres10_p10_r`|    0.68| 20|   |
-| 17|`83aa254f7d17e1df7bee19322ac4752b-1.normalised.cnf`   |        |124|   |
-| 18|`8e62c5d47920ffe36052f86177403e70-SC25_Timetable_C_39`|   13.60| 10|   |
-| 19|`908433870bee8ba2c86f266d0b002fdb-MVRoundRobin_n20_d1`|        |124|   |
-| 20|`918d9e7c2e197312517736421d728958-SCPC-500-1.cnf`     |  235.12| 20|   |
-| 21|`91c429adc2dc8430461b6d87a9aef335-16_16_booth_wallace`|        |124|   |
-| 22|`967b58fea99a99b8da592d3e2fe7139b-dubois50.cnf.mis-99`|        |124|   |
-| 23|`98a9352230efc411c092f1dcdcdedcfc-bp4_BC012_IXA_LPI_F`|        |124|   |
-| 24|`9b5f767eb5c14eb888d51acf70e045c8-uniqinv40prop.cnf`  |        |124|   |
-| 25|`a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r`|    0.68| 20|   |
-| 26|`a1fdd60d2570f47fb14956ac9e96951f-oddball_22_5_ttf.no`|   32.42| 20|   |
-| 27|`a70883771fd1c210d94a916d52510a3a-gm28sparrc.cnf`     |   17.62| 20|   |
-| 28|`b3d3680b3287a989ce61a6db1054efd2-case20.normalised.c`|    5.46| 10|   |
-| 29|`b9ed6fd14f4fc969ec966a4b54c36872-n320p5q2_n.apx_16.c`|   19.50| 10|   |
-| 30|`c21096fa2f550785c33dc862d83bc941-case17.normalised.c`|   52.47| 10|   |
-| 31|`cb950b9accfb53eb98f77b0f995ac0ae-rphp5_050_shuffled.`|        |124|   |
-| 32|`d5928883c1e1f70764a31a83aa419eaf-oski15a01b42s_opt.c`| 1824.52| 20|   |
-| 33|`d8666a18cf3a32af0a606099f0070b4b-7.normalised.cnf`   |        |124|   |
-| 34|`ddf9620410e6a4351f64c745670ef5d4-oddball_57_5_tto_zp`|   62.92| 10|   |
-| 35|`e23edb67db2d1dfdbfe2f4c02d09c6c7-14.normalised.cnf`  |  495.46| 10|   |
-| 36|`e430acf720b63044e5c825a00a76b0eb-rphp_p25_r25.cnf`   |        |124|   |
-| 37|`e442248e155eb81a811edd1deca8a2cd-sudoku-N30-23.cnf`  |        |124|   |
-| 38|`f17dfbed8c18716a41b231702e127524-SC25_Timetable_C_40`|   12.37| 10|   |
-| 39|`f25a1df88f89c6bcbe2602fa7f6e816b-1-TC-256-K-63.sanit`| 2607.61| 10|   |
-| 40|`f33a6163305d6559043b7438a692dea9-simon-r17-1.sanitiz`|        |124|   |
-
-"splr"    , med:     32.42, max:   2607.61,total except 19 timeouts: 7575.10
+- (0.19.0-rc7) @ 2026-06-28T00:12:52
+
+| # | target CNF solved by splr                            |time (s)|ret|
+|--:|:-----------------------------------------------------|-------:|:-:|
+|  1|`04648cef5bed430ab6429991fa9e107d-ramsey_3_6_19.norma`|        |124|
+|  2|`0c0430a68f147be18ab3fded07f30fdb-oddball_53_5_tto_zp`|  929.05| 10|
+|  3|`0ccb0f855352783a972be45188bf3164-SCPC-500-12.cnf`    |  139.97| 20|
+|  4|`0e1d562093d5f4fc9013cf4a14a03f70-Break_12_50.xml.cnf`|   42.03| 10|
+|  5|`110f8eb8b9b80204fe955ea0973bbb00-clqcl_30_7_6.normal`|        |124|
+|  6|`24bde22f729a988fb2394b644cb60d39-SC25_Timetable_C_48`|  114.26| 10|
+|  7|`2d0c041c0fe72dc32527bfbf34f63e61-170223547.cnf`      |        |124|
+|  8|`35b9091b90bd28a492c9556d6fc4348d-bp4_TCO_CSO_ZR.norm`|        |124|
+|  9|`35ec95b9b2398fb522db178855016ae0-MVRoundRobin_n14_d1`|        |124|
+| 10|`46a8727e27d848faafd83a990c2e01a7-case8.normalised.cn`|        |124|
+| 11|`482295be38dc1d63a16f3cf649ef7ef6-myciel6-cn.used-as.`|        |124|
+| 12|`53c21f3e78f060883026b5a12ba691d8-maximum_constrained`|   42.53| 10|
+| 13|`57b478982ee9aba245ba792452b18fe3-VanDerWaerden_pd_2-`| 2360.11| 10|
+| 14|`6147e666b75f603a4c4490d21ab654cd-hid-uns-enc-6-1-0-0`|  830.97| 20|
+| 15|`65f7145996bbec02b90bd0fa64a20502-test_v7_r12_vr10_c1`|        |124|
+| 16|`68e33d998466bbdd4bfb7249a5790e4f-arles_thres10_p10_r`|    2.99| 20|
+| 17|`83aa254f7d17e1df7bee19322ac4752b-1.normalised.cnf`   |        |124|
+| 18|`8e62c5d47920ffe36052f86177403e70-SC25_Timetable_C_39`|   38.42| 10|
+| 19|`908433870bee8ba2c86f266d0b002fdb-MVRoundRobin_n20_d1`|        |124|
+| 20|`918d9e7c2e197312517736421d728958-SCPC-500-1.cnf`     |  172.92| 20|
+| 21|`91c429adc2dc8430461b6d87a9aef335-16_16_booth_wallace`|        |124|
+| 22|`967b58fea99a99b8da592d3e2fe7139b-dubois50.cnf.mis-99`|        |124|
+| 23|`98a9352230efc411c092f1dcdcdedcfc-bp4_BC012_IXA_LPI_F`|        |124|
+| 24|`9b5f767eb5c14eb888d51acf70e045c8-uniqinv40prop.cnf`  |        |124|
+| 25|`a0bcdaffb0ea36b678899fd86bdc7f18-arles_thres10_p10_r`|    2.96| 20|
+| 26|`a1fdd60d2570f47fb14956ac9e96951f-oddball_22_5_ttf.no`|   38.66| 20|
+| 27|`a70883771fd1c210d94a916d52510a3a-gm28sparrc.cnf`     |    4.75| 20|
+| 28|`b3d3680b3287a989ce61a6db1054efd2-case20.normalised.c`|  378.93| 10|
+| 29|`b9ed6fd14f4fc969ec966a4b54c36872-n320p5q2_n.apx_16.c`|   29.64| 10|
+| 30|`c21096fa2f550785c33dc862d83bc941-case17.normalised.c`|  794.55| 10|
+| 31|`cb950b9accfb53eb98f77b0f995ac0ae-rphp5_050_shuffled.`|        |124|
+| 32|`d5928883c1e1f70764a31a83aa419eaf-oski15a01b42s_opt.c`|        |124|
+| 33|`d8666a18cf3a32af0a606099f0070b4b-7.normalised.cnf`   |        |124|
+| 34|`ddf9620410e6a4351f64c745670ef5d4-oddball_57_5_tto_zp`| 1148.32| 10|
+| 35|`e23edb67db2d1dfdbfe2f4c02d09c6c7-14.normalised.cnf`  |  619.00| 10|
+| 36|`e430acf720b63044e5c825a00a76b0eb-rphp_p25_r25.cnf`   |        |124|
+| 37|`e442248e155eb81a811edd1deca8a2cd-sudoku-N30-23.cnf`  |        |124|
+| 38|`f17dfbed8c18716a41b231702e127524-SC25_Timetable_C_40`| 1266.08| 10|
+| 39|`f25a1df88f89c6bcbe2602fa7f6e816b-1-TC-256-K-63.sanit`|  773.27| 10|
+| 40|`f33a6163305d6559043b7438a692dea9-simon-r17-1.sanitiz`|  117.68| 10|
+
+- "splr"    , med:    139.97, max:   2360.11,total except 19 timeouts: 9847.07
 
 #### Version 0.17.0
 
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 2883bf838..102f0da6a 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -50,7 +50,7 @@ impl VivifyIF for ClauseDB {
                 continue;
             }
             let span: usize = 4_000 * (c.vivify_age + 1);
-            if c.vivify_at + span > asg.num_conflict || c.vivify_age > 8 {
+            if c.vivify_at.max(c.referred_at) + span > asg.num_conflict {
                 continue;
             }
             let c = &mut self[cid];
@@ -60,11 +60,11 @@ impl VivifyIF for ClauseDB {
             // that are not too short and have a moderate LBD; outside this band
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
-            let lbd = asg.literal_block_distance_current(&c.lits);
-            if 6 < lbd {
+            if 6 < c.lbd {
                 continue;
             }
             c.vivify_age += 1;
+            c.vivify_at = asg.num_conflict;
             let is_learnt = c.is(FlagClause::LEARNT);
             let vivify_at = c.vivify_at;
             let referred_at = c.referred_at;
diff --git a/src/solver/search.rs b/src/solver/search.rs
index fc5e56b57..aa0d6fda9 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -224,15 +224,12 @@ impl SolveIF for Solver {
 }
 
 /// table of (RephaseTarget, span length, next index)
-const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 8] = [
+const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 5] = [
     (RephaseTarget::Polarity, 80, 1),
     (RephaseTarget::False, 20, 2),
     (RephaseTarget::True, 20, 3),
     (RephaseTarget::Best, 20, 4),
     (RephaseTarget::Walk, 80, 0),
-    (RephaseTarget::Walk, 0, 0),
-    (RephaseTarget::Polarity, 0, 0),
-    (RephaseTarget::Polarity, 0, 0),
 ];
 
 /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT.

From d9b044a437ab694291d1dc31a1494d64a12017d5 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 28 Jun 2026 12:18:26 +0900
Subject: [PATCH 17/26] feat(SplitMix64): add `next_bool`

---
 src/types/rng.rs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/types/rng.rs b/src/types/rng.rs
index 8a8b301f3..b0f2e5870 100644
--- a/src/types/rng.rs
+++ b/src/types/rng.rs
@@ -36,6 +36,10 @@ impl SplitMix64 {
         // Use the top 53 bits to fill the mantissa of an f64.
         (self.next_u64() >> 11) as f64 / ((1u64 << 53) as f64)
     }
+    /// Return a pseudo-random `bool`.
+    pub fn next_bool(&mut self) -> bool {
+        self.next_u64().is_multiple_of(2)
+    }
     /// Return a pseudo-random `usize` in the half-open range `[0, bound)`.
     /// Returns `0` when `bound` is `0`.
     pub fn below(&mut self, bound: usize) -> usize {

From b77015163da5524494e5f13ff988ef4f9a118b71 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sun, 28 Jun 2026 13:21:17 +0900
Subject: [PATCH 18/26] chore(cancel_until): use `rng::next_bool` for
 `RephaseTarget::Random`

---
 src/assign/propagate.rs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 3ef85be02..6ed720a6d 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -248,9 +248,7 @@ impl PropagateIF for AssignStack {
                             RephaseTarget::Best => {
                                 self.best_phases[vi].0.unwrap_or(v.assign.unwrap())
                             }
-                            RephaseTarget::Random => {
-                                (v.last_conflict + i + self.num_propagation).is_multiple_of(2)
-                            }
+                            RephaseTarget::Random => self.rng.next_bool(),
                             RephaseTarget::Inverted => !v.assign.unwrap(),
                             RephaseTarget::Polarity => {
                                 if self.rng.next_f64() <= v.polarity.abs().powf(1.1) {

From 7f2fea000bae0bbe0f315a334897570e3c1230db Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Wed, 8 Jul 2026 17:05:48 +0900
Subject: [PATCH 19/26] a snapshot

---
 src/assign/propagate.rs    |   2 +-
 src/cdb/db.rs              | 171 ++++++++++++++++++++-----------------
 src/cdb/mod.rs             |   2 +-
 src/cdb/vivify.rs          |  26 +++---
 src/processor/eliminate.rs |   5 ++
 src/solver/conflict.rs     |   4 +-
 src/solver/search.rs       |  25 ++++--
 src/state.rs               |   3 +
 src/types/clause.rs        |  32 +++----
 9 files changed, 155 insertions(+), 115 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 6ed720a6d..728b5859c 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -251,7 +251,7 @@ impl PropagateIF for AssignStack {
                             RephaseTarget::Random => self.rng.next_bool(),
                             RephaseTarget::Inverted => !v.assign.unwrap(),
                             RephaseTarget::Polarity => {
-                                if self.rng.next_f64() <= v.polarity.abs().powf(1.1) {
+                                if self.rng.next_f64() <= v.polarity.abs().powf(1.2) {
                                     v.assign.unwrap()
                                 } else {
                                     !v.assign.unwrap()
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 2911f9c0c..3b0d27825 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -16,6 +16,7 @@ use {
     },
 };
 
+use std::f64;
 #[cfg(not(feature = "no_IO"))]
 use std::{fs::File, io::Write, path::Path};
 
@@ -313,11 +314,6 @@ impl ClauseDBIF for ClauseDB {
             c.flags = FlagClause::empty();
             debug_assert!(c.lits.is_empty()); // c.lits.clear();
             std::mem::swap(&mut c.lits, vec);
-            c.search_from = 2;
-            c.referred_at = 0;
-            c.reference_rate = 1.0;
-            c.vivify_age = 0;
-            c.vivify_at = 0;
         } else {
             cid = ClauseId::from(self.clause.len());
             let mut c = Clause {
@@ -339,6 +335,12 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
+        c.search_from = 2;
+        c.lbd = DecisionLevel::MAX;
+        c.born_at = 0;
+        c.vivify_age = 0;
+        c.vivify_at = 0;
+        c.reference_distance_sum = 0;
         let len2 = c.lits.len() == 2;
         *num_clause += 1;
         if learnt {
@@ -831,7 +833,7 @@ impl ClauseDBIF for ClauseDB {
         c.is(FlagClause::LEARNT)
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    fn reduce(&mut self, asg: &mut impl AssignIF) {
+    fn reduce(&mut self, asg: &mut impl AssignIF, span: usize) {
         self.num_reduction += 1;
         let ClauseDB {
             clause,
@@ -848,14 +850,12 @@ impl ClauseDBIF for ClauseDB {
         *num_lbd2 = 0;
         let num_conflict = asg.derefer(assign::property::Tusize::NumConflict);
         let mut num_alives: usize = 0;
-        // tier 1 group: the small clauses under the best assignment
+        let mut tier0: Vec<SortKey<usize>> = Vec::new();
+        // let mut tier1: Vec<SortKey<usize>> = Vec::new();
+        // let mut tier2: Vec<SortKey<usize>> = Vec::new();
         let mut ntier1: usize = 0;
-        // tier 2 group: the small clauses under the best assignment
-        let mut ntier2: usize = 10_000;
-        let mut cands: Vec<SortKey<usize>> = Vec::new();
-        let thr: f64 = 1.0;
-        let scale: f64 = 2.0;
-        let cutoff: DecisionLevel = 3;
+        let mut ntier2: usize = 0;
+        let _lits_index = |lits: &[Lit]| lits.iter().map(|l| asg.activity(l.vi())).sum::<f64>();
         for (i, c) in clause
             .iter_mut()
             .enumerate()
@@ -863,24 +863,27 @@ impl ClauseDBIF for ClauseDB {
             .filter(|(_, c)| !c.is_dead())
         {
             num_alives += 1;
-            c.update_reference_rate(num_conflict);
-            match c.lbd {
-                0..=2 => {
-                    *num_lbd2 += 1;
-                    continue;
-                }
-                n @ (3..=5) if c.reference_rate >= scale.powf((n - cutoff) as f64) * thr => {
-                    ntier1 += 1;
-                    continue;
-                }
-                _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => {
-                    continue;
-                }
-                n @ (6..) if c.reference_rate >= scale.powf((n - cutoff) as f64) * thr => {
-                    cands.push(SortKey::new(i, c.len() as f64));
-                    continue;
+            if !c.is(FlagClause::LEARNT) {
+                *num_lbd2 += (c.lbd <= 2) as usize;
+                continue;
+            }
+            if c.is(FlagClause::ASSIGN_REASON) {
+                *num_lbd2 += (c.lbd <= 2) as usize;
+                continue;
+            }
+            // clause criteia : LBD - 1 / SIZE
+            let a: usize = num_conflict - c.referred_at;
+            let l: usize = c.lbd as usize;
+            let s: usize = c.len().saturating_sub(2).pow(2);
+            let d: f64 = c.reference_distance();
+            if a <= (100_000 / l).max(400_000 / s) && d <= 35.0 {
+                match c.lbd {
+                    0..=2 => *num_lbd2 += 1,
+                    3..=6 => ntier1 += 1,
+                    _ => ntier2 += 1,
                 }
-                _ => (),
+                // tier0.push(SortKey::new(i, d));
+                continue;
             }
             remove_clause_fn(
                 certification_store,
@@ -893,54 +896,69 @@ impl ClauseDBIF for ClauseDB {
                 c,
             );
             freelist.push(ClauseId::from(i));
-            /* match c.len() {
-                0..=5 => {
-                    *num_lbd2 += 1;
-                    continue;
-                }
-                6..=8 if c.reference_rate >= 0.0001 => {
-                    ntier1 += 1;
-                    continue;
-                }
-                9 | 10 if c.reference_rate >= 0.001 => {
-                    ntier2 += 1;
-                    continue;
-                }
-                11 | 12 if c.reference_rate >= 0.01 => {
-                    ntier2 += 1;
-                    continue;
-                }
-                _ if c.lbd <= 6 && c.reference_rate >= 1.0 => {
-                    continue;
-                }
-                _ if c.referred_at >= *last_reduction_at /* && referred */ => {
-                    continue;
-                }
-                _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => {
-                    continue;
-                }
-                _ => {
-                    remove_clause_fn(
-                        certification_store,
-                        binary_link,
-                        watch_cache,
-                        num_bi_clause,
-                        num_clause,
-                        num_learnt,
-                        ClauseId::from(i),
-                        c,
-                    );
-                    freelist.push(ClauseId::from(i));
+        }
+        tier0.sort_unstable();
+        let mut sum: f64 = 0.0;
+        // let thr: f64 = span as f64;
+        let thr: f64 = (100_000 + 2 * *num_lbd2 + span) as f64;
+        for (_, cid) in tier0.into_iter().enumerate() {
+            // let r = (sum / thr).min(1.0);
+            let c = &mut clause[cid.to()];
+            // if c.lbd as f64 <= 32.0 * (1.0 - r).powf(1.2) + 2.0 {
+            if sum < thr {
+                match c.lbd {
+                    0..=2 => (),
+                    3..=6 => ntier1 += 1,
+                    _ => ntier2 += 1,
                 }
+                sum += c.len() as f64;
+                sum += cid.value();
+                continue;
             }
-            */
+            // if c.len() <= 5 && c.reference_distance(40_000, num_conflict) < 1.0 {
+            //     continue;
+            // }
+            let cid = ClauseId::from(cid.to());
+            remove_clause_fn(
+                certification_store,
+                binary_link,
+                watch_cache,
+                num_bi_clause,
+                num_clause,
+                num_learnt,
+                cid,
+                c,
+            );
+            freelist.push(cid);
+        }
+        /*
+        let thr = span.saturating_sub(ntier1 + *num_lbd2);
+        if tier1.len() > thr {
+            ntier1 += thr;
+            tier1.sort_unstable();
+            for cid in tier1.into_iter().skip(thr) {
+                let c = &mut clause[cid.to()];
+                let cid = ClauseId::from(cid.to());
+                remove_clause_fn(
+                    certification_store,
+                    binary_link,
+                    watch_cache,
+                    num_bi_clause,
+                    num_clause,
+                    num_learnt,
+                    cid,
+                    c,
+                );
+                freelist.push(cid);
+            }
+        } else {
+            ntier1 += tier1.len();
         }
-        if cands.len() > ntier2 {
-            cands.sort_unstable();
-            for cid in cands
-                .iter() // .skip(ntier1)
-                .skip(ntier2)
-            {
+        let thr = span.saturating_sub(ntier2);
+        if tier2.len() > thr {
+            ntier2 += thr;
+            tier2.sort_unstable();
+            for cid in tier2.into_iter().skip(thr) {
                 let c = &mut clause[cid.to()];
                 let cid = ClauseId::from(cid.to());
                 remove_clause_fn(
@@ -956,8 +974,9 @@ impl ClauseDBIF for ClauseDB {
                 freelist.push(cid);
             }
         } else {
-            ntier2 = cands.len();
+            ntier2 += tier2.len();
         }
+        */
         self.last_reduction_at = num_conflict;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 399ee624a..3e1820f79 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -103,7 +103,7 @@ pub trait ClauseDBIF:
     /// reduce learnt clauses
     /// # CAVEAT
     /// *precondition*: decision level == 0.
-    fn reduce(&mut self, asg: &mut impl AssignIF);
+    fn reduce(&mut self, asg: &mut impl AssignIF, span: usize);
     /// turn `FlagClause::BEST_PROPAGATOR` of 'used clauses' on
     fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool);
     /// update flags.
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 102f0da6a..11357712e 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -49,8 +49,8 @@ impl VivifyIF for ClauseDB {
             if c.is_dead() {
                 continue;
             }
-            let span: usize = 4_000 * (c.vivify_age + 1);
-            if c.vivify_at.max(c.referred_at) + span > asg.num_conflict {
+            let span: usize = 4_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1);
+            if c.vivify_at.max(c.born_at) + span > asg.num_conflict {
                 continue;
             }
             let c = &mut self[cid];
@@ -60,15 +60,20 @@ impl VivifyIF for ClauseDB {
             // that are not too short and have a moderate LBD; outside this band
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
-            if 6 < c.lbd {
-                continue;
-            }
-            c.vivify_age += 1;
+            // if 6 < c.lbd {
+            //     continue;
+            // }
+            // if c.vivify_age > 6 {
+            //     continue;
+            // }
+            // assert!(!c.is(FlagClause::ASSIGN_REASON));
             c.vivify_at = asg.num_conflict;
             let is_learnt = c.is(FlagClause::LEARNT);
+            let lbd = c.lbd;
             let vivify_at = c.vivify_at;
-            let referred_at = c.referred_at;
-            let reference_rate = c.reference_rate;
+            c.vivify_age += 1;
+            let born_at = c.born_at;
+            let reference_dist = c.reference_distance_sum;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
             if to_display <= num_check {
                 state.flush("");
@@ -156,9 +161,10 @@ impl VivifyIF for ClauseDB {
                                 _ => {
                                     if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new()
                                     {
-                                        self[cid].referred_at = referred_at;
-                                        self[cid].reference_rate = reference_rate;
+                                        self[cid].born_at = born_at;
+                                        self[cid].reference_distance_sum = reference_dist;
                                         self[cid].vivify_at = vivify_at;
+                                        self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
                                     }
                                     self.remove_clause(cid);
                                     num_shrink += 1;
diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs
index 61bc87b4e..7e2ea9acc 100644
--- a/src/processor/eliminate.rs
+++ b/src/processor/eliminate.rs
@@ -94,6 +94,11 @@ pub fn eliminate_var(
                         RefClause::Clause(ci) => {
                             // the merged clause might be a duplicated clause.
                             elim.add_cid_occur(asg, ci, &mut cdb[ci], true);
+                            cdb[ci].born_at = cdb[*p].born_at.max(cdb[*n].born_at);
+                            cdb[ci].reference_distance_sum = cdb[*p]
+                                .reference_distance_sum
+                                .min(cdb[*n].reference_distance_sum);
+                            cdb[ci].lbd = cdb[*p].lbd.max(cdb[*n].lbd);
 
                             #[cfg(feature = "trace_elimination")]
                             println!(
diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs
index e90fe9602..daa81f340 100644
--- a/src/solver/conflict.rs
+++ b/src/solver/conflict.rs
@@ -216,7 +216,6 @@ pub fn handle_conflict(
                 asg.assign_by_implication(l0, AssignReason::Implication(cid), assign_level);
                 cdb[cid].turn_on(FlagClause::ASSIGN_REASON);
             }
-            cdb[cid].reference_rate = 1.0;
             // lbd should be calculated at conflict level, where all literals are assigned.
             // But since vars hold the last level even after unassignment,
             // we can have postponed the calculation.
@@ -422,8 +421,7 @@ fn conflict_analyze(
                         trace!(q, " -- ignore flagged already");
                     }
                 }
-                cdb[cid].referred_at = asg.num_conflict;
-                cdb[cid].referred += 1;
+                cdb[cid].update_reference(asg.num_conflict, dl as usize);
                 cdb[cid].lbd = cdb[cid]
                     .lbd
                     .min(asg.literal_block_distance_current(&cdb[cid].lits));
diff --git a/src/solver/search.rs b/src/solver/search.rs
index aa0d6fda9..c799b81eb 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -247,7 +247,7 @@ fn search(
     let reduction_interval: usize = 40_000;
     let mut rephase_rotation_pressure: usize = 0;
     let mut vivification_pressure: usize = 0;
-    let vivification_interval: usize = 80_000;
+    let vivification_interval: usize = 40_000;
     let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0];
     let vmtf_interval: usize = 20;
     let mut assign_peak: usize = 0;
@@ -259,7 +259,7 @@ fn search(
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
-            cdb.reduce(asg);
+            cdb.reduce(asg, state.span_manager.current_segment());
         }};
     }
     macro_rules! to_lrb {
@@ -340,6 +340,7 @@ fn search(
             return Err(SolverError::RootLevelConflict(cc));
         }
         asg.update_activity_tick();
+        let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar);
         let (cid, lbd) = handle_conflict(asg, cdb, state, &cc)?;
         if cid == ClauseId::default() {
             match asg.activity_scheme {
@@ -356,6 +357,7 @@ fn search(
         } else {
             cdb.lbd.update(lbd as f64);
             cdb[cid].lbd = DecisionLevel::MAX;
+            cdb[cid].born_at = asg.num_conflict;
         }
         match asg.stack_len().cmp(&assign_peak) {
             Ordering::Less => {}
@@ -396,14 +398,20 @@ fn search(
         span_len += 1;
         // Don't check with `>= 1 * reduction_interval`. It prevents `reduce!(true)`.
         if reduction_pressure > reduction_interval {
+            state.flush("");
+            state.flush(format!("{:>9}", state.span_manager.current_segment()));
             reduce!();
         }
         if state.span_manager.span_ended(span_len / span_scale) {
             span_len = 0;
             let new_segment = state.span_manager.prepare_new_span(span_len);
             dump_stage(asg, state, new_segment);
-            let unasserted_pre = asg.derefer(assign::property::Tusize::NumUnassertedVar);
             RESTART!(asg, cdb, state)?;
+            // if reduction_pressure > reduction_interval {
+            //     state.flush("");
+            //     state.flush(format!("{:>9}", state.span_manager.current_segment()));
+            //     reduce!();
+            // }
             if vivification_pressure >= vivification_interval {
                 if cfg!(feature = "clause_vivification") {
                     cdb.vivify(asg, state, true)?;
@@ -419,11 +427,6 @@ fn search(
                 }
                 elimination_pressure = 0;
             }
-            let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar);
-            if unasserted_now != unasserted_pre {
-                update_core!(unasserted_pre - unasserted_now);
-                // to_vmtf!();
-            }
             if cfg!(feature = "rephase") {
                 match asg.activity_scheme {
                     VarActivityScheme::LRB
@@ -451,6 +454,12 @@ fn search(
                 asg.rescale_learning_rate(0.9);
             }
         }
+        let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar);
+        if unasserted_now != unasserted_pre {
+            state.last_assertion = asg.num_conflict;
+            update_core!(unasserted_pre - unasserted_now);
+            // to_vmtf!();
+        }
         if progress_pressure >= progress_interval {
             state.progress(asg, cdb);
             if let Some(p) = state.elapsed() {
diff --git a/src/state.rs b/src/state.rs
index ac9053f5c..b9d9fbd93 100644
--- a/src/state.rs
+++ b/src/state.rs
@@ -123,6 +123,8 @@ pub struct State {
     pub core_size: usize,
     /// the last restart in conflicts
     pub last_restart: usize,
+    /// the last assertion in conflicts
+    pub last_assertion: usize,
 
     #[cfg(feature = "chrono_BT")]
     /// chronoBT threshold
@@ -167,6 +169,7 @@ impl Default for State {
             bt_drift_average: Ema::default().with_span(1000),
             core_size: 0,
             last_restart: 0,
+            last_assertion: 0,
 
             #[cfg(feature = "chrono_BT")]
             chrono_bt_threshold: 100,
diff --git a/src/types/clause.rs b/src/types/clause.rs
index 868b743c1..b0478b1d7 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -19,10 +19,11 @@ pub struct Clause {
     pub search_from: u16,
     /// The number of referrences in conflict analysis
     pub(crate) referred: usize,
-    /// Sum of activated (used as propagated) duration
     pub(crate) referred_at: usize,
+    /// Sum of activated (used as propagated) duration
+    pub(crate) born_at: usize,
     /// The average number of references in a vivification interval
-    pub(crate) reference_rate: f64,
+    pub(crate) reference_distance_sum: usize,
     /// last vivified time in conflicts
     pub(crate) vivify_age: usize,
     // last vivified time in conflict
@@ -51,8 +52,10 @@ pub trait ClauseIF {
     fn len(&self) -> usize;
     /// return true is this is a unit clause under `asg`.
     fn is_unit_under(&self, asg: &impl AssignIF) -> bool;
-    /// update reference_rate and return `true` if referred.
-    fn update_reference_rate(&mut self, base: usize) -> bool;
+    /// update reference_distance.
+    fn update_reference(&mut self, now: usize, literal_distance: usize);
+    /// return reference distance as `f64`
+    fn reference_distance(&self) -> f64;
 }
 
 impl Default for Clause {
@@ -63,7 +66,8 @@ impl Default for Clause {
             search_from: 2,
             referred: 0,
             referred_at: 0,
-            reference_rate: 1.0,
+            born_at: 0,
+            reference_distance_sum: 0,
             vivify_age: 0,
             vivify_at: 0,
             lbd: DecisionLevel::MAX,
@@ -223,17 +227,13 @@ impl ClauseIF for Clause {
             .all(|l| asg.assigned(*l) == Some(false));
         unassigned == 1 && all_others_false
     }
-    fn update_reference_rate(&mut self, base: usize) -> bool {
-        let span: usize = 10_000; //  * (1.0 + self.vivify_age as f64).powf(1.0);
-        if self.referred_at + span <= base {
-            let referred = self.referred >= 1;
-            self.reference_rate *= 0.9;
-            self.reference_rate += 0.1 * self.referred as f64;
-            self.referred = 0;
-            referred
-        } else {
-            true
-        }
+    fn update_reference(&mut self, now: usize, literal_distance: usize) {
+        self.referred += 1;
+        self.referred_at = now;
+        self.reference_distance_sum += literal_distance;
+    }
+    fn reference_distance(&self) -> f64 {
+        self.reference_distance_sum as f64 / (1 + self.referred) as f64
     }
 }
 

From fe8395928fbe67544c19bd34e46c052685e72b19 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Thu, 9 Jul 2026 17:28:57 +0900
Subject: [PATCH 20/26] exp: another better snapshot

---
 src/cdb/db.rs              | 95 ++++++++++++--------------------------
 src/cdb/mod.rs             |  2 +-
 src/cdb/vivify.rs          |  4 +-
 src/processor/eliminate.rs |  5 +-
 src/solver/search.rs       |  8 +---
 src/state.rs               |  4 +-
 src/types/clause.rs        | 13 ++++--
 7 files changed, 48 insertions(+), 83 deletions(-)

diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 3b0d27825..ec0a085e8 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -1,5 +1,3 @@
-use crate::assign;
-
 use {
     super::{
         BinaryLinkDB, CertificationStore, ClauseDBIF, ClauseId, RefClause,
@@ -69,7 +67,7 @@ pub struct ClauseDB {
     pub(crate) tier1_clauses: Ema,
     /// the ratio of pretty good learnt clauses
     pub(crate) tier2_clauses: Ema,
-    pub(crate) last_reduction_at: usize,
+    pub(crate) last_reduction_count: usize,
 }
 
 impl Default for ClauseDB {
@@ -92,7 +90,7 @@ impl Default for ClauseDB {
             num_reregistration: 0,
             tier1_clauses: Ema::default(),
             tier2_clauses: Ema::default(),
-            last_reduction_at: 0,
+            last_reduction_count: 0,
         }
     }
 }
@@ -340,7 +338,7 @@ impl ClauseDBIF for ClauseDB {
         c.born_at = 0;
         c.vivify_age = 0;
         c.vivify_at = 0;
-        c.reference_distance_sum = 0;
+        c.reference_height = 0;
         let len2 = c.lits.len() == 2;
         *num_clause += 1;
         if learnt {
@@ -833,7 +831,7 @@ impl ClauseDBIF for ClauseDB {
         c.is(FlagClause::LEARNT)
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    fn reduce(&mut self, asg: &mut impl AssignIF, span: usize) {
+    fn reduce(&mut self, asg: &mut impl AssignIF, b_lvl: f64) {
         self.num_reduction += 1;
         let ClauseDB {
             clause,
@@ -848,14 +846,14 @@ impl ClauseDBIF for ClauseDB {
             ..
         } = self;
         *num_lbd2 = 0;
-        let num_conflict = asg.derefer(assign::property::Tusize::NumConflict);
         let mut num_alives: usize = 0;
-        let mut tier0: Vec<SortKey<usize>> = Vec::new();
-        // let mut tier1: Vec<SortKey<usize>> = Vec::new();
+        let mut reserved: Vec<SortKey<usize>> = Vec::new();
         // let mut tier2: Vec<SortKey<usize>> = Vec::new();
         let mut ntier1: usize = 0;
         let mut ntier2: usize = 0;
+        let mut survived: usize = 0;
         let _lits_index = |lits: &[Lit]| lits.iter().map(|l| asg.activity(l.vi())).sum::<f64>();
+        let depth = (b_lvl / 2.0).min(16.0);
         for (i, c) in clause
             .iter_mut()
             .enumerate()
@@ -869,20 +867,23 @@ impl ClauseDBIF for ClauseDB {
             }
             if c.is(FlagClause::ASSIGN_REASON) {
                 *num_lbd2 += (c.lbd <= 2) as usize;
+                c.reference_height += c.lbd.ilog2() as usize;
                 continue;
             }
-            // clause criteia : LBD - 1 / SIZE
-            let a: usize = num_conflict - c.referred_at;
-            let l: usize = c.lbd as usize;
-            let s: usize = c.len().saturating_sub(2).pow(2);
             let d: f64 = c.reference_distance();
-            if a <= (100_000 / l).max(400_000 / s) && d <= 35.0 {
+            if d <= depth {
                 match c.lbd {
                     0..=2 => *num_lbd2 += 1,
                     3..=6 => ntier1 += 1,
                     _ => ntier2 += 1,
                 }
-                // tier0.push(SortKey::new(i, d));
+                c.reference_height += c.lbd.ilog2() as usize;
+                survived += 1;
+                continue;
+            }
+            // Note: assert!(c.len() > 2)
+            if d <= depth + 1.0 || c.len() <= 3 {
+                reserved.push(SortKey::new(i, c.lbd as f64));
                 continue;
             }
             remove_clause_fn(
@@ -897,48 +898,21 @@ impl ClauseDBIF for ClauseDB {
             );
             freelist.push(ClauseId::from(i));
         }
-        tier0.sort_unstable();
-        let mut sum: f64 = 0.0;
-        // let thr: f64 = span as f64;
-        let thr: f64 = (100_000 + 2 * *num_lbd2 + span) as f64;
-        for (_, cid) in tier0.into_iter().enumerate() {
-            // let r = (sum / thr).min(1.0);
-            let c = &mut clause[cid.to()];
-            // if c.lbd as f64 <= 32.0 * (1.0 - r).powf(1.2) + 2.0 {
-            if sum < thr {
+        if survived < 40_000 {
+            reserved.sort_unstable();
+            for i in reserved.iter().take(survived) {
+                let c = &mut clause[i.to()];
                 match c.lbd {
-                    0..=2 => (),
+                    0..=2 => *num_lbd2 += 1,
                     3..=6 => ntier1 += 1,
                     _ => ntier2 += 1,
                 }
-                sum += c.len() as f64;
-                sum += cid.value();
-                continue;
+                c.reference_height += c.lbd.ilog2() as usize;
+                survived += 1;
             }
-            // if c.len() <= 5 && c.reference_distance(40_000, num_conflict) < 1.0 {
-            //     continue;
-            // }
-            let cid = ClauseId::from(cid.to());
-            remove_clause_fn(
-                certification_store,
-                binary_link,
-                watch_cache,
-                num_bi_clause,
-                num_clause,
-                num_learnt,
-                cid,
-                c,
-            );
-            freelist.push(cid);
-        }
-        /*
-        let thr = span.saturating_sub(ntier1 + *num_lbd2);
-        if tier1.len() > thr {
-            ntier1 += thr;
-            tier1.sort_unstable();
-            for cid in tier1.into_iter().skip(thr) {
-                let c = &mut clause[cid.to()];
-                let cid = ClauseId::from(cid.to());
+            for i in reserved.iter().skip(survived) {
+                let c = &mut clause[i.to()];
+                let cid = ClauseId::from(i.to());
                 remove_clause_fn(
                     certification_store,
                     binary_link,
@@ -952,15 +926,9 @@ impl ClauseDBIF for ClauseDB {
                 freelist.push(cid);
             }
         } else {
-            ntier1 += tier1.len();
-        }
-        let thr = span.saturating_sub(ntier2);
-        if tier2.len() > thr {
-            ntier2 += thr;
-            tier2.sort_unstable();
-            for cid in tier2.into_iter().skip(thr) {
-                let c = &mut clause[cid.to()];
-                let cid = ClauseId::from(cid.to());
+            for i in reserved {
+                let c = &mut clause[i.to()];
+                let cid = ClauseId::from(i.to());
                 remove_clause_fn(
                     certification_store,
                     binary_link,
@@ -973,11 +941,8 @@ impl ClauseDBIF for ClauseDB {
                 );
                 freelist.push(cid);
             }
-        } else {
-            ntier2 += tier2.len();
         }
-        */
-        self.last_reduction_at = num_conflict;
+        self.last_reduction_count = survived;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
     }
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 3e1820f79..9790daad1 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -103,7 +103,7 @@ pub trait ClauseDBIF:
     /// reduce learnt clauses
     /// # CAVEAT
     /// *precondition*: decision level == 0.
-    fn reduce(&mut self, asg: &mut impl AssignIF, span: usize);
+    fn reduce(&mut self, asg: &mut impl AssignIF, b_lvl: f64);
     /// turn `FlagClause::BEST_PROPAGATOR` of 'used clauses' on
     fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool);
     /// update flags.
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 11357712e..7aaa70305 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -73,7 +73,7 @@ impl VivifyIF for ClauseDB {
             let vivify_at = c.vivify_at;
             c.vivify_age += 1;
             let born_at = c.born_at;
-            let reference_dist = c.reference_distance_sum;
+            let reference_dist = c.reference_height;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
             if to_display <= num_check {
                 state.flush("");
@@ -162,7 +162,7 @@ impl VivifyIF for ClauseDB {
                                     if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new()
                                     {
                                         self[cid].born_at = born_at;
-                                        self[cid].reference_distance_sum = reference_dist;
+                                        self[cid].reference_height = reference_dist;
                                         self[cid].vivify_at = vivify_at;
                                         self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
                                     }
diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs
index 7e2ea9acc..fb635cc7a 100644
--- a/src/processor/eliminate.rs
+++ b/src/processor/eliminate.rs
@@ -95,9 +95,8 @@ pub fn eliminate_var(
                             // the merged clause might be a duplicated clause.
                             elim.add_cid_occur(asg, ci, &mut cdb[ci], true);
                             cdb[ci].born_at = cdb[*p].born_at.max(cdb[*n].born_at);
-                            cdb[ci].reference_distance_sum = cdb[*p]
-                                .reference_distance_sum
-                                .min(cdb[*n].reference_distance_sum);
+                            cdb[ci].reference_height =
+                                cdb[*p].reference_height.min(cdb[*n].reference_height);
                             cdb[ci].lbd = cdb[*p].lbd.max(cdb[*n].lbd);
 
                             #[cfg(feature = "trace_elimination")]
diff --git a/src/solver/search.rs b/src/solver/search.rs
index c799b81eb..627af9934 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -251,7 +251,7 @@ fn search(
     let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0];
     let vmtf_interval: usize = 20;
     let mut assign_peak: usize = 0;
-    let luby_scale: usize = 256;
+    let luby_scale: usize = 80;
     let mut span_scale: usize = luby_scale;
 
     macro_rules! reduce {
@@ -259,7 +259,7 @@ fn search(
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
-            cdb.reduce(asg, state.span_manager.current_segment());
+            cdb.reduce(asg, state.b_lvl.get_slow());
         }};
     }
     macro_rules! to_lrb {
@@ -398,8 +398,6 @@ fn search(
         span_len += 1;
         // Don't check with `>= 1 * reduction_interval`. It prevents `reduce!(true)`.
         if reduction_pressure > reduction_interval {
-            state.flush("");
-            state.flush(format!("{:>9}", state.span_manager.current_segment()));
             reduce!();
         }
         if state.span_manager.span_ended(span_len / span_scale) {
@@ -408,8 +406,6 @@ fn search(
             dump_stage(asg, state, new_segment);
             RESTART!(asg, cdb, state)?;
             // if reduction_pressure > reduction_interval {
-            //     state.flush("");
-            //     state.flush(format!("{:>9}", state.span_manager.current_segment()));
             //     reduce!();
             // }
             if vivification_pressure >= vivification_interval {
diff --git a/src/state.rs b/src/state.rs
index b9d9fbd93..d6947bc43 100644
--- a/src/state.rs
+++ b/src/state.rs
@@ -164,8 +164,8 @@ impl Default for State {
                 Ema2::default().with_value(0.5),
                 Ema2::default().with_value(0.5),
             ),
-            b_lvl: Ema2::default_extended(),
-            c_lvl: Ema2::default_extended(),
+            b_lvl: Ema2::default_extended().with_slow(80_000),
+            c_lvl: Ema2::default_extended().with_slow(80_000),
             bt_drift_average: Ema::default().with_span(1000),
             core_size: 0,
             last_restart: 0,
diff --git a/src/types/clause.rs b/src/types/clause.rs
index b0478b1d7..05bab6323 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -23,7 +23,7 @@ pub struct Clause {
     /// Sum of activated (used as propagated) duration
     pub(crate) born_at: usize,
     /// The average number of references in a vivification interval
-    pub(crate) reference_distance_sum: usize,
+    pub(crate) reference_height: usize,
     /// last vivified time in conflicts
     pub(crate) vivify_age: usize,
     // last vivified time in conflict
@@ -67,7 +67,7 @@ impl Default for Clause {
             referred: 0,
             referred_at: 0,
             born_at: 0,
-            reference_distance_sum: 0,
+            reference_height: 0,
             vivify_age: 0,
             vivify_at: 0,
             lbd: DecisionLevel::MAX,
@@ -230,10 +230,15 @@ impl ClauseIF for Clause {
     fn update_reference(&mut self, now: usize, literal_distance: usize) {
         self.referred += 1;
         self.referred_at = now;
-        self.reference_distance_sum += literal_distance;
+        if self.reference_height == 0 {
+            self.reference_height = literal_distance;
+        }
+        self.reference_height = self.reference_height.min(literal_distance);
+        // self.reference_distance_sum += literal_distance;
     }
     fn reference_distance(&self) -> f64 {
-        self.reference_distance_sum as f64 / (1 + self.referred) as f64
+        self.reference_height as f64
+        // self.reference_distance_sum as f64 / (1 + self.referred) as f64
     }
 }
 

From d04d5a71027c0f1fbbbed11d8109f16a25b5ad3b Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Sat, 11 Jul 2026 13:24:07 +0900
Subject: [PATCH 21/26] exp: another better snapshot

---
 src/assign/mod.rs      |  2 +
 src/assign/stack.rs    |  3 ++
 src/cdb/db.rs          | 84 +++++++++++++-----------------------------
 src/cdb/mod.rs         |  4 +-
 src/cdb/vivify.rs      |  6 +--
 src/solver/conflict.rs | 13 ++++++-
 src/solver/search.rs   |  2 +-
 src/types/clause.rs    | 22 ++++-------
 8 files changed, 56 insertions(+), 80 deletions(-)

diff --git a/src/assign/mod.rs b/src/assign/mod.rs
index 1258dd435..3889cc8b4 100644
--- a/src/assign/mod.rs
+++ b/src/assign/mod.rs
@@ -43,6 +43,8 @@ pub trait AssignIF:
 {
     /// return root level.
     fn root_level(&self) -> DecisionLevel;
+    /// return current conflict index.
+    fn current_conflict_index(&self) -> usize;
     /// return a literal in the stack.
     fn stack(&self, i: usize) -> Lit;
     /// return literals in the range of stack.
diff --git a/src/assign/stack.rs b/src/assign/stack.rs
index 98472884e..bfadaf97b 100644
--- a/src/assign/stack.rs
+++ b/src/assign/stack.rs
@@ -204,6 +204,9 @@ impl AssignIF for AssignStack {
     fn root_level(&self) -> DecisionLevel {
         self.root_level
     }
+    fn current_conflict_index(&self) -> usize {
+        self.num_conflict
+    }
     fn stack(&self, i: usize) -> Lit {
         self.trail[i]
     }
diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index ec0a085e8..fe735397a 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -5,7 +5,7 @@ use {
         property,
         watch_cache::*,
     },
-    crate::{assign::AssignIF, types::*},
+    crate::{assign::AssignIF, state::State, types::*},
     std::{
         collections::HashMap,
         num::NonZeroU32,
@@ -831,7 +831,7 @@ impl ClauseDBIF for ClauseDB {
         c.is(FlagClause::LEARNT)
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    fn reduce(&mut self, asg: &mut impl AssignIF, b_lvl: f64) {
+    fn reduce(&mut self, _asg: &mut impl AssignIF, state: &State) {
         self.num_reduction += 1;
         let ClauseDB {
             clause,
@@ -845,15 +845,27 @@ impl ClauseDBIF for ClauseDB {
             freelist,
             ..
         } = self;
+        let depth: f64 = 0.6 * state.b_lvl.get_slow();
+        let (total, targets) = clause
+            .iter()
+            .skip(1)
+            .filter(|c| {
+                !c.is_dead() && c.is(FlagClause::LEARNT) && !c.is(FlagClause::ASSIGN_REASON)
+            })
+            .fold((0, 0), |(total, target), c| {
+                (
+                    total + 1,
+                    target + (c.reference_height as f64 + c.lbd as f64 <= depth) as usize,
+                )
+            });
+        if targets as f64 > 0.5 * total as f64 {
+            return;
+        }
         *num_lbd2 = 0;
         let mut num_alives: usize = 0;
-        let mut reserved: Vec<SortKey<usize>> = Vec::new();
-        // let mut tier2: Vec<SortKey<usize>> = Vec::new();
         let mut ntier1: usize = 0;
         let mut ntier2: usize = 0;
         let mut survived: usize = 0;
-        let _lits_index = |lits: &[Lit]| lits.iter().map(|l| asg.activity(l.vi())).sum::<f64>();
-        let depth = (b_lvl / 2.0).min(16.0);
         for (i, c) in clause
             .iter_mut()
             .enumerate()
@@ -867,25 +879,23 @@ impl ClauseDBIF for ClauseDB {
             }
             if c.is(FlagClause::ASSIGN_REASON) {
                 *num_lbd2 += (c.lbd <= 2) as usize;
-                c.reference_height += c.lbd.ilog2() as usize;
+                c.reference_height += c.lbd.ilog2() as DecisionLevel;
                 continue;
             }
-            let d: f64 = c.reference_distance();
-            if d <= depth {
+            // Don't introduce any length-based crteria!
+            // Clause lengths without context make result worse.
+            if c.reference_height as f64 + c.lbd as f64 <= depth {
                 match c.lbd {
                     0..=2 => *num_lbd2 += 1,
                     3..=6 => ntier1 += 1,
                     _ => ntier2 += 1,
                 }
-                c.reference_height += c.lbd.ilog2() as usize;
+                if targets >= 20_000 {
+                    c.reference_height += c.lbd.ilog2() as DecisionLevel;
+                }
                 survived += 1;
                 continue;
             }
-            // Note: assert!(c.len() > 2)
-            if d <= depth + 1.0 || c.len() <= 3 {
-                reserved.push(SortKey::new(i, c.lbd as f64));
-                continue;
-            }
             remove_clause_fn(
                 certification_store,
                 binary_link,
@@ -898,50 +908,6 @@ impl ClauseDBIF for ClauseDB {
             );
             freelist.push(ClauseId::from(i));
         }
-        if survived < 40_000 {
-            reserved.sort_unstable();
-            for i in reserved.iter().take(survived) {
-                let c = &mut clause[i.to()];
-                match c.lbd {
-                    0..=2 => *num_lbd2 += 1,
-                    3..=6 => ntier1 += 1,
-                    _ => ntier2 += 1,
-                }
-                c.reference_height += c.lbd.ilog2() as usize;
-                survived += 1;
-            }
-            for i in reserved.iter().skip(survived) {
-                let c = &mut clause[i.to()];
-                let cid = ClauseId::from(i.to());
-                remove_clause_fn(
-                    certification_store,
-                    binary_link,
-                    watch_cache,
-                    num_bi_clause,
-                    num_clause,
-                    num_learnt,
-                    cid,
-                    c,
-                );
-                freelist.push(cid);
-            }
-        } else {
-            for i in reserved {
-                let c = &mut clause[i.to()];
-                let cid = ClauseId::from(i.to());
-                remove_clause_fn(
-                    certification_store,
-                    binary_link,
-                    watch_cache,
-                    num_bi_clause,
-                    num_clause,
-                    num_learnt,
-                    cid,
-                    c,
-                );
-                freelist.push(cid);
-            }
-        }
         self.last_reduction_count = survived;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 9790daad1..65e2a4532 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -23,7 +23,7 @@ pub use self::{
 };
 
 use {
-    crate::{assign::AssignIF, types::*},
+    crate::{assign::AssignIF, state::State, types::*},
     std::{
         ops::IndexMut,
         slice::{Iter, IterMut},
@@ -103,7 +103,7 @@ pub trait ClauseDBIF:
     /// reduce learnt clauses
     /// # CAVEAT
     /// *precondition*: decision level == 0.
-    fn reduce(&mut self, asg: &mut impl AssignIF, b_lvl: f64);
+    fn reduce(&mut self, asg: &mut impl AssignIF, state: &State);
     /// turn `FlagClause::BEST_PROPAGATOR` of 'used clauses' on
     fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool);
     /// update flags.
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 7aaa70305..d453bd7d3 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -49,7 +49,7 @@ impl VivifyIF for ClauseDB {
             if c.is_dead() {
                 continue;
             }
-            let span: usize = 4_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1);
+            let span: usize = 5_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1);
             if c.vivify_at.max(c.born_at) + span > asg.num_conflict {
                 continue;
             }
@@ -73,7 +73,7 @@ impl VivifyIF for ClauseDB {
             let vivify_at = c.vivify_at;
             c.vivify_age += 1;
             let born_at = c.born_at;
-            let reference_dist = c.reference_height;
+            let reference_height = c.reference_height;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
             if to_display <= num_check {
                 state.flush("");
@@ -162,7 +162,7 @@ impl VivifyIF for ClauseDB {
                                     if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new()
                                     {
                                         self[cid].born_at = born_at;
-                                        self[cid].reference_height = reference_dist;
+                                        self[cid].reference_height = reference_height / 2;
                                         self[cid].vivify_at = vivify_at;
                                         self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
                                     }
diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs
index daa81f340..c4ed23d94 100644
--- a/src/solver/conflict.rs
+++ b/src/solver/conflict.rs
@@ -134,12 +134,23 @@ pub fn handle_conflict(
                 }
             }
             AssignReason::Implication(r) => {
+                let mut cs = Vec::new();
                 for l in cdb[r].iter() {
                     let vi = l.vi();
                     if !bumped.contains(&vi) {
                         asg.reward_at_analysis(vi);
                         bumped.push(vi);
                     }
+                    if let AssignReason::Implication(ci) = asg.reason(l.vi()) {
+                        cs.push((asg.level(l.vi()), ci));
+                    }
+                }
+                for (lvl, ci) in cs.into_iter() {
+                    if cdb[ci].reference_height == 0 {
+                        cdb[ci].reference_height = lvl;
+                    } else {
+                        cdb[ci].reference_height = cdb[ci].reference_height.min(lvl);
+                    }
                 }
             }
             AssignReason::Decision(_) => (),
@@ -421,7 +432,7 @@ fn conflict_analyze(
                         trace!(q, " -- ignore flagged already");
                     }
                 }
-                cdb[cid].update_reference(asg.num_conflict, dl as usize);
+                cdb[cid].update_reference(asg);
                 cdb[cid].lbd = cdb[cid]
                     .lbd
                     .min(asg.literal_block_distance_current(&cdb[cid].lits));
diff --git a/src/solver/search.rs b/src/solver/search.rs
index 627af9934..5fe8e8e41 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -259,7 +259,7 @@ fn search(
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
-            cdb.reduce(asg, state.b_lvl.get_slow());
+            cdb.reduce(asg, state);
         }};
     }
     macro_rules! to_lrb {
diff --git a/src/types/clause.rs b/src/types/clause.rs
index 05bab6323..31a2317fd 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -22,8 +22,8 @@ pub struct Clause {
     pub(crate) referred_at: usize,
     /// Sum of activated (used as propagated) duration
     pub(crate) born_at: usize,
-    /// The average number of references in a vivification interval
-    pub(crate) reference_height: usize,
+    /// The minimal decision level at which a conflict occured by this clause
+    pub(crate) reference_height: DecisionLevel,
     /// last vivified time in conflicts
     pub(crate) vivify_age: usize,
     // last vivified time in conflict
@@ -53,9 +53,7 @@ pub trait ClauseIF {
     /// return true is this is a unit clause under `asg`.
     fn is_unit_under(&self, asg: &impl AssignIF) -> bool;
     /// update reference_distance.
-    fn update_reference(&mut self, now: usize, literal_distance: usize);
-    /// return reference distance as `f64`
-    fn reference_distance(&self) -> f64;
+    fn update_reference(&mut self, asg: &impl AssignIF);
 }
 
 impl Default for Clause {
@@ -227,18 +225,14 @@ impl ClauseIF for Clause {
             .all(|l| asg.assigned(*l) == Some(false));
         unassigned == 1 && all_others_false
     }
-    fn update_reference(&mut self, now: usize, literal_distance: usize) {
+    fn update_reference(&mut self, asg: &impl AssignIF) {
         self.referred += 1;
-        self.referred_at = now;
+        self.referred_at = asg.current_conflict_index();
+        let level = asg.decision_level();
         if self.reference_height == 0 {
-            self.reference_height = literal_distance;
+            self.reference_height = level;
         }
-        self.reference_height = self.reference_height.min(literal_distance);
-        // self.reference_distance_sum += literal_distance;
-    }
-    fn reference_distance(&self) -> f64 {
-        self.reference_height as f64
-        // self.reference_distance_sum as f64 / (1 + self.referred) as f64
+        self.reference_height = self.reference_height.min(level);
     }
 }
 

From 059c01ee1b531b404ecbf4e6feb5f162c5f7fa51 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 13 Jul 2026 12:04:40 +0900
Subject: [PATCH 22/26] exp: a better snapshot

---
 src/cdb/db.rs          | 74 ++++++++++++++++++++++++++----------------
 src/cdb/mod.rs         |  2 +-
 src/cdb/vivify.rs      | 44 +++++++++++++------------
 src/solver/conflict.rs |  6 +---
 src/solver/search.rs   | 20 ++++++------
 src/types/clause.rs    |  5 +--
 6 files changed, 82 insertions(+), 69 deletions(-)

diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index fe735397a..edb0673a4 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -67,7 +67,7 @@ pub struct ClauseDB {
     pub(crate) tier1_clauses: Ema,
     /// the ratio of pretty good learnt clauses
     pub(crate) tier2_clauses: Ema,
-    pub(crate) last_reduction_count: usize,
+    // pub(crate) last_reduction_count: usize,
 }
 
 impl Default for ClauseDB {
@@ -90,7 +90,7 @@ impl Default for ClauseDB {
             num_reregistration: 0,
             tier1_clauses: Ema::default(),
             tier2_clauses: Ema::default(),
-            last_reduction_count: 0,
+            // last_reduction_count: 0,
         }
     }
 }
@@ -338,7 +338,7 @@ impl ClauseDBIF for ClauseDB {
         c.born_at = 0;
         c.vivify_age = 0;
         c.vivify_at = 0;
-        c.reference_height = 0;
+        c.reference_height = DecisionLevel::MAX;
         let len2 = c.lits.len() == 2;
         *num_clause += 1;
         if learnt {
@@ -831,7 +831,19 @@ impl ClauseDBIF for ClauseDB {
         c.is(FlagClause::LEARNT)
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    fn reduce(&mut self, _asg: &mut impl AssignIF, state: &State) {
+    fn reduce(&mut self, asg: &impl AssignIF, state: &State) {
+        macro_rules! _height {
+            ($c: expr) => {
+                // $c.reference_height as f64
+                ($c.reference_height + ($c.lbd as f64)) as f64
+            };
+        }
+        let conflict_index: usize = asg.current_conflict_index();
+        let _distance: DecisionLevel =
+            2 + (state.c_lvl.get_slow() - state.b_lvl.get_slow()) as DecisionLevel;
+        let _height: f64 = state.b_lvl.get_slow();
+        let udist: DecisionLevel =
+            (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel;
         self.num_reduction += 1;
         let ClauseDB {
             clause,
@@ -845,27 +857,24 @@ impl ClauseDBIF for ClauseDB {
             freelist,
             ..
         } = self;
-        let depth: f64 = 0.6 * state.b_lvl.get_slow();
-        let (total, targets) = clause
-            .iter()
-            .skip(1)
-            .filter(|c| {
-                !c.is_dead() && c.is(FlagClause::LEARNT) && !c.is(FlagClause::ASSIGN_REASON)
-            })
-            .fold((0, 0), |(total, target), c| {
-                (
-                    total + 1,
-                    target + (c.reference_height as f64 + c.lbd as f64 <= depth) as usize,
-                )
-            });
-        if targets as f64 > 0.5 * total as f64 {
-            return;
-        }
+        // let depth: f64 = 6.0 + state.b_lvl.get_slow().log2();
+        // let (total, targets) = clause
+        //     .iter()
+        //     .skip(1)
+        //     .filter(|c| {
+        //         !c.is_dead() && c.is(FlagClause::LEARNT) && !c.is(FlagClause::ASSIGN_REASON)
+        //     })
+        //     .fold((0, 0), |(total, target), c| {
+        //         (total + 1, target + (height!(c) <= depth) as usize)
+        //     });
+        // if targets as f64 > 0.5 * total as f64 {
+        //     return;
+        // }
         *num_lbd2 = 0;
         let mut num_alives: usize = 0;
         let mut ntier1: usize = 0;
         let mut ntier2: usize = 0;
-        let mut survived: usize = 0;
+        // let mut survived: usize = 0;
         for (i, c) in clause
             .iter_mut()
             .enumerate()
@@ -879,21 +888,30 @@ impl ClauseDBIF for ClauseDB {
             }
             if c.is(FlagClause::ASSIGN_REASON) {
                 *num_lbd2 += (c.lbd <= 2) as usize;
-                c.reference_height += c.lbd.ilog2() as DecisionLevel;
+                // c.reference_height += 1.0;
+                // c.reference_height += c.lbd as f64;
+                // c.reference_height += (c.lbd as f64).log2();
                 continue;
             }
             // Don't introduce any length-based crteria!
             // Clause lengths without context make result worse.
-            if c.reference_height as f64 + c.lbd as f64 <= depth {
+            if c.reference_height + c.lbd <= udist
+            // height!(c) <= height
+            //     && c.lbd <= distance
+                && (c.reference_height <= 4 || (conflict_index - c.referred_at) <= 800_000)
+            {
                 match c.lbd {
                     0..=2 => *num_lbd2 += 1,
                     3..=6 => ntier1 += 1,
                     _ => ntier2 += 1,
                 }
-                if targets >= 20_000 {
-                    c.reference_height += c.lbd.ilog2() as DecisionLevel;
-                }
-                survived += 1;
+                // c.reference_height *= 1.1;
+                // c.reference_height += 1.0;
+                // c.reference_height += c.lbd as f64;
+                // if targets >= 20_000 {
+                //     c.reference_height += (c.lbd as f64).log2();
+                // }
+                // survived += 1;
                 continue;
             }
             remove_clause_fn(
@@ -908,7 +926,7 @@ impl ClauseDBIF for ClauseDB {
             );
             freelist.push(ClauseId::from(i));
         }
-        self.last_reduction_count = survived;
+        // self.last_reduction_count = survived;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
     }
diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs
index 65e2a4532..81116ffee 100644
--- a/src/cdb/mod.rs
+++ b/src/cdb/mod.rs
@@ -103,7 +103,7 @@ pub trait ClauseDBIF:
     /// reduce learnt clauses
     /// # CAVEAT
     /// *precondition*: decision level == 0.
-    fn reduce(&mut self, asg: &mut impl AssignIF, state: &State);
+    fn reduce(&mut self, asg: &impl AssignIF, state: &State);
     /// turn `FlagClause::BEST_PROPAGATOR` of 'used clauses' on
     fn save_best_assign_reasons(&mut self, asg: &impl AssignIF, clear: bool);
     /// update flags.
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index d453bd7d3..56b6c6b2e 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -8,30 +8,21 @@ use crate::{
 };
 
 pub trait VivifyIF {
-    fn vivify(
-        &mut self,
-        asg: &mut AssignStack,
-        state: &mut State,
-        skip_evaluation: bool,
-    ) -> MaybeInconsistent;
+    fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent;
 }
 
 impl VivifyIF for ClauseDB {
     /// vivify clauses under `asg`
-    fn vivify(
-        &mut self,
-        asg: &mut AssignStack,
-        state: &mut State,
-        _eval: bool,
-    ) -> MaybeInconsistent {
+    fn vivify(&mut self, asg: &mut AssignStack, state: &mut State) -> MaybeInconsistent {
         // This is a reusable vector to reduce memory consumption,
         // the key is the number of invocation
+        // let db_skip: usize = 1 + self.num_clause / 1_000_000;
         let mut seen: Vec<usize> = vec![0; asg.num_vars + 1];
         let display_step: usize = 1000;
-        let mut num_check = 0;
-        let mut num_shrink = 0;
-        let mut num_assert = 0;
-        let mut to_display = 0;
+        let mut num_check: usize = 0;
+        let mut num_shrink: usize = 0;
+        let mut num_assert: usize = 0;
+        let mut to_display: usize = display_step;
         state[Stat::Vivification] += 1;
         if asg.remains() {
             asg.propagate_sandbox(self).map_err(|cc| {
@@ -49,10 +40,22 @@ impl VivifyIF for ClauseDB {
             if c.is_dead() {
                 continue;
             }
-            let span: usize = 5_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1);
-            if c.vivify_at.max(c.born_at) + span > asg.num_conflict {
+            let span: usize = 10_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1);
+            if c.vivify_at.max(c.born_at) + span > asg.num_conflict
+                || (c.referred_at <= c.vivify_at && (c.is(FlagClause::LEARNT) || c.vivify_age != 0))
+            {
                 continue;
             }
+            num_check += 1;
+            // if !num_check.is_multiple_of(db_skip) && c.reference_height > 0.0 {
+            //     continue;
+            // }
+            // if c.reference_height > 0.0 {
+            //     continue;
+            // }
+            // if c.reference_height > 2.0 * c.lbd as f64 {
+            //     continue;
+            // }
             let c = &mut self[cid];
             // c.update_reference_rate(asg.num_conflict);
             // Skip clauses that are unlikely to be improved by vivification.
@@ -68,6 +71,7 @@ impl VivifyIF for ClauseDB {
             // }
             // assert!(!c.is(FlagClause::ASSIGN_REASON));
             c.vivify_at = asg.num_conflict;
+            c.vivify_age += 1;
             let is_learnt = c.is(FlagClause::LEARNT);
             let lbd = c.lbd;
             let vivify_at = c.vivify_at;
@@ -82,7 +86,6 @@ impl VivifyIF for ClauseDB {
                 ));
                 to_display = num_check + display_step;
             }
-            num_check += 1;
             // debug_assert!(clits.iter().all(|l| !clits.contains(&!*l)));
             // Build a clean environment
             // debug_assert!(asg.stack_is_empty() || !asg.remains());
@@ -147,7 +150,6 @@ impl VivifyIF for ClauseDB {
                             }
                             match vec.len() {
                                 0 => {
-                                    state.flush("");
                                     state[Stat::VivifiedClause] += num_shrink;
                                     state[Stat::VivifiedVar] += num_assert;
                                     state.log(None, "RootLevelConflict By vivify");
@@ -162,7 +164,7 @@ impl VivifyIF for ClauseDB {
                                     if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new()
                                     {
                                         self[cid].born_at = born_at;
-                                        self[cid].reference_height = reference_height / 2;
+                                        self[cid].reference_height = reference_height;
                                         self[cid].vivify_at = vivify_at;
                                         self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
                                     }
diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs
index c4ed23d94..ccde3cb7e 100644
--- a/src/solver/conflict.rs
+++ b/src/solver/conflict.rs
@@ -146,11 +146,7 @@ pub fn handle_conflict(
                     }
                 }
                 for (lvl, ci) in cs.into_iter() {
-                    if cdb[ci].reference_height == 0 {
-                        cdb[ci].reference_height = lvl;
-                    } else {
-                        cdb[ci].reference_height = cdb[ci].reference_height.min(lvl);
-                    }
+                    cdb[ci].reference_height = cdb[ci].reference_height.min(lvl);
                 }
             }
             AssignReason::Decision(_) => (),
diff --git a/src/solver/search.rs b/src/solver/search.rs
index 5fe8e8e41..a556fb52c 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -76,7 +76,7 @@ impl SolveIF for Solver {
         #[cfg(feature = "clause_vivification")]
         {
             state.flush("vivifying...");
-            if cdb.vivify(asg, state, true).is_err() {
+            if cdb.vivify(asg, state).is_err() {
                 state.log(None, "By vivifier as a pre-possessor");
                 return Ok(Certificate::UNSAT);
             }
@@ -225,11 +225,11 @@ impl SolveIF for Solver {
 
 /// table of (RephaseTarget, span length, next index)
 const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 5] = [
-    (RephaseTarget::Polarity, 80, 1),
-    (RephaseTarget::False, 20, 2),
-    (RephaseTarget::True, 20, 3),
-    (RephaseTarget::Best, 20, 4),
-    (RephaseTarget::Walk, 80, 0),
+    (RephaseTarget::Polarity, 8, 1),
+    (RephaseTarget::False, 2, 2),
+    (RephaseTarget::True, 2, 3),
+    (RephaseTarget::Best, 2, 4),
+    (RephaseTarget::Walk, 8, 0),
 ];
 
 /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT.
@@ -244,14 +244,14 @@ fn search(
     let mut progress_pressure: usize = 0;
     let progress_interval: usize = 10_000;
     let mut reduction_pressure: usize = 0;
-    let reduction_interval: usize = 40_000;
+    let reduction_interval: usize = 80_000;
     let mut rephase_rotation_pressure: usize = 0;
     let mut vivification_pressure: usize = 0;
-    let vivification_interval: usize = 40_000;
+    let vivification_interval: usize = 20_000;
     let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0];
     let vmtf_interval: usize = 20;
     let mut assign_peak: usize = 0;
-    let luby_scale: usize = 80;
+    let luby_scale: usize = 32;
     let mut span_scale: usize = luby_scale;
 
     macro_rules! reduce {
@@ -410,7 +410,7 @@ fn search(
             // }
             if vivification_pressure >= vivification_interval {
                 if cfg!(feature = "clause_vivification") {
-                    cdb.vivify(asg, state, true)?;
+                    cdb.vivify(asg, state)?;
                 }
                 vivification_pressure = 0;
             }
diff --git a/src/types/clause.rs b/src/types/clause.rs
index 31a2317fd..7c33efa54 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -65,7 +65,7 @@ impl Default for Clause {
             referred: 0,
             referred_at: 0,
             born_at: 0,
-            reference_height: 0,
+            reference_height: DecisionLevel::MAX,
             vivify_age: 0,
             vivify_at: 0,
             lbd: DecisionLevel::MAX,
@@ -229,9 +229,6 @@ impl ClauseIF for Clause {
         self.referred += 1;
         self.referred_at = asg.current_conflict_index();
         let level = asg.decision_level();
-        if self.reference_height == 0 {
-            self.reference_height = level;
-        }
         self.reference_height = self.reference_height.min(level);
     }
 }

From 50902447399416ee79942c98e2b9aebbea58233a Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 13 Jul 2026 13:35:56 +0900
Subject: [PATCH 23/26] chore: clean up

---
 src/cdb/db.rs     | 38 ++++----------------------------------
 src/cdb/vivify.rs | 15 ---------------
 2 files changed, 4 insertions(+), 49 deletions(-)

diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index edb0673a4..94ae93508 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -67,7 +67,6 @@ pub struct ClauseDB {
     pub(crate) tier1_clauses: Ema,
     /// the ratio of pretty good learnt clauses
     pub(crate) tier2_clauses: Ema,
-    // pub(crate) last_reduction_count: usize,
 }
 
 impl Default for ClauseDB {
@@ -90,7 +89,6 @@ impl Default for ClauseDB {
             num_reregistration: 0,
             tier1_clauses: Ema::default(),
             tier2_clauses: Ema::default(),
-            // last_reduction_count: 0,
         }
     }
 }
@@ -832,17 +830,13 @@ impl ClauseDBIF for ClauseDB {
     }
     /// reduce the number of 'learnt' or *removable* clauses.
     fn reduce(&mut self, asg: &impl AssignIF, state: &State) {
-        macro_rules! _height {
+        macro_rules! height {
             ($c: expr) => {
-                // $c.reference_height as f64
-                ($c.reference_height + ($c.lbd as f64)) as f64
+                $c.reference_height + $c.lbd
             };
         }
         let conflict_index: usize = asg.current_conflict_index();
-        let _distance: DecisionLevel =
-            2 + (state.c_lvl.get_slow() - state.b_lvl.get_slow()) as DecisionLevel;
-        let _height: f64 = state.b_lvl.get_slow();
-        let udist: DecisionLevel =
+        let effective_height: DecisionLevel =
             (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel;
         self.num_reduction += 1;
         let ClauseDB {
@@ -857,24 +851,10 @@ impl ClauseDBIF for ClauseDB {
             freelist,
             ..
         } = self;
-        // let depth: f64 = 6.0 + state.b_lvl.get_slow().log2();
-        // let (total, targets) = clause
-        //     .iter()
-        //     .skip(1)
-        //     .filter(|c| {
-        //         !c.is_dead() && c.is(FlagClause::LEARNT) && !c.is(FlagClause::ASSIGN_REASON)
-        //     })
-        //     .fold((0, 0), |(total, target), c| {
-        //         (total + 1, target + (height!(c) <= depth) as usize)
-        //     });
-        // if targets as f64 > 0.5 * total as f64 {
-        //     return;
-        // }
         *num_lbd2 = 0;
         let mut num_alives: usize = 0;
         let mut ntier1: usize = 0;
         let mut ntier2: usize = 0;
-        // let mut survived: usize = 0;
         for (i, c) in clause
             .iter_mut()
             .enumerate()
@@ -895,9 +875,7 @@ impl ClauseDBIF for ClauseDB {
             }
             // Don't introduce any length-based crteria!
             // Clause lengths without context make result worse.
-            if c.reference_height + c.lbd <= udist
-            // height!(c) <= height
-            //     && c.lbd <= distance
+            if height!(c) <= effective_height
                 && (c.reference_height <= 4 || (conflict_index - c.referred_at) <= 800_000)
             {
                 match c.lbd {
@@ -905,13 +883,6 @@ impl ClauseDBIF for ClauseDB {
                     3..=6 => ntier1 += 1,
                     _ => ntier2 += 1,
                 }
-                // c.reference_height *= 1.1;
-                // c.reference_height += 1.0;
-                // c.reference_height += c.lbd as f64;
-                // if targets >= 20_000 {
-                //     c.reference_height += (c.lbd as f64).log2();
-                // }
-                // survived += 1;
                 continue;
             }
             remove_clause_fn(
@@ -926,7 +897,6 @@ impl ClauseDBIF for ClauseDB {
             );
             freelist.push(ClauseId::from(i));
         }
-        // self.last_reduction_count = survived;
         self.tier1_clauses.update(ntier1 as f64 / num_alives as f64);
         self.tier2_clauses.update(ntier2 as f64 / num_alives as f64);
     }
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 56b6c6b2e..1a8ccb154 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -47,15 +47,6 @@ impl VivifyIF for ClauseDB {
                 continue;
             }
             num_check += 1;
-            // if !num_check.is_multiple_of(db_skip) && c.reference_height > 0.0 {
-            //     continue;
-            // }
-            // if c.reference_height > 0.0 {
-            //     continue;
-            // }
-            // if c.reference_height > 2.0 * c.lbd as f64 {
-            //     continue;
-            // }
             let c = &mut self[cid];
             // c.update_reference_rate(asg.num_conflict);
             // Skip clauses that are unlikely to be improved by vivification.
@@ -63,12 +54,6 @@ impl VivifyIF for ClauseDB {
             // that are not too short and have a moderate LBD; outside this band
             // the success rate collapses, so skipping them saves work without
             // losing many improvable clauses.
-            // if 6 < c.lbd {
-            //     continue;
-            // }
-            // if c.vivify_age > 6 {
-            //     continue;
-            // }
             // assert!(!c.is(FlagClause::ASSIGN_REASON));
             c.vivify_at = asg.num_conflict;
             c.vivify_age += 1;

From 8c086eb817777858efc9aabfbb8e8ab1100d15b5 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 13 Jul 2026 13:39:01 +0900
Subject: [PATCH 24/26] chore: cargo clippy (1.97.0)

---
 src/assign/propagate.rs | 2 +-
 src/assign/stack.rs     | 2 +-
 src/bin/dmcr.rs         | 6 +++---
 src/solver/conflict.rs  | 2 +-
 src/state.rs            | 2 +-
 5 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs
index 728b5859c..d6d1a772a 100644
--- a/src/assign/propagate.rs
+++ b/src/assign/propagate.rs
@@ -206,7 +206,7 @@ impl PropagateIF for AssignStack {
                 self.var[l.vi()].assign.is_some(),
                 "cancel_until found unassigned var in trail {}{:?}",
                 l.vi(),
-                &self.var[l.vi()],
+                self.var[l.vi()],
             );
             let vi = l.vi();
             #[cfg(feature = "trace_propagation")]
diff --git a/src/assign/stack.rs b/src/assign/stack.rs
index bfadaf97b..a98e9e31b 100644
--- a/src/assign/stack.rs
+++ b/src/assign/stack.rs
@@ -390,7 +390,7 @@ impl fmt::Display for AssignStack {
                 f,
                 "ASG:: trail({}):[(0, {:?})]\n      level: {}, asserted: {}, eliminated: {}",
                 self.trail.len(),
-                &v,
+                v,
                 levels,
                 self.num_asserted_vars,
                 self.num_eliminated_vars,
diff --git a/src/bin/dmcr.rs b/src/bin/dmcr.rs
index 2ec7add04..45556ce5d 100644
--- a/src/bin/dmcr.rs
+++ b/src/bin/dmcr.rs
@@ -198,14 +198,14 @@ fn main() {
         None if from_file => println!(
             "{}A valid assignment set for {}{} is found in {}",
             green,
-            &args.problem.to_str().unwrap(),
+            args.problem.to_str().unwrap(),
             RESET,
-            &args.assign.unwrap().to_str().unwrap(),
+            args.assign.unwrap().to_str().unwrap(),
         ),
         None => println!(
             "{}A valid assignment set for {}.{}",
             green,
-            &args.problem.to_str().unwrap(),
+            args.problem.to_str().unwrap(),
             RESET,
         ),
     }
diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs
index ccde3cb7e..a7e04b5c2 100644
--- a/src/solver/conflict.rs
+++ b/src/solver/conflict.rs
@@ -618,7 +618,7 @@ fn lit_level(
                 cdb[cid].lit0(),
                 lit,
                 cid,
-                &cdb[cid]
+                cdb[cid]
             );
             // assert!(
             //     !bag.contains(&lit),
diff --git a/src/state.rs b/src/state.rs
index d6947bc43..4be79afaa 100644
--- a/src/state.rs
+++ b/src/state.rs
@@ -878,7 +878,7 @@ impl fmt::Display for State {
         if width < vclen + fnlen + 1 {
             write!(f, "{fname:<width$} |time:{tm:>9.2}")
         } else {
-            write!(f, "{fname}{:>w$} |time:{tm:>9.2}", &vc, w = width - fnlen,)
+            write!(f, "{fname}{:>w$} |time:{tm:>9.2}", vc, w = width - fnlen,)
         }
     }
 }

From b37e0cc09535dfa1ffc5c2cf828a9f1ccf7bd097 Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Mon, 13 Jul 2026 19:48:13 +0900
Subject: [PATCH 25/26] set `vivify_age` for the shortened clauses; remove
 `born_at` and `referred` from `Clause`

---
 src/cdb/db.rs              | 1 -
 src/cdb/vivify.rs          | 6 +++---
 src/processor/eliminate.rs | 1 -
 src/solver/search.rs       | 1 -
 src/types/clause.rs        | 8 +-------
 5 files changed, 4 insertions(+), 13 deletions(-)

diff --git a/src/cdb/db.rs b/src/cdb/db.rs
index 94ae93508..2934c155a 100644
--- a/src/cdb/db.rs
+++ b/src/cdb/db.rs
@@ -333,7 +333,6 @@ impl ClauseDBIF for ClauseDB {
         let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
         c.search_from = 2;
         c.lbd = DecisionLevel::MAX;
-        c.born_at = 0;
         c.vivify_age = 0;
         c.vivify_at = 0;
         c.reference_height = DecisionLevel::MAX;
diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index 1a8ccb154..e95aaec8e 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -41,7 +41,7 @@ impl VivifyIF for ClauseDB {
                 continue;
             }
             let span: usize = 10_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1);
-            if c.vivify_at.max(c.born_at) + span > asg.num_conflict
+            if c.vivify_at + span > asg.num_conflict
                 || (c.referred_at <= c.vivify_at && (c.is(FlagClause::LEARNT) || c.vivify_age != 0))
             {
                 continue;
@@ -57,11 +57,11 @@ impl VivifyIF for ClauseDB {
             // assert!(!c.is(FlagClause::ASSIGN_REASON));
             c.vivify_at = asg.num_conflict;
             c.vivify_age += 1;
+            let vivify_age = c.vivify_age;
             let is_learnt = c.is(FlagClause::LEARNT);
             let lbd = c.lbd;
             let vivify_at = c.vivify_at;
             c.vivify_age += 1;
-            let born_at = c.born_at;
             let reference_height = c.reference_height;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
             if to_display <= num_check {
@@ -148,9 +148,9 @@ impl VivifyIF for ClauseDB {
                                 _ => {
                                     if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new()
                                     {
-                                        self[cid].born_at = born_at;
                                         self[cid].reference_height = reference_height;
                                         self[cid].vivify_at = vivify_at;
+                                        self[cid].vivify_age = vivify_age;
                                         self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
                                     }
                                     self.remove_clause(cid);
diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs
index fb635cc7a..180018831 100644
--- a/src/processor/eliminate.rs
+++ b/src/processor/eliminate.rs
@@ -94,7 +94,6 @@ pub fn eliminate_var(
                         RefClause::Clause(ci) => {
                             // the merged clause might be a duplicated clause.
                             elim.add_cid_occur(asg, ci, &mut cdb[ci], true);
-                            cdb[ci].born_at = cdb[*p].born_at.max(cdb[*n].born_at);
                             cdb[ci].reference_height =
                                 cdb[*p].reference_height.min(cdb[*n].reference_height);
                             cdb[ci].lbd = cdb[*p].lbd.max(cdb[*n].lbd);
diff --git a/src/solver/search.rs b/src/solver/search.rs
index a556fb52c..8e444f26a 100644
--- a/src/solver/search.rs
+++ b/src/solver/search.rs
@@ -357,7 +357,6 @@ fn search(
         } else {
             cdb.lbd.update(lbd as f64);
             cdb[cid].lbd = DecisionLevel::MAX;
-            cdb[cid].born_at = asg.num_conflict;
         }
         match asg.stack_len().cmp(&assign_peak) {
             Ordering::Less => {}
diff --git a/src/types/clause.rs b/src/types/clause.rs
index 7c33efa54..194cb8da3 100644
--- a/src/types/clause.rs
+++ b/src/types/clause.rs
@@ -17,11 +17,8 @@ pub struct Clause {
     /// the index from which `propagate` starts searching an un-falsified literal.
     /// Since it's just a hint, we don't need u32 or usize.
     pub search_from: u16,
-    /// The number of referrences in conflict analysis
-    pub(crate) referred: usize,
+    /// The last reference time in conflict analysis
     pub(crate) referred_at: usize,
-    /// Sum of activated (used as propagated) duration
-    pub(crate) born_at: usize,
     /// The minimal decision level at which a conflict occured by this clause
     pub(crate) reference_height: DecisionLevel,
     /// last vivified time in conflicts
@@ -62,9 +59,7 @@ impl Default for Clause {
             lits: vec![],
             flags: FlagClause::empty(),
             search_from: 2,
-            referred: 0,
             referred_at: 0,
-            born_at: 0,
             reference_height: DecisionLevel::MAX,
             vivify_age: 0,
             vivify_at: 0,
@@ -226,7 +221,6 @@ impl ClauseIF for Clause {
         unassigned == 1 && all_others_false
     }
     fn update_reference(&mut self, asg: &impl AssignIF) {
-        self.referred += 1;
         self.referred_at = asg.current_conflict_index();
         let level = asg.decision_level();
         self.reference_height = self.reference_height.min(level);

From ded83ff42ecb27ac86fc9f5ea0aa678011aa7c0e Mon Sep 17 00:00:00 2001
From: "Narazaki, Shuji" <shujinarazaki@protonmail.com>
Date: Tue, 14 Jul 2026 14:06:18 +0900
Subject: [PATCH 26/26] exp: set vivify_age of shortened clauses to zero

---
 src/cdb/vivify.rs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs
index e95aaec8e..05926995b 100644
--- a/src/cdb/vivify.rs
+++ b/src/cdb/vivify.rs
@@ -57,11 +57,9 @@ impl VivifyIF for ClauseDB {
             // assert!(!c.is(FlagClause::ASSIGN_REASON));
             c.vivify_at = asg.num_conflict;
             c.vivify_age += 1;
-            let vivify_age = c.vivify_age;
             let is_learnt = c.is(FlagClause::LEARNT);
             let lbd = c.lbd;
             let vivify_at = c.vivify_at;
-            c.vivify_age += 1;
             let reference_height = c.reference_height;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
             if to_display <= num_check {
@@ -150,7 +148,6 @@ impl VivifyIF for ClauseDB {
                                     {
                                         self[cid].reference_height = reference_height;
                                         self[cid].vivify_at = vivify_at;
-                                        self[cid].vivify_age = vivify_age;
                                         self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
                                     }
                                     self.remove_clause(cid);