diff --git a/Cargo.lock b/Cargo.lock index a02f99dee..7c59a9209 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -150,12 +150,12 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.9" +version = "0.3.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba" +checksum = "33d852cb9b869c2a9b3df2f71a3074817f01e1844f839a144f5fcef059a4eb5d" dependencies = [ "libc", - "windows-sys", + "windows-sys 0.59.0", ] [[package]] @@ -172,9 +172,9 @@ checksum = "f81ec6369c545a7d40e4589b5597581fa1c441fe1cce96dd1de43159910a36a2" [[package]] name = "hashbrown" -version = "0.15.1" +version = "0.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" +checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" dependencies = [ "allocator-api2", "equivalent", @@ -242,9 +242,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.11" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" +checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674" [[package]] name = "js-sys" @@ -257,9 +257,9 @@ dependencies = [ [[package]] name = "libc" -version = "0.2.162" +version = "0.2.166" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398" +checksum = "c2ccc108bbc0b1331bd061864e7cd823c0cab660bbe6970e66e2c0614decde36" [[package]] name = "linux-raw-sys" @@ -302,7 +302,7 @@ dependencies = [ "libc", "log", "wasi", - "windows-sys", + "windows-sys 0.52.0", ] [[package]] @@ -373,9 +373,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.89" +version = "1.0.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" +checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0" dependencies = [ "unicode-ident", ] @@ -422,15 +422,15 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.40" +version = "0.38.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99e4ea3e1cdc4b559b8e5650f9c8e5998e3e5c1343b4eaf034565f32318d63c0" +checksum = "d7f649912bc1495e167a6edee79151c84b1bad49748cb4f1f1167f459f6224f6" dependencies = [ "bitflags", "errno", "libc", "linux-raw-sys", - "windows-sys", + "windows-sys 0.52.0", ] [[package]] @@ -553,9 +553,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.87" +version = "2.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" +checksum = "44d46482f1c1c87acd84dea20c1bf5ebff4c757009ed6bf19cfd36fb10e92c4e" dependencies = [ "proc-macro2", "quote", @@ -585,9 +585,9 @@ checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3" [[package]] name = "unicode-ident" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" +checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83" [[package]] name = "unicode-segmentation" @@ -720,6 +720,15 @@ dependencies = [ "windows-targets", ] +[[package]] +name = "windows-sys" +version = "0.59.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" +dependencies = [ + "windows-targets", +] + [[package]] name = "windows-targets" version = "0.52.6" diff --git a/src/assign/mod.rs b/src/assign/mod.rs index 92e801865..caeb1ef89 100644 --- a/src/assign/mod.rs +++ b/src/assign/mod.rs @@ -1,6 +1,6 @@ /// Module `assign` implements Boolean Constraint Propagation and decision var selection. /// This version can handle Chronological and Non Chronological Backtrack. - +/// /// Ema mod ema; /// Heap @@ -54,7 +54,7 @@ pub trait AssignIF: { /// return root level. fn root_level(&self) -> DecisionLevel; - /// return a literal in the stack. + /// return the `i`-th literal in the stack. fn stack(&self, i: usize) -> Lit; /// return literals in the range of stack. fn stack_range(&self, r: Range) -> &[Lit]; diff --git a/src/assign/stack.rs b/src/assign/stack.rs index 6a432f344..1bddc6d75 100644 --- a/src/assign/stack.rs +++ b/src/assign/stack.rs @@ -212,6 +212,10 @@ impl Instantiate for AssignStack { SolverEvent::Eliminate(vi) => { self.make_var_eliminated(vi); } + SolverEvent::Restart => { + #[cfg(feature = "trail_saving")] + self.clear_saved_trail(); + } SolverEvent::Stage(scale) => { self.stage_scale = scale; #[cfg(feature = "trail_saving")] diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 1414b2d86..102141dd7 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -164,7 +164,9 @@ impl Instantiate for ClauseDB { self.watch.push(WatchLiteralIndexRef::default()); self.lbd_temp.push(0); } - SolverEvent::Restart => (), + SolverEvent::Restart => { + self.lbd.reset_fast(); + } _ => (), } } diff --git a/src/cdb/ema.rs b/src/cdb/ema.rs index f1622f1aa..cf96d6188 100644 --- a/src/cdb/ema.rs +++ b/src/cdb/ema.rs @@ -49,6 +49,9 @@ impl EmaMutIF for ProgressLBD { self.sum += d as usize; self.ema.update(d as f64); } + fn reset_fast(&mut self) { + self.ema.reset_fast(); + } fn reset_to(&mut self, val: f64) { self.ema.reset_to(val); } diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 466a52c91..f8e38b179 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -87,12 +87,14 @@ pub trait ClauseDBIF: /// reduce learnt clauses /// # CAVEAT /// *precondition*: decision level == 0. - fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64); + fn reduce(&mut self, asg: &impl AssignIF, threshold: f64, new_assertion: bool); /// remove all learnt clauses. fn reset(&mut self); /// update flags. /// return `true` if it's learnt. fn update_entanglement(&mut self, asg: &impl AssignIF, ci: ClauseIndex); + /// update LBD and return the new value + fn update_lbd(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> DecisionLevel; /// record an asserted literal to unsat certification. fn certificate_add_assertion(&mut self, lit: Lit); /// save the certification record to a file. @@ -518,21 +520,29 @@ impl ClauseDBIF for ClauseDB { let rank: DecisionLevel = c.update_lbd(asg, lbd_temp); self.lb_entanglement.update(rank as f64); } + fn update_lbd(&mut self, asg: &impl AssignIF, ci: ClauseIndex) -> DecisionLevel { + let ClauseDB { + ref mut clause, + ref mut lbd_temp, + .. + } = self; + let c = &mut clause[ci]; + c.update_lbd(asg, lbd_temp) + } /// reduce the number of 'learnt' or *removable* clauses. #[cfg(feature = "keep_just_used_clauses")] - fn reduce(&mut self, asg: &mut impl AssignIF, threshold: f64) { - impl Clause { - fn extended_lbd(&self) -> f64 { - let l: f64 = self.len() as f64; - let r: f64 = self.rank as f64; - r + (l - r) / (l - r + 1.0) - } - } + fn reduce(&mut self, asg: &impl AssignIF, threshold: f64, new_assertion: bool) { + // impl Clause { + // fn extended_lbd(&self) -> f64 { + // let l: f64 = self.len() as f64; + // let r: f64 = self.rank as f64; + // r + (l - r) / (l - r + 1.0) + // } + // } // let ClauseDB { // ref mut clause, // ref mut lbd_temp, // ref mut num_reduction, - // #[cfg(feature = "clause_rewarding")] // ref tick, // #[cfg(feature = "clause_rewarding")] @@ -542,71 +552,42 @@ impl ClauseDBIF for ClauseDB { self.num_reduction += 1; // let mut keep: usize = 0; // let mut alives: usize = 0; - // let mut perm: Vec> = Vec::with_capacity(clause.len()); // let reduction_threshold = self.reduction_threshold + 4; for ci in 1..self.clause.len() { if self.clause[ci].is_dead() { continue; } - // alives += 1; - // keep += 1; - self.clause[ci].turn_off(FlagClause::NEW_CLAUSE); - // if self.clause[ci].is(FlagClause::FORWD_LINK) - // || self.clause[ci].is(FlagClause::BCKWD_LINK) - // { - // self.clause[ci].turn_off(FlagClause::FORWD_LINK); - // self.clause[ci].turn_off(FlagClause::BCKWD_LINK); - // continue; - // } - /* let fwd: bool = self.clause[ci].is(FlagClause::FORWD_LINK); - self.clause[ci].turn_off(FlagClause::FORWD_LINK); - if self.clause[ci].is(FlagClause::BCKWD_LINK) { - self.clause[ci].turn_off(FlagClause::BCKWD_LINK); - continue; - } */ - if self.clause[ci].is(FlagClause::FORWD_LINK) - || self.clause[ci].is(FlagClause::BCKWD_LINK) - { + let fwd = self.clause[ci].is(FlagClause::FORWD_LINK); + if fwd { self.clause[ci].turn_off(FlagClause::FORWD_LINK); + } + let bck = self.clause[ci].is(FlagClause::BCKWD_LINK); + if bck { self.clause[ci].turn_off(FlagClause::BCKWD_LINK); + } + let new = self.clause[ci].is(FlagClause::NEW_CLAUSE); + if new { + self.clause[ci].turn_off(FlagClause::NEW_CLAUSE); + } + if bck && new && self.clause[ci].rank <= (2 * threshold as DecisionLevel) / 3 { continue; } - /* let bwd: bool = self.clause[ci].is(FlagClause::BCKWD_LINK); - if bwd { - self.clause[ci].turn_off(FlagClause::BCKWD_LINK); - } */ - if self.clause[ci].is(FlagClause::LEARNT) { - let ClauseDB { - ref mut clause, - ref mut lbd_temp, - .. - } = self; - if clause[ci].rank < threshold as DecisionLevel { - continue; - } - clause[ci].update_lbd(asg, lbd_temp); - if threshold < clause[ci].extended_lbd() { - // keep -= 1; - // perm.push(OrderedProxy::new(ci, c.rank as f64)); - self.delete_clause(ci); - continue; - } + if new_assertion && self.clause[ci].is_satisfied_under(asg) { + self.delete_clause(ci); + continue; + } + if !self.clause[ci].is(FlagClause::LEARNT) { + continue; + } + // alives += 1; + // keep += 1; + if (threshold as DecisionLevel) < self.clause[ci].rank + /* extended_lbd() */ + { + // keep -= 1; + self.delete_clause(ci); } } - // let keep = perm.len().max(alives); - // if perm.is_empty() { - // return; - // } - // perm.sort(); - // let threshold = perm[keep.min(perm.len() - 1)].value(); - // for i in perm.iter().skip(keep) { - // // Being clause-position-independent, we keep or delete - // // all clauses that have a same value as a unit. - // if i.value() == threshold { - // continue; - // } - // self.delete_clause(i.to()); - // } } #[cfg(not(feature = "keep_just_used_clauses"))] #[allow(unreachable_code, unused_variables)] diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index d2a178f24..78f6e2c9f 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -36,7 +36,7 @@ impl VivifyIF for ClauseDB { let display_step: usize = 1000; let mut num_checked: usize = 0; let mut num_shrink: usize = 0; - let mut num_subsumed: usize = 0; + // let mut num_subsumed: usize = 0; let mut num_assert: usize = 0; let mut to_display: usize = 0; 'next_clause: while let Some(cp) = clauses.pop() { @@ -60,7 +60,7 @@ impl VivifyIF for ClauseDB { if to_display <= num_checked { state.flush(""); state.flush(format!( - "vivifying(assert:{num_assert} subsume:{num_subsumed}, shorten:{num_shrink}, check:{num_checked}/{num_target})..." + "vivifying(assert:{num_assert}, shorten:{num_shrink}, check:{num_checked}/{num_target})..." )); to_display = num_checked + display_step; } @@ -102,18 +102,21 @@ impl VivifyIF for ClauseDB { } } AssignReason::Implication(wli) => { - if wli.as_ci() != ci && decisions.len() <= clits.len() - // && self.clause[wli.as_ci()].len() <= clits.len() - { - debug_assert!(!self.clause[wli.as_ci()].is_dead()); - debug_assert!(!self.clause[ci].is_dead()); + if wli.as_ci() != ci { asg.backtrack_sandbox(); - self.delete_clause(ci); - if !is_learnt && self.clause[wli.as_ci()].is(FlagClause::LEARNT) + /* if decisions.len() < clits.len() + && self.clause[wli.as_ci()] + .iter() + .all(|l| decisions.contains(l)) { - self.clause[wli.as_ci()].turn_off(FlagClause::LEARNT); - } - num_subsumed += 1; + self.delete_clause(ci); + if !is_learnt + && self.clause[wli.as_ci()].is(FlagClause::LEARNT) + { + self.clause[wli.as_ci()].turn_off(FlagClause::LEARNT); + } + num_subsumed += 1; + } */ continue 'next_clause; } if wli.as_ci() == ci && clits.len() == decisions.len() { @@ -145,6 +148,7 @@ impl VivifyIF for ClauseDB { 1 => { self.certificate_add_assertion(vec[0]); asg.assign_at_root_level(vec[0])?; + state.stm.handle(SolverEvent::Assert(vec[0].vi())); num_assert += 1; } _ => { @@ -155,7 +159,7 @@ impl VivifyIF for ClauseDB { } #[cfg(not(feature = "clause_rewarding"))] self.new_clause(asg, &mut vec, is_learnt); - // propage_sandbox can't handle dead watchers correctly + // propagate_sandbox can't handle dead watchers correctly self.delete_clause(ci); num_shrink += 1; } @@ -178,7 +182,7 @@ impl VivifyIF for ClauseDB { debug_assert!(asg.stack_is_empty() || !asg.remains()); state.flush(""); state.flush(format!( - "vivified(assert:{num_assert}, subsume:{num_subsumed}, shorten:{num_shrink}), " + "vivified(assert:{num_assert}, shorten:{num_shrink}), " )); // state.log( // asg.num_conflict, diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index 7117c7b43..cb86c8e2f 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -167,6 +167,7 @@ pub fn eliminate_var( */ elim[vi].clear(); asg.handle(SolverEvent::Eliminate(vi)); + state.stm.handle(SolverEvent::Eliminate(vi)); elim.backward_subsumption_check(asg, cdb) } diff --git a/src/processor/mod.rs b/src/processor/mod.rs index 61b179c26..afe79ac0a 100644 --- a/src/processor/mod.rs +++ b/src/processor/mod.rs @@ -41,7 +41,7 @@ use { /// use crate::{splr::config::Config, splr::types::*}; /// use crate::splr::processor::{Eliminator, EliminateIF}; /// use crate::splr::solver::Solver; - +/// /// let mut s = Solver::instantiate(&Config::default(), &CNFDescription::default()); /// let mut elim = Eliminator::instantiate(&s.state.config, &s.state.cnf); /// assert_eq!(elim.is_running(), false); diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs index aa288c214..2e27e271f 100644 --- a/src/processor/simplify.rs +++ b/src/processor/simplify.rs @@ -513,7 +513,7 @@ impl Eliminator { /// /// clause queue operations /// - + /// /// enqueue a clause into eliminator's clause queue. pub fn enqueue_clause(&mut self, ci: ClauseIndex, c: &mut Clause) { if self.mode != EliminatorMode::Running @@ -540,7 +540,7 @@ impl Eliminator { /// /// var queue operations /// - + /// /// clear eliminator's var queue fn clear_var_queue(&mut self, asg: &mut impl AssignIF) { self.var_queue.clear(asg); diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 3d6963139..17dca4dd1 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -102,7 +102,7 @@ pub fn handle_conflict( match asg.assigned(l0) { Some(true) if asg.level(l0.vi()) == root_level => { // dbg!("double assignment occured"); - return Ok(root_level); + return Ok(0); } Some(false) if asg.level(l0.vi()) == root_level => { return Err(SolverError::RootLevelConflict((l0, asg.reason(l0.vi())))); @@ -115,7 +115,7 @@ pub fn handle_conflict( } let vi = l0.vi(); cdb.handle(SolverEvent::Assert(vi)); - return Ok(asg.root_level()); + return Ok(0); } } } @@ -376,8 +376,11 @@ fn conflict_analyze( } if max_lbd < cdb[ci].rank { - max_lbd = cdb[ci].rank; - ci_with_max_lbd = Some(ci); + let r = cdb.update_lbd(asg, ci); + if max_lbd < r { + max_lbd = r; + ci_with_max_lbd = Some(ci); + } } assert_eq!( p, diff --git a/src/solver/search.rs b/src/solver/search.rs index f879c6d54..14658dc53 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -15,7 +15,11 @@ const STAGE_SIZE: usize = 32; #[derive(Debug, Default, PartialEq, PartialOrd)] pub struct SearchState { num_reduction: usize, + new_assertion: bool, reduce_step: usize, + last_restart: usize, + next_restart: usize, + restart_threshold: f64, next_reduce: usize, current_core: usize, current_span: usize, @@ -63,6 +67,7 @@ pub trait SolveIF { macro_rules! RESTART { ($asg: expr, $cdb: expr, $state: expr) => { $asg.cancel_until($asg.root_level()); + $asg.handle(SolverEvent::Restart); $cdb.handle(SolverEvent::Restart); $state.handle(SolverEvent::Restart); }; @@ -422,8 +427,12 @@ impl SolveIF for Solver { Ok(SearchState { num_reduction: 0, + new_assertion: false, reduce_step: (nv + nc) as usize, next_reduce: 64, + last_restart: 0, + next_restart: 1024, + restart_threshold: 1.25, from_segment_beginning: 0, current_core: asg.derefer(assign::property::Tusize::NumUnassertedVar), current_span: 1, @@ -438,6 +447,9 @@ impl SolveIF for Solver { }) } fn search_stage(&mut self, ss: &mut SearchState) -> Result, SolverError> { + fn sgm(x: f64) -> f64 { + 1.0 / (1.0 + (-x).exp()) + } // main loop; returns `Ok(true)` for SAT, `Ok(false)` for UNSAT. let Solver { ref mut asg, @@ -462,18 +474,41 @@ impl SolveIF for Solver { #[cfg(feature = "clause_rewarding")] cdb.update_activity_tick(); - if asg.root_level() == handle_conflict(asg, cdb, state, &cc)? { - // let nv: u32 = asg.derefer(assign::Tusize::NumUnassertedVar).ilog2(); - // let nc: u32 = cdb - // .iter() - // .filter(|c| !c.is_dead() && 2 < c.len()) - // .count() - // .ilog2(); - // ss.reduce_step = ((nv + nc) as usize + ss.reduce_step) / 2; + let _last_activity: Option = match handle_conflict(asg, cdb, state, &cc)? { + 0 => { + state.stm.handle(SolverEvent::Assert(0)); + ss.new_assertion = true; + None + } + _ => { + let act: f64 = asg.var(asg.stack(asg.stack_len() - 1).vi()).activity(); + state.refinement_ema.update(act); + Some(act) + } + }; + let num_conflict = asg.derefer(assign::Tusize::NumConflict); + let _dist = (num_conflict - ss.last_restart).ilog10() as f64; + let lbd_trend = cdb.refer(cdb::property::TEma::LBD).trend(); + // let with_restart = 0.95 + 0.25 / (dist + 1.0) <= lbd_trend; + // let with_restart = ss.restart_threshold <= lbd_trend; + let ref_trend = state.refinement_ema.trend(); + let with_restart = + ss.restart_threshold < lbd_trend && ref_trend.clamp(0.75, 1.25) == ref_trend; + /* ss.restart_threshold <= lbd_trend || */ + // state.refinement_ema.trend() > 1.15; + // && last_activity.map_or(false, |a| a < state.refinement_ema.get()); + if with_restart { + RESTART!(asg, cdb, state); + ss.last_restart = num_conflict; + ss.restart_threshold = 1.25; + asg.clear_asserted_literals(cdb)?; + #[cfg(feature = "trace_equivalency")] + cdb.check_consistency(asg, "before simplify"); + } else { + ss.restart_threshold *= 0.99; } ss.from_segment_beginning += 1; if ss.current_span <= ss.from_segment_beginning { - let with_restart = 1.0 < cdb.refer(cdb::property::TEma::LBD).trend(); ss.from_segment_beginning = 0; #[cfg(feature = "graph_view")] @@ -482,83 +517,61 @@ impl SolveIF for Solver { let next_stage: Option = state .stm .prepare_new_stage(asg.derefer(assign::Tusize::NumConflict)); - if with_restart || next_stage.is_some() { - RESTART!(asg, cdb, state); - - #[cfg(any(feature = "best_phases_tracking", feature = "rephase"))] - if ss.with_rephase { - asg.select_rephasing_target(); - asg.clear_asserted_literals(cdb)?; - if next_stage == Some(true) { - ss.with_rephase = false; - } - } - - #[cfg(feature = "trace_equivalency")] - cdb.check_consistency(asg, "before simplify"); - } ss.current_span = state.stm.current_span() as usize; let scale = state.stm.current_scale(); asg.handle(SolverEvent::Stage(scale)); if let Some(new_segment) = next_stage { - // a beginning of a new cycle - { - let stm = &state.stm; - let b: f64 = stm.segment_starting_cycle() as f64; - let n: f64 = stm.current_cycle() as f64 - b; - - if cfg!(feature = "reward_annealing") { - let k: f64 = (stm.current_segment() as f64).log2(); - let ratio: f64 = stm.segment_progress_ratio(); - const SLOP: f64 = 8.0; - const R: (f64, f64) = (0.84, 0.995); - let d: f64 = R.1 - (R.1 - R.0) * SLOP / (k + SLOP); - let x: f64 = k * (2.0 * ratio - 1.0); - let r = { - let sgm = |x: f64| 1.0 / (1.0 + (-x).exp()); - d + sgm(x) * (1.0 - d) - }; - asg.update_activity_decay(r); + let num_restart = asg.derefer(assign::Tusize::NumRestart); + if ss.next_reduce <= num_restart { + if !with_restart { + RESTART!(asg, cdb, state); + asg.clear_asserted_literals(cdb)?; } - - let num_restart = asg.derefer(assign::Tusize::NumRestart); - if ss.next_reduce <= num_restart { - let ent: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow(); - let lbd: f64 = cdb.refer(cdb::property::TEma::LBD).get_slow(); - // Note: val can be inf. It got better results. - let val: f64 = 0.5 * ent.min(lbd) + ent.max(lbd) / (1.0 + n).log2(); - state.reduction_threshold = val; - cdb.reduce(asg, val); - ss.num_reduction += 1; - ss.reduce_step += 1; - ss.next_reduce = ss.reduce_step + num_restart; - - if cfg!(feature = "clause_vivification") { - cdb.vivify(asg, state)?; - } - if cfg!(feature = "clause_elimination") - && !cfg!(feature = "incremental_solver") - && ss.num_reduction % 8 == 0 - { - 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()); - state[Stat::Simplify] += 1; - state[Stat::SubsumedClause] = elim.num_subsumed; + let ents: f64 = cdb.refer(cdb::property::TEma::Entanglement).get_slow(); + // let threshold = 12.0 / (state.stm.current_segment() as f64).sqrt(); + let threshold = (2.0 / state.stm.segment_progress_ratio()).min(ents.sqrt()); + state.reduction_threshold = threshold; + cdb.reduce(asg, threshold, ss.new_assertion); + ss.new_assertion = false; + ss.num_reduction += 1; + ss.reduce_step += ss.current_core.ilog2() as usize; + ss.next_reduce = ss.reduce_step + num_restart; + if cfg!(feature = "clause_vivification") && ss.num_reduction % 6 == 0 { + cdb.vivify(asg, state)?; + } + if cfg!(feature = "clause_elimination") + && !cfg!(feature = "incremental_solver") + && ss.num_reduction % 24 == 0 + { + let mut elim = Eliminator::instantiate(&state.config, &state.cnf); + state.flush("clause subsumption, "); + elim.simplify(asg, cdb, state, false)?; + let el = elim.eliminated_lits(); + if !el.is_empty() { + asg.eliminated.append(el); } + state[Stat::Simplify] += 1; + state[Stat::SubsumedClause] = elim.num_subsumed; } } + // a beginning of a new cycle + let stm = &state.stm; + if cfg!(feature = "reward_annealing") { + // let k: f64 = (stm.current_segment() as f64).log2(); + let k: f64 = (stm.current_segment() as f64).sqrt(); + let ratio: f64 = stm.segment_progress_ratio(); + const R: (f64, f64) = (0.96, 1.0); + let x: f64 = k * (2.0 * ratio - 1.0); + let r = { + let s = sgm(x); + (1.0 - s) * R.0 + s * R.1 + }; + asg.update_activity_decay(r); + } state .stm .set_span_base(state.c_lvl.get_slow() - state.b_lvl.get_slow()); - - asg.clear_asserted_literals(cdb)?; dump_stage(asg, cdb, state, &ss.previous_stage); - - #[cfg(feature = "rephase")] - rephase(asg, cdb, state, ss); - if new_segment { state.exploration_rate_ema.update(1.0); } @@ -577,6 +590,11 @@ impl SolveIF for Solver { return Err(SolverError::UndescribedError); } } + #[cfg(feature = "rephase")] + if with_restart { + asg.select_rephasing_target(); + rephase(asg, cdb, state, ss); + } } if let Some(na) = asg.best_assigned() { if ss.current_core < na && ss.core_was_rebuilt.is_none() { diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 03f3e3d32..541d7aeb2 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -49,8 +49,11 @@ impl Instantiate for StageManager { ..StageManager::default() } } - fn handle(&mut self, _: SolverEvent) { - unimplemented!(); + fn handle(&mut self, e: SolverEvent) { + match e { + SolverEvent::Assert(_) | SolverEvent::Eliminate(_) => self.reset(), + _ => (), + } } } diff --git a/src/state.rs b/src/state.rs index 15f146f80..5296cc78b 100644 --- a/src/state.rs +++ b/src/state.rs @@ -97,6 +97,8 @@ pub struct State { pub b_lvl: Ema2, /// EMA of conflicting levels pub c_lvl: Ema2, + /// EMA of a sort of refinement + pub refinement_ema: Ema2, /// EMA of c_lbd - b_lbd, or Exploration vs. Eploitation pub e_mode: Ema2, pub e_mode_threshold: f64, @@ -146,6 +148,7 @@ impl Default for State { b_lvl: Ema2::new(16).with_slow(4096), c_lvl: Ema2::new(16).with_slow(4096), + refinement_ema: Ema2::new(16).with_slow(4096), e_mode: Ema2::new(32).with_slow(4096).with_value(10.0), e_mode_threshold: 1.20, exploration_rate_ema: Ema::new(1000),