diff --git a/Cargo.lock b/Cargo.lock index 544fb3a1b..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.12" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a73e9fe3c49d7afb2ace819fa181a287ce54a0983eda4e0eb05c22f82ffe534" +checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674" [[package]] name = "js-sys" @@ -257,9 +257,9 @@ dependencies = [ [[package]] name = "libc" -version = "0.2.164" +version = "0.2.166" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "433bfe06b8c75da9b2e3fbea6e5329ff87748f0b144ef75306e674c3f6f7c13f" +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", ] @@ -430,7 +430,7 @@ dependencies = [ "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", @@ -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/cdb/mod.rs b/src/cdb/mod.rs index 55251307e..f8e38b179 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -569,7 +569,7 @@ impl ClauseDBIF for ClauseDB { if new { self.clause[ci].turn_off(FlagClause::NEW_CLAUSE); } - if bck { + if bck && new && self.clause[ci].rank <= (2 * threshold as DecisionLevel) / 3 { continue; } if new_assertion && self.clause[ci].is_satisfied_under(asg) { 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/search.rs b/src/solver/search.rs index 32fdc7e2d..14658dc53 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -17,7 +17,9 @@ 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, @@ -428,7 +430,9 @@ impl SolveIF for Solver { 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, @@ -443,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, @@ -467,27 +474,38 @@ impl SolveIF for Solver { #[cfg(feature = "clause_rewarding")] cdb.update_activity_tick(); - match handle_conflict(asg, cdb, state, &cc)? { + let _last_activity: Option = match handle_conflict(asg, cdb, state, &cc)? { 0 => { state.stm.handle(SolverEvent::Assert(0)); ss.new_assertion = true; + None } - 1 => (), // ss.next_reduce = 0, - _ => (), - } + _ => { + 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 with_restart = /* ss.next_restart <= num_conflict - && */ 1.2 <= cdb.refer(cdb::property::TEma::LBD).trend(); + 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)?; - // ss.next_restart = num_conflict + 12; #[cfg(feature = "trace_equivalency")] cdb.check_consistency(asg, "before simplify"); - } else if ss.next_restart <= num_conflict - && cdb.refer(cdb::property::TEma::LBD).trend() <= 0.75 - { - // ss.next_restart = num_conflict + 4; + } else { + ss.restart_threshold *= 0.99; } ss.from_segment_beginning += 1; if ss.current_span <= ss.from_segment_beginning { @@ -509,7 +527,6 @@ impl SolveIF for Solver { RESTART!(asg, cdb, state); asg.clear_asserted_literals(cdb)?; } - let _lbd = cdb.refer(cdb::property::TEma::LBD).get(); 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()); @@ -543,11 +560,11 @@ impl SolveIF for Solver { // 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.95, 0.99); + const R: (f64, f64) = (0.96, 1.0); let x: f64 = k * (2.0 * ratio - 1.0); let r = { - let sgm = 1.0 / (1.0 + (-x).exp()); - (1.0 - sgm) * R.0 + sgm * R.1 + let s = sgm(x); + (1.0 - s) * R.0 + s * R.1 }; asg.update_activity_decay(r); } 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),