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 { diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 2934c155a..622f08081 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -333,9 +333,10 @@ impl ClauseDBIF for ClauseDB { let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize]; c.search_from = 2; c.lbd = DecisionLevel::MAX; + c.referred = 0; + // c.referred_at = 0; c.vivify_age = 0; c.vivify_at = 0; - c.reference_height = DecisionLevel::MAX; let len2 = c.lits.len() == 2; *num_clause += 1; if learnt { @@ -828,15 +829,12 @@ impl ClauseDBIF for ClauseDB { c.is(FlagClause::LEARNT) } /// reduce the number of 'learnt' or *removable* clauses. - fn reduce(&mut self, asg: &impl AssignIF, state: &State) { - macro_rules! height { + fn reduce(&mut self, _asg: &impl AssignIF, _state: &State) { + macro_rules! _height { ($c: expr) => { $c.reference_height + $c.lbd }; } - let conflict_index: usize = asg.current_conflict_index(); - let effective_height: DecisionLevel = - (0.25 * (state.c_lvl.get_slow() + state.b_lvl.get_slow())) as DecisionLevel; self.num_reduction += 1; let ClauseDB { clause, @@ -874,9 +872,12 @@ impl ClauseDBIF for ClauseDB { } // Don't introduce any length-based crteria! // Clause lengths without context make result worse. - if height!(c) <= effective_height - && (c.reference_height <= 4 || (conflict_index - c.referred_at) <= 800_000) - { + if c.lbd <= 8 && c.referred > 0 || c.referred >= 16 { + if c.lbd <= 4 { + c.referred -= 1; + } else { + c.referred /= 2; + } match c.lbd { 0..=2 => *num_lbd2 += 1, 3..=6 => ntier1 += 1, 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/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/solver/search.rs b/src/solver/search.rs index 8e444f26a..698bfa5a9 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -223,88 +223,26 @@ impl SolveIF for Solver { } } -/// table of (RephaseTarget, span length, next index) -const REPHASE_ROTATION: [(RephaseTarget, usize, usize); 5] = [ - (RephaseTarget::Polarity, 8, 1), - (RephaseTarget::False, 2, 2), - (RephaseTarget::True, 2, 3), - (RephaseTarget::Best, 2, 4), - (RephaseTarget::Walk, 8, 0), -]; - /// main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT. fn search( asg: &mut AssignStack, cdb: &mut ClauseDB, state: &mut State, ) -> Result { + let mut rng: SplitMix64 = SplitMix64::new(state.cnf.num_of_variables as u64); let mut span_len: usize = 1; - let mut elimination_pressure: usize = 0; - let elimination_interval: usize = 80_000; let mut progress_pressure: usize = 0; let progress_interval: usize = 10_000; let mut reduction_pressure: usize = 0; - let reduction_interval: usize = 80_000; - let mut rephase_rotation_pressure: usize = 0; - let mut vivification_pressure: usize = 0; - let vivification_interval: usize = 20_000; - let mut current_phase: &(RephaseTarget, usize, usize) = &REPHASE_ROTATION[0]; - let vmtf_interval: usize = 20; let mut assign_peak: usize = 0; - let luby_scale: usize = 32; - let mut span_scale: usize = luby_scale; + let luby_scale: usize = 2048 * 4; macro_rules! reduce { - () => {{ + () => { state.search_mode_ratio.0.update(0.0); state.search_mode_ratio.1.update(0.0); reduction_pressure = 0; cdb.reduce(asg, state); - }}; - } - macro_rules! to_lrb { - () => { - if asg.activity_scheme != VarActivityScheme::LRB { - asg.activity_scheme = VarActivityScheme::LRB; - let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64; - let adaptive_lr: f64 = 1.0 / span.sqrt(); - asg.set_learning_rate(adaptive_lr); - asg.rebuild_order(); - } - current_phase = &REPHASE_ROTATION[0]; - asg.phase_mode = current_phase.0; - rephase_rotation_pressure = 0; - }; - } - macro_rules! to_vmtf { - () => { - if asg.activity_scheme != VarActivityScheme::VMTF { - asg.activity_scheme = VarActivityScheme::VMTF; - asg.phase_mode = RephaseTarget::Walk; - asg.set_learning_rate(0.0); // Don't change this - asg.rebuild_order(); - rephase_rotation_pressure = 0; - } - }; - } - macro_rules! rotate_rephase_mode { - () => { - current_phase = &REPHASE_ROTATION[current_phase.2]; - asg.phase_mode = current_phase.0; - rephase_rotation_pressure = 0; - // if current_phase.2 == 0 { - // current_phase = &REPHASE_ROTATION[current_phase.2]; - // asg.phase_mode = current_phase.0; - // rephase_rotation_pressure = 0; - // // asg.clear_best_phases(); - // // state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar); - // // assign_peak = 0; - // // to_vmtf!(); - // } else { - // current_phase = &REPHASE_ROTATION[current_phase.2]; - // asg.phase_mode = current_phase.0; - // rephase_rotation_pressure = 0; - // } }; } macro_rules! update_core { @@ -313,15 +251,15 @@ fn search( if let Some(core) = asg.check_best_phases() { assign_peak = assign_peak.saturating_sub(2 * $n); state.core_size = core; - to_vmtf!(); + // to_vmtf!(); } else { assign_peak = 0; - let pre = state.core_size; + // let pre = state.core_size; state.core_size = asg.derefer(assign::property::Tusize::NumUnassertedVar); cdb.save_best_assign_reasons(asg, true); - if pre < state.core_size { - to_vmtf!(); - } + // if pre < state.core_size { + // to_vmtf!(); + // } } }; } @@ -356,7 +294,8 @@ fn search( update_core!(1); } else { cdb.lbd.update(lbd as f64); - cdb[cid].lbd = DecisionLevel::MAX; + cdb[cid].lbd = lbd; + cdb[cid].referred_at = asg.current_conflict_index(); } match asg.stack_len().cmp(&assign_peak) { Ordering::Less => {} @@ -389,71 +328,82 @@ fn search( // } } } - elimination_pressure += 1; progress_pressure += 1; reduction_pressure += 1; - rephase_rotation_pressure += 1; - vivification_pressure += 1; span_len += 1; - // Don't check with `>= 1 * reduction_interval`. It prevents `reduce!(true)`. - if reduction_pressure > reduction_interval { + if reduction_pressure >= 4 * luby_scale { + RESTART!(asg, cdb, state)?; reduce!(); + if cfg!(feature = "clause_vivification") { + cdb.vivify(asg, state)?; + } + if cfg!(feature = "clause_elimination") { + let mut elim = Eliminator::instantiate(&state.config, &state.cnf); + state.flush("clause subsumption, "); + elim.simplify(asg, cdb, state, false)?; + asg.eliminated.append(elim.eliminated_lits()); + } } - if state.span_manager.span_ended(span_len / span_scale) { + + if state.span_manager.span_ended(span_len / luby_scale) { span_len = 0; let new_segment = state.span_manager.prepare_new_span(span_len); dump_stage(asg, state, new_segment); - RESTART!(asg, cdb, state)?; - // if reduction_pressure > reduction_interval { - // reduce!(); - // } - if vivification_pressure >= vivification_interval { - if cfg!(feature = "clause_vivification") { - cdb.vivify(asg, state)?; - } - vivification_pressure = 0; - } - if elimination_pressure >= elimination_interval { - if cfg!(feature = "clause_elimination") { - let mut elim = Eliminator::instantiate(&state.config, &state.cnf); - state.flush("clause subsumption, "); - elim.simplify(asg, cdb, state, false)?; - asg.eliminated.append(elim.eliminated_lits()); - } - elimination_pressure = 0; - } + let _conflict_index = asg.current_conflict_index(); if cfg!(feature = "rephase") { - match asg.activity_scheme { - VarActivityScheme::LRB - if rephase_rotation_pressure >= current_phase.1 * span_scale => - { - rotate_rephase_mode!(); + match rng.next_f64() { + 0.0..0.25 => { + asg.phase_mode = RephaseTarget::Walk; + } + 0.25..0.45 => { + asg.phase_mode = RephaseTarget::Best; } - VarActivityScheme::VMTF - if rephase_rotation_pressure >= vmtf_interval * span_scale => - { - to_lrb!(); + 0.45..0.6 => { + asg.phase_mode = RephaseTarget::Polarity; + } + 0.6..0.75 => { + asg.phase_mode = RephaseTarget::False; + } + 0.75..0.9 => { + asg.phase_mode = RephaseTarget::True; + } + 0.9..1.0 => { + asg.phase_mode = RephaseTarget::Random; + } + // 0.95..1.0 => { + // asg.phase_mode = RephaseTarget::Inverted; + // } + _ => { + asg.phase_mode = RephaseTarget::Walk; + } + } + match rng.next_f64() { + 0.0..0.2 if asg.activity_scheme != VarActivityScheme::VMTF => { + asg.activity_scheme = VarActivityScheme::VMTF; + // asg.set_learning_rate(adaptive_lr); + // asg.set_learning_rate(0.0); + asg.rebuild_order(); + } + 0.2..1.0 if asg.activity_scheme != VarActivityScheme::LRB => { + asg.activity_scheme = VarActivityScheme::LRB; + // Adapt LRB learning rate to the upcoming Luby envelope height: + // asg.set_learning_rate(adaptive_lr); + asg.rebuild_order(); } _ => (), } } + // span_scale = luby_scale * state.span_manager.current_span(); if new_segment.is_some() { - span_scale = luby_scale * state.span_manager.envelop_index(); - // Adapt LRB learning rate to the upcoming Luby envelope height: - // shorter spans → higher α (fast learning before the next restart), - // longer spans → lower α (stable estimates over more conflicts). - let span: f64 = (state.span_manager.envelop_index() * luby_scale) as f64; - let adaptive_lr: f64 = 1.0 / span.sqrt(); + let span_scale = luby_scale * state.span_manager.envelop_index(); + let adaptive_lr = 1.0 / (span_scale as f64).sqrt(); asg.set_learning_rate(adaptive_lr); - } else { - asg.rescale_learning_rate(0.9); } } let unasserted_now = asg.derefer(assign::property::Tusize::NumUnassertedVar); if unasserted_now != unasserted_pre { state.last_assertion = asg.num_conflict; update_core!(unasserted_pre - unasserted_now); - // to_vmtf!(); } if progress_pressure >= progress_interval { state.progress(asg, cdb); 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 } diff --git a/src/state.rs b/src/state.rs index 4be79afaa..8aaba2cb3 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, @@ -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" diff --git a/src/types/clause.rs b/src/types/clause.rs index 194cb8da3..af1f18532 100644 --- a/src/types/clause.rs +++ b/src/types/clause.rs @@ -17,16 +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, /// 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, } /// API for Clause, providing literal accessors. @@ -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 { @@ -59,11 +59,11 @@ impl Default for Clause { lits: vec![], flags: FlagClause::empty(), search_from: 2, + lbd: DecisionLevel::MAX, + referred: 0, referred_at: 0, - reference_height: DecisionLevel::MAX, vivify_age: 0, vivify_at: 0, - lbd: DecisionLevel::MAX, } } } @@ -220,10 +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 += 1; self.referred_at = asg.current_conflict_index(); - let level = asg.decision_level(); - self.reference_height = self.reference_height.min(level); + self.lbd = self.lbd.min(asg.literal_block_distance_current(&self.lits)); } }