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/propagate.rs b/src/assign/propagate.rs index 6ed720a6d..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")] @@ -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/assign/stack.rs b/src/assign/stack.rs index 98472884e..a98e9e31b 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] } @@ -387,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/cdb/db.rs b/src/cdb/db.rs index 2911f9c0c..2934c155a 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, @@ -7,7 +5,7 @@ use { property, watch_cache::*, }, - crate::{assign::AssignIF, types::*}, + crate::{assign::AssignIF, state::State, types::*}, std::{ collections::HashMap, num::NonZeroU32, @@ -16,6 +14,7 @@ use { }, }; +use std::f64; #[cfg(not(feature = "no_IO"))] use std::{fs::File, io::Write, path::Path}; @@ -68,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_at: usize, } impl Default for ClauseDB { @@ -91,7 +89,6 @@ impl Default for ClauseDB { num_reregistration: 0, tier1_clauses: Ema::default(), tier2_clauses: Ema::default(), - last_reduction_at: 0, } } } @@ -313,11 +310,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 +331,11 @@ impl ClauseDBIF for ClauseDB { .. } = self; let c = &mut clause[NonZeroU32::get(cid.ordinal) as usize]; + c.search_from = 2; + c.lbd = DecisionLevel::MAX; + c.vivify_age = 0; + c.vivify_at = 0; + c.reference_height = DecisionLevel::MAX; let len2 = c.lits.len() == 2; *num_clause += 1; if learnt { @@ -831,7 +828,15 @@ 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: &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, @@ -846,16 +851,9 @@ impl ClauseDBIF for ClauseDB { .. } = self; *num_lbd2 = 0; - let num_conflict = asg.derefer(assign::property::Tusize::NumConflict); let mut num_alives: usize = 0; - // tier 1 group: the small clauses under the best assignment let mut ntier1: usize = 0; - // tier 2 group: the small clauses under the best assignment - let mut ntier2: usize = 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; for (i, c) in clause .iter_mut() .enumerate() @@ -863,24 +861,28 @@ 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; + // 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 height!(c) <= effective_height + && (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, } - _ => (), + continue; } remove_clause_fn( certification_store, @@ -893,72 +895,7 @@ impl ClauseDBIF for ClauseDB { c, ); freelist.push(ClauseId::from(i)); - /* match c.len() { - 0..=5 => { - *num_lbd2 += 1; - continue; - } - 6..=8 if c.reference_rate >= 0.0001 => { - ntier1 += 1; - continue; - } - 9 | 10 if c.reference_rate >= 0.001 => { - ntier2 += 1; - continue; - } - 11 | 12 if c.reference_rate >= 0.01 => { - ntier2 += 1; - continue; - } - _ if c.lbd <= 6 && c.reference_rate >= 1.0 => { - continue; - } - _ if c.referred_at >= *last_reduction_at /* && referred */ => { - continue; - } - _ if !c.is(FlagClause::LEARNT) || c.is(FlagClause::ASSIGN_REASON) => { - continue; - } - _ => { - remove_clause_fn( - certification_store, - binary_link, - watch_cache, - num_bi_clause, - num_clause, - num_learnt, - ClauseId::from(i), - c, - ); - freelist.push(ClauseId::from(i)); - } - } - */ - } - if cands.len() > ntier2 { - cands.sort_unstable(); - for cid in cands - .iter() // .skip(ntier1) - .skip(ntier2) - { - let c = &mut clause[cid.to()]; - let cid = ClauseId::from(cid.to()); - remove_clause_fn( - certification_store, - binary_link, - watch_cache, - num_bi_clause, - num_clause, - num_learnt, - cid, - c, - ); - freelist.push(cid); - } - } else { - ntier2 = cands.len(); } - self.last_reduction_at = num_conflict; self.tier1_clauses.update(ntier1 as f64 / num_alives as f64); self.tier2_clauses.update(ntier2 as f64 / num_alives as f64); } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 399ee624a..81116ffee 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); + 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 102f0da6a..e95aaec8e 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,13 @@ 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 = 10_000 * c.len() * 2_usize.pow(c.vivify_age as u32 + 1); + if c.vivify_at + span > asg.num_conflict + || (c.referred_at <= c.vivify_at && (c.is(FlagClause::LEARNT) || c.vivify_age != 0)) + { continue; } + num_check += 1; let c = &mut self[cid]; // c.update_reference_rate(asg.num_conflict); // Skip clauses that are unlikely to be improved by vivification. @@ -60,15 +54,15 @@ 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; + // 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; - let referred_at = c.referred_at; - let reference_rate = c.reference_rate; + c.vivify_age += 1; + let reference_height = c.reference_height; let clits = c.iter().copied().collect::>(); if to_display <= num_check { state.flush(""); @@ -77,7 +71,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()); @@ -142,7 +135,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"); @@ -156,9 +148,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].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); num_shrink += 1; diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index 61bc87b4e..180018831 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -94,6 +94,9 @@ 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); #[cfg(feature = "trace_elimination")] println!( diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index e90fe9602..a7e04b5c2 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -134,12 +134,19 @@ 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() { + cdb[ci].reference_height = cdb[ci].reference_height.min(lvl); } } AssignReason::Decision(_) => (), @@ -216,7 +223,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 +428,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); cdb[cid].lbd = cdb[cid] .lbd .min(asg.literal_block_distance_current(&cdb[cid].lits)); @@ -613,7 +618,7 @@ fn lit_level( cdb[cid].lit0(), lit, cid, - &cdb[cid] + cdb[cid] ); // assert!( // !bag.contains(&lit), diff --git a/src/solver/search.rs b/src/solver/search.rs index aa0d6fda9..8e444f26a 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 = 80_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 = 256; + let luby_scale: usize = 32; 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); + cdb.reduce(asg, state); }}; } 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 { @@ -402,11 +403,13 @@ fn search( 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 { + // reduce!(); + // } if vivification_pressure >= vivification_interval { if cfg!(feature = "clause_vivification") { - cdb.vivify(asg, state, true)?; + cdb.vivify(asg, state)?; } vivification_pressure = 0; } @@ -419,11 +422,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 +449,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..4be79afaa 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 @@ -162,11 +164,12 @@ 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, + last_assertion: 0, #[cfg(feature = "chrono_BT")] chrono_bt_threshold: 100, @@ -875,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,) } } } diff --git a/src/types/clause.rs b/src/types/clause.rs index 868b743c1..194cb8da3 100644 --- a/src/types/clause.rs +++ b/src/types/clause.rs @@ -17,12 +17,10 @@ pub struct Clause { /// the index from which `propagate` starts searching an un-falsified literal. /// Since it's just a hint, we don't need u32 or usize. pub search_from: u16, - /// The number of referrences in conflict analysis - pub(crate) referred: usize, - /// Sum of activated (used as propagated) duration + /// The last reference time in conflict analysis pub(crate) referred_at: usize, - /// The average number of references in a vivification interval - pub(crate) reference_rate: f64, + /// 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 @@ -51,8 +49,8 @@ pub trait ClauseIF { fn len(&self) -> usize; /// return true is this is a unit clause under `asg`. fn is_unit_under(&self, asg: &impl AssignIF) -> bool; - /// update reference_rate and return `true` if referred. - fn update_reference_rate(&mut self, base: usize) -> bool; + /// update reference_distance. + fn update_reference(&mut self, asg: &impl AssignIF); } impl Default for Clause { @@ -61,9 +59,8 @@ impl Default for Clause { lits: vec![], flags: FlagClause::empty(), search_from: 2, - referred: 0, referred_at: 0, - reference_rate: 1.0, + reference_height: DecisionLevel::MAX, vivify_age: 0, vivify_at: 0, lbd: DecisionLevel::MAX, @@ -223,17 +220,10 @@ 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, asg: &impl AssignIF) { + self.referred_at = asg.current_conflict_index(); + let level = asg.decision_level(); + self.reference_height = self.reference_height.min(level); } }