Periodic Restart and Luby (based) Rephase Rotation 20260717

src/assign/propagate.rs

@@ -153,6 +153,8 @@ impl PropagateIF for AssignStack {
 
         self.var[vi].level = lv;
         self.var[vi].reason = reason;
+        self.var[vi].polarity *= 0.999;
+        self.var[vi].polarity += 0.001 * if l.as_bool() { 1.0 } else { -1.0 };
         self.reward_at_assign(vi);
         debug_assert!(!self.trail.contains(&l));
         debug_assert!(!self.trail.contains(&!l));
@@ -237,8 +239,6 @@ impl PropagateIF for AssignStack {
                 if cfg!(feature = "rephase")
                 // && self.num_conflict - v.last_conflict <= 1000
                 {
-                    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 {

src/cdb/db.rs

@@ -333,9 +333,10 @@ impl ClauseDBIF for ClauseDB {
         let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize];
         c.search_from = 2;
         c.lbd = DecisionLevel::MAX;
+        c.referred = 0;
+        // c.referred_at = 0;
         c.vivify_age = 0;
         c.vivify_at = 0;
-        c.reference_height = DecisionLevel::MAX;
         let len2 = c.lits.len() == 2;
         *num_clause += 1;
         if learnt {
@@ -828,15 +829,12 @@ impl ClauseDBIF for ClauseDB {
         c.is(FlagClause::LEARNT)
     }
     /// reduce the number of 'learnt' or *removable* clauses.
-    fn reduce(&mut self, asg: &impl AssignIF, state: &State) {
-        macro_rules! height {
+    fn reduce(&mut self, _asg: &impl AssignIF, _state: &State) {
+        macro_rules! _height {
             ($c: expr) => {
                 $c.reference_height + $c.lbd
             };
         }
-        let conflict_index: usize = asg.current_conflict_index();
-        let effective_height: DecisionLevel =
-            (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel;
         self.num_reduction += 1;
         let ClauseDB {
             clause,
@@ -874,9 +872,12 @@ impl ClauseDBIF for ClauseDB {
             }
             // Don't introduce any length-based crteria!
             // Clause lengths without context make result worse.
-            if height!(c) <= effective_height
-                && (c.reference_height <= 4 || (conflict_index - c.referred_at) <= 800_000)
-            {
+            if c.lbd <= 8 && c.referred > 0 || c.referred >= 16 {
+                if c.lbd <= 4 {
+                    c.referred -= 1;
+                } else {
+                    c.referred /= 2;
+                }
                 match c.lbd {
                     0..=2 => *num_lbd2 += 1,
                     3..=6 => ntier1 += 1,

src/cdb/vivify.rs

@@ -59,8 +59,10 @@ impl VivifyIF for ClauseDB {
             c.vivify_age += 1;
             let is_learnt = c.is(FlagClause::LEARNT);
             let lbd = c.lbd;
+            let referred = c.referred;
+            let referred_at = c.referred_at;
+            let vivify_age = c.vivify_age;
             let vivify_at = c.vivify_at;
-            let reference_height = c.reference_height;
             let clits = c.iter().copied().collect::<Vec<Lit>>();
             if to_display <= num_check {
                 state.flush("");
@@ -146,9 +148,11 @@ impl VivifyIF for ClauseDB {
                                 _ => {
                                     if let Some(cid) = self.new_clause(&mut vec, is_learnt).is_new()
                                     {
-                                        self[cid].reference_height = reference_height;
-                                        self[cid].vivify_at = vivify_at;
                                         self[cid].lbd = lbd.min(decisions.len() as DecisionLevel);
+                                        self[cid].referred = referred;
+                                        self[cid].referred_at = referred_at;
+                                        self[cid].vivify_age = vivify_age;
+                                        self[cid].vivify_at = vivify_at;
                                     }
                                     self.remove_clause(cid);
                                     num_shrink += 1;

src/processor/eliminate.rs

@@ -94,9 +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].reference_height =
-                                cdb[*p].reference_height.min(cdb[*n].reference_height);
                             cdb[ci].lbd = cdb[*p].lbd.max(cdb[*n].lbd);
+                            cdb[ci].referred = cdb[*p].referred + cdb[*n].referred;
+                            cdb[ci].referred_at = cdb[*p].referred_at.max(cdb[*n].referred_at);
+                            cdb[ci].vivify_age = cdb[*p].vivify_age.min(cdb[*n].vivify_age);
+                            cdb[ci].vivify_at = cdb[*p].vivify_at.max(cdb[*n].vivify_at);
 
                             #[cfg(feature = "trace_elimination")]
                             println!(

src/solver/conflict.rs

@@ -142,11 +142,11 @@ pub fn handle_conflict(
                         bumped.push(vi);
                     }
                     if let AssignReason::Implication(ci) = asg.reason(l.vi()) {
-                        cs.push((asg.level(l.vi()), ci));
+                        cs.push(ci);
                     }
                 }
-                for (lvl, ci) in cs.into_iter() {
-                    cdb[ci].reference_height = cdb[ci].reference_height.min(lvl);
+                for ci in cs.into_iter() {
+                    cdb[ci].update_reference(asg);
                 }
             }
             AssignReason::Decision(_) => (),
@@ -429,9 +429,6 @@ fn conflict_analyze(
                     }
                 }
                 cdb[cid].update_reference(asg);
-                cdb[cid].lbd = cdb[cid]
-                    .lbd
-                    .min(asg.literal_block_distance_current(&cdb[cid].lits));
             }
             AssignReason::Decision(_) | AssignReason::None => {}
         }

src/solver/search.rs

@@ -223,88 +223,26 @@ impl SolveIF for Solver {
     }
 }
 
-/// table of (RephaseTarget, span length, next index)
-const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 5] = [
-    (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.
 fn search(
     asg: &mut AssignStack,
     cdb: &mut ClauseDB,
     state: &mut State,
 ) -> Result<bool, SolverError> {
+    let mut rng: SplitMix64 = SplitMix64::new(state.cnf.num_of_variables as u64);
     let mut span_len: usize = 1;
-    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 = 80_000;
-    let mut rephase_rotation_pressure: usize = 0;
-    let mut vivification_pressure: usize = 0;
-    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 = 32;
-    let mut span_scale: usize = luby_scale;
+    let luby_scale: usize = 2048 * 4;
 
     macro_rules! reduce {
-        () => {{
+        () => {
             state.search_mode_ratio.0.update(0.0);
             state.search_mode_ratio.1.update(0.0);
             reduction_pressure = 0;
             cdb.reduce(asg, state);
-        }};
-    }
-    macro_rules! to_lrb {
-        () => {
-            if asg.activity_scheme != VarActivityScheme::LRB {
-                asg.activity_scheme = VarActivityScheme::LRB;
-                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];
-            asg.phase_mode = current_phase.0;
-            rephase_rotation_pressure = 0;
-        };
-    }
-    macro_rules! to_vmtf {
-        () => {
-            if asg.activity_scheme != VarActivityScheme::VMTF {
-                asg.activity_scheme = VarActivityScheme::VMTF;
-                asg.phase_mode = RephaseTarget::Walk;
-                asg.set_learning_rate(0.0); // Don't change this
-                asg.rebuild_order();
-                rephase_rotation_pressure = 0;
-            }
-        };
-    }
-    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 {
-            //     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 {
@@ -313,15 +251,15 @@ fn search(
             if let Some(core) = asg.check_best_phases() {
                 assign_peak = assign_peak.saturating_sub(2 * $n);
                 state.core_size = core;
-                to_vmtf!();
+                // to_vmtf!();
             } else {
                 assign_peak = 0;
-                let pre = state.core_size;
+                // let pre = state.core_size;
                 state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar);
                 cdb.save_best_assign_reasons(asg, true);
-                if pre < state.core_size {
-                    to_vmtf!();
-                }
+                // if pre < state.core_size {
+                //     to_vmtf!();
+                // }
             }
         };
     }
@@ -356,7 +294,8 @@ fn search(
             update_core!(1);
         } else {
             cdb.lbd.update(lbd as f64);
-            cdb[cid].lbd = DecisionLevel::MAX;
+            cdb[cid].lbd = lbd;
+            cdb[cid].referred_at = asg.current_conflict_index();
         }
         match asg.stack_len().cmp(&assign_peak) {
             Ordering::Less => {}
@@ -389,71 +328,82 @@ fn search(
                 // }
             }
         }
-        elimination_pressure += 1;
         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 {
+        if reduction_pressure >= 4 * luby_scale {
+            RESTART!(asg, cdb, state)?;
             reduce!();
+            if cfg!(feature = "clause_vivification") {
+                cdb.vivify(asg, state)?;
+            }
+            if cfg!(feature = "clause_elimination") {
+                let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
+                state.flush("clause subsumption, ");
+                elim.simplify(asg, cdb, state, false)?;
+                asg.eliminated.append(elim.eliminated_lits());
+            }
         }
-        if state.span_manager.span_ended(span_len / span_scale) {
+
+        if state.span_manager.span_ended(span_len / luby_scale) {
             span_len = 0;
             let new_segment = state.span_manager.prepare_new_span(span_len);
             dump_stage(asg, state, new_segment);
-            RESTART!(asg, cdb, state)?;
-            // if reduction_pressure > reduction_interval {
-            //     reduce!();
-            // }
-            if vivification_pressure >= vivification_interval {
-                if cfg!(feature = "clause_vivification") {
-                    cdb.vivify(asg, state)?;
-                }
-                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, ");
-                    elim.simplify(asg, cdb, state, false)?;
-                    asg.eliminated.append(elim.eliminated_lits());
-                }
-                elimination_pressure = 0;
-            }
+            let _conflict_index = asg.current_conflict_index();
             if cfg!(feature = "rephase") {
-                match asg.activity_scheme {
-                    VarActivityScheme::LRB
-                        if rephase_rotation_pressure >= current_phase.1 * span_scale =>
-                    {
-                        rotate_rephase_mode!();
+                match rng.next_f64() {
+                    0.0..0.25 => {
+                        asg.phase_mode = RephaseTarget::Walk;
+                    }
+                    0.25..0.45 => {
+                        asg.phase_mode = RephaseTarget::Best;
                     }
-                    VarActivityScheme::VMTF
-                        if rephase_rotation_pressure >= vmtf_interval * span_scale =>
-                    {
-                        to_lrb!();
+                    0.45..0.6 => {
+                        asg.phase_mode = RephaseTarget::Polarity;
+                    }
+                    0.6..0.75 => {
+                        asg.phase_mode = RephaseTarget::False;
+                    }
+                    0.75..0.9 => {
+                        asg.phase_mode = RephaseTarget::True;
+                    }
+                    0.9..1.0 => {
+                        asg.phase_mode = RephaseTarget::Random;
+                    }
+                    // 0.95..1.0 => {
+                    //     asg.phase_mode = RephaseTarget::Inverted;
+                    // }
+                    _ => {
+                        asg.phase_mode = RephaseTarget::Walk;
+                    }
+                }
+                match rng.next_f64() {
+                    0.0..0.2 if asg.activity_scheme != VarActivityScheme::VMTF => {
+                        asg.activity_scheme = VarActivityScheme::VMTF;
+                        // asg.set_learning_rate(adaptive_lr);
+                        // asg.set_learning_rate(0.0);
+                        asg.rebuild_order();
+                    }
+                    0.2..1.0 if asg.activity_scheme != VarActivityScheme::LRB => {
+                        asg.activity_scheme = VarActivityScheme::LRB;
+                        // Adapt LRB learning rate to the upcoming Luby envelope height:
+                        // asg.set_learning_rate(adaptive_lr);
+                        asg.rebuild_order();
                     }
                     _ => (),
                 }
             }
+            // span_scale = luby_scale * state.span_manager.current_span();
             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),
-                // longer spans  → lower  α (stable estimates over more conflicts).
-                let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64;
-                let adaptive_lr: f64 = 1.0 / span.sqrt();
+                let span_scale = luby_scale * state.span_manager.envelop_index();
+                let adaptive_lr = 1.0 / (span_scale as f64).sqrt();
                 asg.set_learning_rate(adaptive_lr);
-            } else {
-                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);

src/solver/stage.rs

@@ -79,7 +79,7 @@ impl StageManager {
     pub fn envelop_index(&self) -> usize {
         self.envelope_hight
     }
-    /// returns the scaling factor used in the current span
+    /// returns the current segment length
     pub fn current_segment_length(&self) -> usize {
         self.luby_iter.segment_len() as usize
     }