From ac8afb6b351609a18f24027dae95a50bb8164b45 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Wed, 15 Jul 2026 23:12:30 +0900 Subject: [PATCH 01/14] fix: capsulate lbd calculation and reference_height calculation into `update_reference` --- src/solver/conflict.rs | 9 +++------ src/types/clause.rs | 5 +++-- 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index a7e04b5c2..69b77e6d9 100644 --- a/src/solver/conflict.rs +++ b/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 => {} } diff --git a/src/types/clause.rs b/src/types/clause.rs index 194cb8da3..17f3a1d69 100644 --- a/src/types/clause.rs +++ b/src/types/clause.rs @@ -50,7 +50,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, asg: &impl AssignIF); + fn update_reference(&mut self, asg: &mut impl AssignIF); } impl Default for Clause { @@ -220,9 +220,10 @@ impl ClauseIF for Clause { .all(|l| asg.assigned(*l) == Some(false)); unassigned == 1 && all_others_false } - fn update_reference(&mut self, asg: &impl AssignIF) { + fn update_reference(&mut self, asg: &mut impl AssignIF) { self.referred_at = asg.current_conflict_index(); let level = asg.decision_level(); + self.lbd = self.lbd.min(asg.literal_block_distance_current(&self.lits)); self.reference_height = self.reference_height.min(level); } } From 1e19ebee383c9cac8c42926b9d0fee93f04f0548 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 17 Jul 2026 08:41:59 +0900 Subject: [PATCH 02/14] chore: open PR From 2bdaf922d3beb1b2609c5a6bed7c4d0bec3ecae4 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 17 Jul 2026 08:53:50 +0900 Subject: [PATCH 03/14] exp: a snapshot --- src/cdb/db.rs | 22 +++-- src/solver/search.rs | 198 ++++++++++++++++++++++++++++--------------- src/solver/stage.rs | 2 +- 3 files changed, 147 insertions(+), 75 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 2934c155a..8e333faa7 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -829,14 +829,21 @@ 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 + $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; + // let effective_height: DecisionLevel = 12 as DecisionLevel; + // let effective_height: DecisionLevel = + // (state.span_manager.current_segment_length() + 6) as DecisionLevel; + // let effective_height: DecisionLevel = (state.span_manager.current_segment_length() as f64 + // + state.c_lvl.get_slow().log2()) + // as DecisionLevel; + // let effective_height: DecisionLevel = + // (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel; + let _ffective_height: DecisionLevel = state.b_lvl.get_slow() as DecisionLevel; self.num_reduction += 1; let ClauseDB { clause, @@ -874,8 +881,13 @@ 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 height!(c) <= effective_height && (conflict_index - c.referred_at) <= 8_000 + if (c.lbd <= 2 && conflict_index - c.referred_at <= 16_384) + || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) + || (c.reference_height <= 10 && conflict_index - c.referred_at <= 1024) + || c.len() <= 4 + || (c.lbd <= 4 && c.vivify_age == 0) + // 160_000 / c.len().ilog2() as usize { match c.lbd { 0..=2 => *num_lbd2 += 1, diff --git a/src/solver/search.rs b/src/solver/search.rs index 8e444f26a..5a1085d73 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -224,12 +224,39 @@ impl SolveIF for Solver { } /// table of (RephaseTarget, span length, next index) -const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 5] = [ +const REPHASE_ROTATION: [(RephaseTarget, usize); 5] = [ + (RephaseTarget::Polarity, 1), + (RephaseTarget::False, 2), + (RephaseTarget::True, 3), + (RephaseTarget::Best, 4), + (RephaseTarget::Walk, 0), +]; + +const ___REPHASE_ROTATION: [(RephaseTarget, usize, usize); 4] = [ (RephaseTarget::Polarity, 8, 1), (RephaseTarget::False, 2, 2), (RephaseTarget::True, 2, 3), - (RephaseTarget::Best, 2, 4), - (RephaseTarget::Walk, 8, 0), + (RephaseTarget::Best, 2, 0), +]; + +const __REPHASE_ROTATION: [(RephaseTarget, usize, usize); 7] = [ + (RephaseTarget::Polarity, 0, 1), + (RephaseTarget::False, 0, 2), + (RephaseTarget::Walk, 0, 3), + (RephaseTarget::True, 0, 4), + (RephaseTarget::Polarity, 0, 5), + (RephaseTarget::Best, 0, 6), + (RephaseTarget::Walk, 0, 0), +]; + +const _REPHASE_ROTATION: [(RephaseTarget, usize, usize); 7] = [ + (RephaseTarget::Walk, 0, 1), + (RephaseTarget::Walk, 0, 2), + (RephaseTarget::Walk, 0, 3), + (RephaseTarget::Walk, 0, 4), + (RephaseTarget::Walk, 0, 5), + (RephaseTarget::Walk, 0, 6), + (RephaseTarget::Walk, 0, 0), ]; /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT. @@ -244,25 +271,24 @@ fn search( 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 reduction_interval: usize = 10_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 vivification_interval: usize = 10_000; + let mut current_phase: &(RephaseTarget, usize) = &REPHASE_ROTATION[0]; let mut assign_peak: usize = 0; - let luby_scale: usize = 32; + let luby_scale: usize = 2048 * 8; let mut span_scale: usize = luby_scale; 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 { + macro_rules! _to_lrb { () => { if asg.activity_scheme != VarActivityScheme::LRB { asg.activity_scheme = VarActivityScheme::LRB; @@ -271,41 +297,32 @@ fn search( asg.set_learning_rate(adaptive_lr); asg.rebuild_order(); } - current_phase = &REPHASE_ROTATION[0]; - asg.phase_mode = current_phase.0; - rephase_rotation_pressure = 0; + // current_phase = &REPHASE_ROTATION[0]; + // asg.phase_mode = current_phase.0; }; } - macro_rules! to_vmtf { + macro_rules! _to_vmtf { () => { if asg.activity_scheme != VarActivityScheme::VMTF { asg.activity_scheme = VarActivityScheme::VMTF; - asg.phase_mode = RephaseTarget::Walk; + // 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; + () => {{ + // if current_phase.1 == 0 { + // if asg.activity_scheme == VarActivityScheme::VMTF { + // to_lrb!(); + // } else { + // to_vmtf!(); + // } // } - }; + current_phase = &REPHASE_ROTATION[current_phase.1]; + asg.phase_mode = current_phase.0; + }}; } macro_rules! update_core { ($n: expr) => { @@ -313,15 +330,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 +373,7 @@ fn search( update_core!(1); } else { cdb.lbd.update(lbd as f64); - cdb[cid].lbd = DecisionLevel::MAX; + cdb[cid].lbd = lbd; } match asg.stack_len().cmp(&assign_peak) { Ordering::Less => {} @@ -392,21 +409,13 @@ fn search( elimination_pressure += 1; progress_pressure += 1; reduction_pressure += 1; - rephase_rotation_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 { - 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); + if reduction_pressure >= luby_scale { RESTART!(asg, cdb, state)?; - // if reduction_pressure > reduction_interval { - // reduce!(); - // } + reduce!(); if vivification_pressure >= vivification_interval { if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; @@ -422,31 +431,82 @@ fn search( } elimination_pressure = 0; } + } + + if state.span_manager.span_ended(span_len / span_scale) { + span_len = 0; if cfg!(feature = "rephase") { - match asg.activity_scheme { - VarActivityScheme::LRB - if rephase_rotation_pressure >= current_phase.1 * span_scale => - { - rotate_rephase_mode!(); - } - VarActivityScheme::VMTF - if rephase_rotation_pressure >= vmtf_interval * span_scale => - { - to_lrb!(); - } - _ => (), + // rephase_rotation_pressure = 0; + rotate_rephase_mode!(); + if asg.activity_scheme == VarActivityScheme::VMTF { + 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(); + } else { + asg.activity_scheme = VarActivityScheme::VMTF; + // 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.set_learning_rate(0.0); + asg.rebuild_order(); } } + let new_segment = state.span_manager.prepare_new_span(span_len); + dump_stage(asg, state, new_segment); + let _conflict_index = asg.current_conflict_index(); + // for l in asg.stack_iter() { + // if let AssignReason::Implication(cid) = asg.reason(l.vi()) { + // cdb[cid].referred_at = conflict_index; + // } + // } + // if cfg!(feature = "rephase") && rephase_rotation_pressure >= 4096 { + // if state.span_manager.current_span() * luby_scale >= 4096 { + // asg.phase_mode = RephaseTarget::Walk; + // if asg.activity_scheme == VarActivityScheme::VMTF { + // 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(); + // } else { + // asg.activity_scheme = VarActivityScheme::VMTF; + // asg.set_learning_rate(0.0); + // asg.rebuild_order(); + // } + // } else { + // current_phase = &REPHASE_ROTATION[current_phase.1]; + // asg.phase_mode = current_phase.0; + // if asg.activity_scheme == VarActivityScheme::VMTF { + // 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(); + // } + // } + // rephase_rotation_pressure = 0; + // // rotate_rephase_mode!(); + // // match asg.activity_scheme { + // // VarActivityScheme::LRB => { + // // rotate_rephase_mode!(); + // // } + // // VarActivityScheme::VMTF => { + // // to_lrb!(); + // // } + // // } + // } 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(); - asg.set_learning_rate(adaptive_lr); - } else { - asg.rescale_learning_rate(0.9); + // 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); } } let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar); diff --git a/src/solver/stage.rs b/src/solver/stage.rs index b2c62aa23..d71a231fb 100644 --- a/src/solver/stage.rs +++ b/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 } From c4f8e9d9d46ff8d533aefb07f301b1c053ecb775 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 17 Jul 2026 19:42:12 +0900 Subject: [PATCH 04/14] feat: fixed-length restart and Luby-based rephasing/rewarding --- src/cdb/db.rs | 8 +++--- src/solver/search.rs | 64 ++++++++++++++++++++++++++++++++------------ src/state.rs | 4 +-- 3 files changed, 53 insertions(+), 23 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 8e333faa7..5b729e308 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -882,12 +882,12 @@ impl ClauseDBIF for ClauseDB { // Don't introduce any length-based crteria! // Clause lengths without context make result worse. // if height!(c) <= effective_height && (conflict_index - c.referred_at) <= 8_000 - if (c.lbd <= 2 && conflict_index - c.referred_at <= 16_384) + if (c.lbd <= 2 && conflict_index - c.referred_at <= 8 * 8192) + || (c.lbd <= 4 && conflict_index - c.referred_at <= 4 * 8192) || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) - || (c.reference_height <= 10 && conflict_index - c.referred_at <= 1024) || c.len() <= 4 - || (c.lbd <= 4 && c.vivify_age == 0) - // 160_000 / c.len().ilog2() as usize + || (c.vivify_age == 0 + && c.reference_height <= state.c_lvl.get_slow().powf(0.8) as DecisionLevel) { match c.lbd { 0..=2 => *num_lbd2 += 1, diff --git a/src/solver/search.rs b/src/solver/search.rs index 5a1085d73..928f38c7c 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -265,6 +265,7 @@ fn search( cdb: &mut ClauseDB, state: &mut State, ) -> Result { + 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; @@ -277,7 +278,7 @@ fn search( let vivification_interval: usize = 10_000; let mut current_phase: &(RephaseTarget, usize) = &REPHASE_ROTATION[0]; let mut assign_peak: usize = 0; - let luby_scale: usize = 2048 * 8; + let luby_scale: usize = 2048 * 4; let mut span_scale: usize = luby_scale; macro_rules! reduce { @@ -435,27 +436,56 @@ fn search( 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 _conflict_index = asg.current_conflict_index(); if cfg!(feature = "rephase") { // rephase_rotation_pressure = 0; rotate_rephase_mode!(); - if asg.activity_scheme == VarActivityScheme::VMTF { - 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(); - } else { - asg.activity_scheme = VarActivityScheme::VMTF; - // 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.set_learning_rate(0.0); - asg.rebuild_order(); + match rng.next_f64() { + 0.0..0.5 if state.span_manager.current_span() >= 256 => { + asg.phase_mode = RephaseTarget::Walk; + } + 0.5..1.0 if state.span_manager.current_span() >= 256 => { + asg.phase_mode = RephaseTarget::Polarity; + } + 0.0..0.4 => { + asg.phase_mode = RephaseTarget::Best; + } + 0.4..0.65 => { + asg.phase_mode = RephaseTarget::False; + } + 0.65..0.9 => { + asg.phase_mode = RephaseTarget::True; + } + 0.9..0.95 => { + 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; + // 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.set_learning_rate(0.0); + asg.rebuild_order(); + } + 0.2..1.0 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); + } + _ => (), } } - let new_segment = state.span_manager.prepare_new_span(span_len); - dump_stage(asg, state, new_segment); - let _conflict_index = asg.current_conflict_index(); // for l in asg.stack_iter() { // if let AssignReason::Implication(cid) = asg.reason(l.vi()) { // cdb[cid].referred_at = conflict_index; diff --git a/src/state.rs b/src/state.rs index 4be79afaa..d3d19113e 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().with_slow(80_000), - c_lvl: Ema2::default_extended().with_slow(80_000), + b_lvl: Ema2::default_extended(), + c_lvl: Ema2::default_extended(), bt_drift_average: Ema::default().with_span(1000), core_size: 0, last_restart: 0, From 3d4da889f747a9a45a68d47f076ce27acb7004a9 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 17 Jul 2026 19:46:13 +0900 Subject: [PATCH 05/14] chore: clean up --- src/cdb/db.rs | 10 ---- src/solver/search.rs | 132 +------------------------------------------ 2 files changed, 3 insertions(+), 139 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 5b729e308..eea61d331 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -835,15 +835,6 @@ impl ClauseDBIF for ClauseDB { }; } let conflict_index: usize = asg.current_conflict_index(); - // let effective_height: DecisionLevel = 12 as DecisionLevel; - // let effective_height: DecisionLevel = - // (state.span_manager.current_segment_length() + 6) as DecisionLevel; - // let effective_height: DecisionLevel = (state.span_manager.current_segment_length() as f64 - // + state.c_lvl.get_slow().log2()) - // as DecisionLevel; - // let effective_height: DecisionLevel = - // (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel; - let _ffective_height: DecisionLevel = state.b_lvl.get_slow() as DecisionLevel; self.num_reduction += 1; let ClauseDB { clause, @@ -881,7 +872,6 @@ impl ClauseDBIF for ClauseDB { } // Don't introduce any length-based crteria! // Clause lengths without context make result worse. - // if height!(c) <= effective_height && (conflict_index - c.referred_at) <= 8_000 if (c.lbd <= 2 && conflict_index - c.referred_at <= 8 * 8192) || (c.lbd <= 4 && conflict_index - c.referred_at <= 4 * 8192) || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) diff --git a/src/solver/search.rs b/src/solver/search.rs index 928f38c7c..aa75ef62e 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -223,42 +223,6 @@ impl SolveIF for Solver { } } -/// table of (RephaseTarget, span length, next index) -const REPHASE_ROTATION: [(RephaseTarget, usize); 5] = [ - (RephaseTarget::Polarity, 1), - (RephaseTarget::False, 2), - (RephaseTarget::True, 3), - (RephaseTarget::Best, 4), - (RephaseTarget::Walk, 0), -]; - -const ___REPHASE_ROTATION: [(RephaseTarget, usize, usize); 4] = [ - (RephaseTarget::Polarity, 8, 1), - (RephaseTarget::False, 2, 2), - (RephaseTarget::True, 2, 3), - (RephaseTarget::Best, 2, 0), -]; - -const __REPHASE_ROTATION: [(RephaseTarget, usize, usize); 7] = [ - (RephaseTarget::Polarity, 0, 1), - (RephaseTarget::False, 0, 2), - (RephaseTarget::Walk, 0, 3), - (RephaseTarget::True, 0, 4), - (RephaseTarget::Polarity, 0, 5), - (RephaseTarget::Best, 0, 6), - (RephaseTarget::Walk, 0, 0), -]; - -const _REPHASE_ROTATION: [(RephaseTarget, usize, usize); 7] = [ - (RephaseTarget::Walk, 0, 1), - (RephaseTarget::Walk, 0, 2), - (RephaseTarget::Walk, 0, 3), - (RephaseTarget::Walk, 0, 4), - (RephaseTarget::Walk, 0, 5), - (RephaseTarget::Walk, 0, 6), - (RephaseTarget::Walk, 0, 0), -]; - /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT. fn search( asg: &mut AssignStack, @@ -272,11 +236,8 @@ fn search( let mut progress_pressure: usize = 0; let progress_interval: usize = 10_000; let mut reduction_pressure: usize = 0; - // let reduction_interval: usize = 10_000; - // let mut rephase_rotation_pressure: usize = 0; let mut vivification_pressure: usize = 0; let vivification_interval: usize = 10_000; - let mut current_phase: &(RephaseTarget, usize) = &REPHASE_ROTATION[0]; let mut assign_peak: usize = 0; let luby_scale: usize = 2048 * 4; let mut span_scale: usize = luby_scale; @@ -289,42 +250,6 @@ fn search( 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; - }; - } - 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(); - } - }; - } - macro_rules! rotate_rephase_mode { - () => {{ - // if current_phase.1 == 0 { - // if asg.activity_scheme == VarActivityScheme::VMTF { - // to_lrb!(); - // } else { - // to_vmtf!(); - // } - // } - current_phase = &REPHASE_ROTATION[current_phase.1]; - asg.phase_mode = current_phase.0; - }}; - } macro_rules! update_core { ($n: expr) => { asg.clear_asserted_literals(cdb)?; @@ -410,10 +335,8 @@ 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 >= luby_scale { RESTART!(asg, cdb, state)?; reduce!(); @@ -440,8 +363,6 @@ fn search( dump_stage(asg, state, new_segment); let _conflict_index = asg.current_conflict_index(); if cfg!(feature = "rephase") { - // rephase_rotation_pressure = 0; - rotate_rephase_mode!(); match rng.next_f64() { 0.0..0.5 if state.span_manager.current_span() >= 256 => { asg.phase_mode = RephaseTarget::Walk; @@ -478,6 +399,9 @@ fn search( asg.rebuild_order(); } 0.2..1.0 if asg.activity_scheme != VarActivityScheme::LRB => { + // 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). 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(); @@ -486,64 +410,14 @@ fn search( _ => (), } } - // for l in asg.stack_iter() { - // if let AssignReason::Implication(cid) = asg.reason(l.vi()) { - // cdb[cid].referred_at = conflict_index; - // } - // } - // if cfg!(feature = "rephase") && rephase_rotation_pressure >= 4096 { - // if state.span_manager.current_span() * luby_scale >= 4096 { - // asg.phase_mode = RephaseTarget::Walk; - // if asg.activity_scheme == VarActivityScheme::VMTF { - // 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(); - // } else { - // asg.activity_scheme = VarActivityScheme::VMTF; - // asg.set_learning_rate(0.0); - // asg.rebuild_order(); - // } - // } else { - // current_phase = &REPHASE_ROTATION[current_phase.1]; - // asg.phase_mode = current_phase.0; - // if asg.activity_scheme == VarActivityScheme::VMTF { - // 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(); - // } - // } - // rephase_rotation_pressure = 0; - // // rotate_rephase_mode!(); - // // match asg.activity_scheme { - // // VarActivityScheme::LRB => { - // // rotate_rephase_mode!(); - // // } - // // VarActivityScheme::VMTF => { - // // to_lrb!(); - // // } - // // } - // } 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(); - // 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); From bd88a19143a90566913394d833cf352ae9e1f212 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 18 Jul 2026 09:10:26 +0900 Subject: [PATCH 06/14] fix: fix learning_rate, rebuild_order; tweak one of reduction thresholds --- src/cdb/db.rs | 2 +- src/solver/search.rs | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index eea61d331..e49876097 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -877,7 +877,7 @@ impl ClauseDBIF for ClauseDB { || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) || c.len() <= 4 || (c.vivify_age == 0 - && c.reference_height <= state.c_lvl.get_slow().powf(0.8) as DecisionLevel) + && c.reference_height <= state.c_lvl.get_slow().powf(0.75) as DecisionLevel) { match c.lbd { 0..=2 => *num_lbd2 += 1, diff --git a/src/solver/search.rs b/src/solver/search.rs index aa75ef62e..b543030f0 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -241,6 +241,7 @@ fn search( let mut assign_peak: usize = 0; let luby_scale: usize = 2048 * 4; let mut span_scale: usize = luby_scale; + let adaptive_lr: f64 = 1.0 / (luby_scale as f64).sqrt(); macro_rules! reduce { () => { @@ -392,8 +393,6 @@ fn search( match rng.next_f64() { 0.0..0.2 if asg.activity_scheme != VarActivityScheme::VMTF => { asg.activity_scheme = VarActivityScheme::VMTF; - // 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.set_learning_rate(0.0); asg.rebuild_order(); @@ -403,9 +402,8 @@ fn search( // shorter spans → higher α (fast learning before the next restart), // longer spans → lower α (stable estimates over more conflicts). 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(); } _ => (), } From c2f61e8efc6bbdda4f39100f9ff147dc7b0ed362 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 18 Jul 2026 15:53:43 +0900 Subject: [PATCH 07/14] exp: refine reduction condition --- src/cdb/db.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index e49876097..0d647f066 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -876,8 +876,8 @@ impl ClauseDBIF for ClauseDB { || (c.lbd <= 4 && conflict_index - c.referred_at <= 4 * 8192) || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) || c.len() <= 4 - || (c.vivify_age == 0 - && c.reference_height <= state.c_lvl.get_slow().powf(0.75) as DecisionLevel) + || (c.vivify_age <= 4 + && c.reference_height <= state.c_lvl.get_slow().powf(0.5) as DecisionLevel) { match c.lbd { 0..=2 => *num_lbd2 += 1, From 2a4928b8e1cb692b0dfcd9bc3d5ec956b7313068 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 18 Jul 2026 17:57:07 +0900 Subject: [PATCH 08/14] Revert "exp: refine reduction condition" This reverts commit c2f61e8efc6bbdda4f39100f9ff147dc7b0ed362. --- src/cdb/db.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 0d647f066..e49876097 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -876,8 +876,8 @@ impl ClauseDBIF for ClauseDB { || (c.lbd <= 4 && conflict_index - c.referred_at <= 4 * 8192) || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) || c.len() <= 4 - || (c.vivify_age <= 4 - && c.reference_height <= state.c_lvl.get_slow().powf(0.5) as DecisionLevel) + || (c.vivify_age == 0 + && c.reference_height <= state.c_lvl.get_slow().powf(0.75) as DecisionLevel) { match c.lbd { 0..=2 => *num_lbd2 += 1, From 44baea761b8d4518a9e707df6f4c2f9fa2b12ce9 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 20 Jul 2026 05:21:44 +0900 Subject: [PATCH 09/14] fix: polarity is defined to assign by implication --- src/assign/propagate.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index d6d1a772a..d2022b6b7 100644 --- a/src/assign/propagate.rs +++ b/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 { From f5ef8cde925f92de58496c80de3e6ffc0e08692e Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 20 Jul 2026 05:22:39 +0900 Subject: [PATCH 10/14] chore: tweak on `progress` --- src/state.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/state.rs b/src/state.rs index d3d19113e..8aaba2cb3 100644 --- a/src/state.rs +++ b/src/state.rs @@ -608,14 +608,14 @@ impl StateIF for State { { match asg.activity_scheme() { VarActivityScheme::LRB => { - if self.span_manager.current_span() >= 4098 { + if self.span_manager.current_span() >= 16 { "Long LRB" } else { " LRB" } } VarActivityScheme::VMTF => { - if self.span_manager.current_span() >= 4098 { + if self.span_manager.current_span() >= 16 { "LongVMTF" } else { " VMTF" From 81105c4ca043b1d8f7574efe9eca3695e1d694f3 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 21 Jul 2026 13:49:41 +0900 Subject: [PATCH 11/14] exp: a good snapshot (clause part) --- src/cdb/db.rs | 56 ++++++++++++++++++++++++++++++++++++++------- src/types/clause.rs | 6 +++++ src/types/flags.rs | 2 ++ 3 files changed, 56 insertions(+), 8 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index e49876097..0709618f5 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -332,10 +332,13 @@ impl ClauseDBIF for ClauseDB { } = self; let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize]; c.search_from = 2; + c.age = 0; c.lbd = DecisionLevel::MAX; c.vivify_age = 0; c.vivify_at = 0; c.reference_height = DecisionLevel::MAX; + c.referred = 0; + c.turn_on(FlagClause::YOUNG); let len2 = c.lits.len() == 2; *num_clause += 1; if learnt { @@ -828,7 +831,7 @@ 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) { + fn reduce(&mut self, asg: &impl AssignIF, _state: &State) { macro_rules! _height { ($c: expr) => { $c.reference_height + $c.lbd @@ -852,6 +855,7 @@ impl ClauseDBIF for ClauseDB { let mut num_alives: usize = 0; let mut ntier1: usize = 0; let mut ntier2: usize = 0; + let mut saved: Vec<(usize, usize, usize, usize)> = Vec::new(); for (i, c) in clause .iter_mut() .enumerate() @@ -859,6 +863,10 @@ impl ClauseDBIF for ClauseDB { .filter(|(_, c)| !c.is_dead()) { num_alives += 1; + let young = c.is(FlagClause::YOUNG); + if young { + c.turn_off(FlagClause::YOUNG); + } if !c.is(FlagClause::LEARNT) { *num_lbd2 += (c.lbd <= 2) as usize; continue; @@ -872,13 +880,14 @@ impl ClauseDBIF for ClauseDB { } // Don't introduce any length-based crteria! // Clause lengths without context make result worse. - if (c.lbd <= 2 && conflict_index - c.referred_at <= 8 * 8192) - || (c.lbd <= 4 && conflict_index - c.referred_at <= 4 * 8192) - || (c.lbd <= 6 && conflict_index - c.referred_at <= 8192) - || c.len() <= 4 - || (c.vivify_age == 0 - && c.reference_height <= state.c_lvl.get_slow().powf(0.75) as DecisionLevel) - { + if c.lbd <= 8 && c.referred > 0 || c.referred >= 16 { + if c.lbd <= 4 { + c.referred -= 1; + } else { + // c.referred -= 1; + c.referred /= 2; + } + c.age += 1; match c.lbd { 0..=2 => *num_lbd2 += 1, 3..=6 => ntier1 += 1, @@ -886,6 +895,11 @@ impl ClauseDBIF for ClauseDB { } continue; } + // let life = conflict_index - c.referred_at; + // if c.lbd <= 4 && life <= 16 * 8192 { + // // saved.push((life / 8192, c.lbd as usize, c.len(), i)); + // continue; + // } remove_clause_fn( certification_store, binary_link, @@ -898,6 +912,32 @@ impl ClauseDBIF for ClauseDB { ); freelist.push(ClauseId::from(i)); } + saved.sort_unstable(); + let keep = saved.len() / 2; + for (i, (_, _, _, cid)) in saved.into_iter().enumerate() { + let c = &mut clause[cid]; + if i < keep { + c.age += 1; + c.referred /= 2; + match c.lbd { + 0..=2 => *num_lbd2 += 1, + 3..=6 => ntier1 += 1, + _ => ntier2 += 1, + } + } else { + remove_clause_fn( + certification_store, + binary_link, + watch_cache, + num_bi_clause, + num_clause, + num_learnt, + ClauseId::from(cid), + c, + ); + freelist.push(ClauseId::from(cid)); + } + } 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/types/clause.rs b/src/types/clause.rs index 17f3a1d69..4c3900d52 100644 --- a/src/types/clause.rs +++ b/src/types/clause.rs @@ -21,12 +21,15 @@ pub struct Clause { pub(crate) referred_at: usize, /// The minimal decision level at which a conflict occured by this clause pub(crate) reference_height: DecisionLevel, + pub(crate) referred: usize, /// last vivified time in conflicts pub(crate) vivify_age: usize, // last vivified time in conflict pub(crate) vivify_at: usize, /// the minimal lbd of this clause so far pub(crate) lbd: DecisionLevel, + /// the age in rudece count + pub(crate) age: usize, } /// API for Clause, providing literal accessors. @@ -61,9 +64,11 @@ impl Default for Clause { search_from: 2, referred_at: 0, reference_height: DecisionLevel::MAX, + referred: 0, vivify_age: 0, vivify_at: 0, lbd: DecisionLevel::MAX, + age: 0, } } } @@ -221,6 +226,7 @@ impl ClauseIF for Clause { unassigned == 1 && all_others_false } fn update_reference(&mut self, asg: &mut impl AssignIF) { + self.referred += 1; self.referred_at = asg.current_conflict_index(); let level = asg.decision_level(); self.lbd = self.lbd.min(asg.literal_block_distance_current(&self.lits)); diff --git a/src/types/flags.rs b/src/types/flags.rs index dffb36a45..ba8b42381 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 clause is young + const YOUNG = 0b0001_0000; } } From f6b12bde2d1fb12e95a55474458395fa32733dd1 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 21 Jul 2026 13:51:02 +0900 Subject: [PATCH 12/14] exp: a good snapshot (search part: constant reduction; flat probability model for rephasing) --- src/solver/search.rs | 53 +++++++++++++++++++++++--------------------- 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index b543030f0..fcd60880d 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -240,8 +240,7 @@ fn search( let vivification_interval: usize = 10_000; let mut assign_peak: usize = 0; let luby_scale: usize = 2048 * 4; - let mut span_scale: usize = luby_scale; - let adaptive_lr: f64 = 1.0 / (luby_scale as f64).sqrt(); + // let mut adaptive_lr: f64 = 1.0 / (luby_scale as f64).sqrt(); macro_rules! reduce { () => { @@ -301,6 +300,7 @@ fn search( } else { cdb.lbd.update(lbd as f64); cdb[cid].lbd = lbd; + cdb[cid].referred_at = asg.current_conflict_index(); } match asg.stack_len().cmp(&assign_peak) { Ordering::Less => {} @@ -338,16 +338,16 @@ fn search( reduction_pressure += 1; vivification_pressure += 1; span_len += 1; - if reduction_pressure >= luby_scale { + if reduction_pressure >= 4 * luby_scale { RESTART!(asg, cdb, state)?; reduce!(); - if vivification_pressure >= vivification_interval { + if true || vivification_pressure >= vivification_interval { if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; } vivification_pressure = 0; } - if elimination_pressure >= elimination_interval { + if true || elimination_pressure >= elimination_interval { if cfg!(feature = "clause_elimination") { let mut elim = Eliminator::instantiate(&state.config, &state.cnf); state.flush("clause subsumption, "); @@ -358,34 +358,34 @@ fn search( } } - 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); let _conflict_index = asg.current_conflict_index(); if cfg!(feature = "rephase") { match rng.next_f64() { - 0.0..0.5 if state.span_manager.current_span() >= 256 => { + 0.0..0.25 => { asg.phase_mode = RephaseTarget::Walk; } - 0.5..1.0 if state.span_manager.current_span() >= 256 => { - asg.phase_mode = RephaseTarget::Polarity; - } - 0.0..0.4 => { + 0.25..0.45 => { asg.phase_mode = RephaseTarget::Best; } - 0.4..0.65 => { + 0.45..0.6 => { + asg.phase_mode = RephaseTarget::Polarity; + } + 0.6..0.75 => { asg.phase_mode = RephaseTarget::False; } - 0.65..0.9 => { + 0.75..0.9 => { asg.phase_mode = RephaseTarget::True; } - 0.9..0.95 => { + 0.9..1.0 => { asg.phase_mode = RephaseTarget::Random; } - 0.95..1.0 => { - asg.phase_mode = RephaseTarget::Inverted; - } + // 0.95..1.0 => { + // asg.phase_mode = RephaseTarget::Inverted; + // } _ => { asg.phase_mode = RephaseTarget::Walk; } @@ -394,22 +394,25 @@ fn search( 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.set_learning_rate(0.0); asg.rebuild_order(); } - 0.2..1.0 if asg.activity_scheme != VarActivityScheme::LRB => { + 0.2..1.0 => { + if asg.activity_scheme != VarActivityScheme::LRB { + asg.activity_scheme = VarActivityScheme::LRB; + asg.rebuild_order(); + } // 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). - asg.activity_scheme = VarActivityScheme::LRB; - asg.set_learning_rate(adaptive_lr); - asg.rebuild_order(); + // asg.set_learning_rate(adaptive_lr); } _ => (), } } + // span_scale = luby_scale * state.span_manager.current_span(); if new_segment.is_some() { - span_scale = luby_scale * state.span_manager.envelop_index(); + 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); } } let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar); From 6da2147f993d1fbfe239adb7283f86fa8dcb85e5 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 21 Jul 2026 13:54:08 +0900 Subject: [PATCH 13/14] chore: clean up `search` --- src/solver/search.rs | 35 ++++++++++------------------------- 1 file changed, 10 insertions(+), 25 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index fcd60880d..698bfa5a9 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -231,16 +231,11 @@ fn search( ) -> Result { 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 mut vivification_pressure: usize = 0; - let vivification_interval: usize = 10_000; let mut assign_peak: usize = 0; let luby_scale: usize = 2048 * 4; - // let mut adaptive_lr: f64 = 1.0 / (luby_scale as f64).sqrt(); macro_rules! reduce { () => { @@ -333,28 +328,20 @@ fn search( // } } } - elimination_pressure += 1; progress_pressure += 1; reduction_pressure += 1; - vivification_pressure += 1; span_len += 1; if reduction_pressure >= 4 * luby_scale { RESTART!(asg, cdb, state)?; reduce!(); - if true || vivification_pressure >= vivification_interval { - if cfg!(feature = "clause_vivification") { - cdb.vivify(asg, state)?; - } - vivification_pressure = 0; + if cfg!(feature = "clause_vivification") { + cdb.vivify(asg, state)?; } - if true || 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; + 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()); } } @@ -397,13 +384,11 @@ fn search( // asg.set_learning_rate(0.0); asg.rebuild_order(); } - 0.2..1.0 => { - if asg.activity_scheme != VarActivityScheme::LRB { - asg.activity_scheme = VarActivityScheme::LRB; - 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(); } _ => (), } From 33b982d474099f7998742622089971fb382c732c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 21 Jul 2026 17:20:44 +0900 Subject: [PATCH 14/14] chore: clean up Clause --- src/cdb/db.rs | 47 +++----------------------------------- src/cdb/vivify.rs | 10 +++++--- src/processor/eliminate.rs | 6 +++-- src/types/clause.rs | 19 +++++---------- src/types/flags.rs | 2 -- 5 files changed, 20 insertions(+), 64 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 0709618f5..622f08081 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -332,13 +332,11 @@ impl ClauseDBIF for ClauseDB { } = self; let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize]; c.search_from = 2; - c.age = 0; c.lbd = DecisionLevel::MAX; + c.referred = 0; + // c.referred_at = 0; c.vivify_age = 0; c.vivify_at = 0; - c.reference_height = DecisionLevel::MAX; - c.referred = 0; - c.turn_on(FlagClause::YOUNG); let len2 = c.lits.len() == 2; *num_clause += 1; if learnt { @@ -831,13 +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) { + 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(); self.num_reduction += 1; let ClauseDB { clause, @@ -855,7 +852,6 @@ impl ClauseDBIF for ClauseDB { let mut num_alives: usize = 0; let mut ntier1: usize = 0; let mut ntier2: usize = 0; - let mut saved: Vec<(usize, usize, usize, usize)> = Vec::new(); for (i, c) in clause .iter_mut() .enumerate() @@ -863,10 +859,6 @@ impl ClauseDBIF for ClauseDB { .filter(|(_, c)| !c.is_dead()) { num_alives += 1; - let young = c.is(FlagClause::YOUNG); - if young { - c.turn_off(FlagClause::YOUNG); - } if !c.is(FlagClause::LEARNT) { *num_lbd2 += (c.lbd <= 2) as usize; continue; @@ -884,10 +876,8 @@ impl ClauseDBIF for ClauseDB { if c.lbd <= 4 { c.referred -= 1; } else { - // c.referred -= 1; c.referred /= 2; } - c.age += 1; match c.lbd { 0..=2 => *num_lbd2 += 1, 3..=6 => ntier1 += 1, @@ -895,11 +885,6 @@ impl ClauseDBIF for ClauseDB { } continue; } - // let life = conflict_index - c.referred_at; - // if c.lbd <= 4 && life <= 16 * 8192 { - // // saved.push((life / 8192, c.lbd as usize, c.len(), i)); - // continue; - // } remove_clause_fn( certification_store, binary_link, @@ -912,32 +897,6 @@ impl ClauseDBIF for ClauseDB { ); freelist.push(ClauseId::from(i)); } - saved.sort_unstable(); - let keep = saved.len() / 2; - for (i, (_, _, _, cid)) in saved.into_iter().enumerate() { - let c = &mut clause[cid]; - if i < keep { - c.age += 1; - c.referred /= 2; - match c.lbd { - 0..=2 => *num_lbd2 += 1, - 3..=6 => ntier1 += 1, - _ => ntier2 += 1, - } - } else { - remove_clause_fn( - certification_store, - binary_link, - watch_cache, - num_bi_clause, - num_clause, - num_learnt, - ClauseId::from(cid), - c, - ); - freelist.push(ClauseId::from(cid)); - } - } 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 05926995b..4d4c9ab3a 100644 --- a/src/cdb/vivify.rs +++ b/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::>(); 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; diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index 180018831..f117e0a7b 100644 --- a/src/processor/eliminate.rs +++ b/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!( diff --git a/src/types/clause.rs b/src/types/clause.rs index 4c3900d52..af1f18532 100644 --- a/src/types/clause.rs +++ b/src/types/clause.rs @@ -17,19 +17,16 @@ 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 minimal lbd of this clause so far + pub(crate) lbd: DecisionLevel, + ///the count of references in conflict analysis + pub(crate) referred: usize, /// The last reference time in conflict analysis pub(crate) referred_at: usize, - /// The minimal decision level at which a conflict occured by this clause - pub(crate) reference_height: DecisionLevel, - pub(crate) referred: usize, /// last vivified time in conflicts pub(crate) vivify_age: usize, // last vivified time in conflict pub(crate) vivify_at: usize, - /// the minimal lbd of this clause so far - pub(crate) lbd: DecisionLevel, - /// the age in rudece count - pub(crate) age: usize, } /// API for Clause, providing literal accessors. @@ -62,13 +59,11 @@ impl Default for Clause { lits: vec![], flags: FlagClause::empty(), search_from: 2, - referred_at: 0, - reference_height: DecisionLevel::MAX, + lbd: DecisionLevel::MAX, referred: 0, + referred_at: 0, vivify_age: 0, vivify_at: 0, - lbd: DecisionLevel::MAX, - age: 0, } } } @@ -228,9 +223,7 @@ impl ClauseIF for Clause { fn update_reference(&mut self, asg: &mut impl AssignIF) { self.referred += 1; self.referred_at = asg.current_conflict_index(); - let level = asg.decision_level(); self.lbd = self.lbd.min(asg.literal_block_distance_current(&self.lits)); - self.reference_height = self.reference_height.min(level); } } diff --git a/src/types/flags.rs b/src/types/flags.rs index ba8b42381..dffb36a45 100644 --- a/src/types/flags.rs +++ b/src/types/flags.rs @@ -27,8 +27,6 @@ bitflags! { const ASSIGN_REASON = 0b0000_1000; // /// used in the best assignments // const BEST_PROPAGATOR = 0b0010_0000; - /// a clause is young - const YOUNG = 0b0001_0000; } }