From 34c4304af89001743aa76803ebd0e119916bf1bb Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Wed, 8 Jul 2026 17:05:48 +0900 Subject: [PATCH 1/7] 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> = Vec::new(); + // let mut tier1: Vec> = Vec::new(); + // let mut tier2: Vec> = 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> = 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::(); 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::>(); 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 894bd9ca39762c54997bee7d28cf69bb11c254f9 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 9 Jul 2026 17:28:57 +0900 Subject: [PATCH 2/7] 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> = Vec::new(); - // let mut tier1: Vec> = Vec::new(); + let mut reserved: Vec> = Vec::new(); // let mut tier2: Vec> = 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::(); + 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::>(); 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 594fcf4c150bba5cbcd1aef95828ceb7f097722e Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 11 Jul 2026 13:24:07 +0900 Subject: [PATCH 3/7] 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> = Vec::new(); - // let mut tier2: Vec> = 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::(); - 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::>(); 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 043f971059c2c07923cc65642cb0b79aa26e19a8 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 13 Jul 2026 12:04:40 +0900 Subject: [PATCH 4/7] 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 = 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 032fbe83ff7682b42231eb1b81872b9c8b947fc3 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 13 Jul 2026 13:35:56 +0900 Subject: [PATCH 5/7] 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 080f0afaa096ad0073096fb91db88717e54fc54f Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 13 Jul 2026 13:39:01 +0900 Subject: [PATCH 6/7] 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: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 e036cf3281ce278840d97b77a096042f51d08cd3 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 13 Jul 2026 19:48:13 +0900 Subject: [PATCH 7/7] 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::>(); 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);