From e51c883e8bd4d8e3942346e62aa379286450b211 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 11 Oct 2022 10:11:14 +0900 Subject: [PATCH 01/29] the initial implementation of SLS --- Cargo.toml | 2 +- src/cdb/mod.rs | 2 ++ src/cdb/sls.rs | 45 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 48 insertions(+), 1 deletion(-) create mode 100644 src/cdb/sls.rs diff --git a/Cargo.toml b/Cargo.toml index a26420159..c3ebaa6c3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "splr" -version = "0.17.0-alpha.2" +version = "0.17.0-alpha.3" authors = ["Narazaki Shuji "] description = "A modern CDCL SAT solver in Rust" edition = "2021" diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 2eb084fed..dc1e32a6b 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -10,6 +10,8 @@ mod clause; mod db; /// EMA mod ema; +/// methods for Stochastic Local Search +mod sls; /// methods for UNSAT certification mod unsat_certificate; /// implementation of clause vivification diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs new file mode 100644 index 000000000..752deee98 --- /dev/null +++ b/src/cdb/sls.rs @@ -0,0 +1,45 @@ +/// Implementation of Stochastic Local Search +use {crate::types::*, std::collections::HashMap}; + +pub trait StochasticLocalSearchIF { + fn stochastic_local_search(&mut self, start: &[Option], limit: usize) -> Vec; +} + +impl StochasticLocalSearchIF for ClauseDB { + fn stochastic_local_search(&mut self, start: &[Option], limit: usize) -> Vec { + let mut assignment: Vec = start + .iter() + .map(|a| a.map_or(false, |b| b)) + .collect::>(); + for _ in 0..limit { + let mut flip_target: HashMap = HashMap::new(); + let mut satisfied = true; + for c in self + .clause + .iter() + .skip(1) + .filter(|c| !c.is(FlagClause::LEARNT)) + { + satisfied &= c.check_parity(&assignment, &mut flip_target); + } + if satisfied { + return assignment; + } + let i: usize = flip_target.iter().map(|(k, v)| (*v, *k)).max().unwrap().1; + assignment[i] = !assignment[i]; + } + assignment + } +} + +impl Clause { + fn check_parity(&self, assignment: &[bool], flip_target: &mut HashMap) -> bool { + for l in self.iter() { + let vi = l.vi(); + if assignment[vi] != l.as_bool() { + *flip_target.entry(vi).or_insert(0) += 1; + } + } + todo!(); + } +} From 1f52bdb407b6778e24b559aab484148d9dcb89ea Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 11 Oct 2022 10:17:31 +0900 Subject: [PATCH 02/29] add new feature 'stochastic_local_search' --- Cargo.toml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cargo.toml b/Cargo.toml index c3ebaa6c3..dcec191ec 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -29,6 +29,7 @@ default = [ "reason_side_rewarding", "rephase", # "reward_annealing", # for big problems since 0.17(need to evalate with larger timeout) + "stochastic_local_search", # since 0.17 # "suppress_reason_chain", "trail_saving", "unsafe_access" @@ -53,6 +54,7 @@ no_IO = [] reason_side_rewarding = [] rephase = ["best_phases_tracking"] reward_annealing = [] +stochastic_local_search = [] support_user_assumption = [] suppress_reason_chain = [] trace_analysis = [] From 5615de35a3e4f34a3f2a624c1459f4e8677b4a67 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 11 Oct 2022 10:33:12 +0900 Subject: [PATCH 03/29] wiring --- src/cdb/mod.rs | 4 ++++ src/solver/search.rs | 15 ++++++++++++++- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index dc1e32a6b..cd53af263 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -10,6 +10,7 @@ mod clause; mod db; /// EMA mod ema; +#[cfg(feature = "stochastic_local_search")] /// methods for Stochastic Local Search mod sls; /// methods for UNSAT certification @@ -26,6 +27,9 @@ pub use self::{ unsat_certificate::CertificationStore, vivify::VivifyIF, }; +#[cfg(feature = "stochastic_local_search")] +pub use sls::StochasticLocalSearchIF; + use { self::ema::ProgressLBD, crate::{assign::AssignIF, types::*}, diff --git a/src/solver/search.rs b/src/solver/search.rs index 3e2492607..d1c76c3aa 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -287,7 +287,20 @@ fn search( } if let Some(new_segment) = next_stage { #[cfg(feature = "rephase")] - asg.select_rephasing_target(); + { + #[cfg(feature = "stochastic_local_search")] + { + use cdb::StochasticLocalSearchIF; + let limit = 100; // FIXME: use entanglement + + let _assignment = cdb.stochastic_local_search(asg.assign_ref(), limit); + // asg.select_rephasing_target(Some(assignment)); + } + #[cfg(not(feature = "stochastic_local_search"))] + { + asg.select_rephasing_target(); + } + } if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; } From 9f9e2c966ad07a69be17874c54a325ad2e8c125c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 11 Oct 2022 10:44:09 +0900 Subject: [PATCH 04/29] ditto --- src/assign/select.rs | 11 +++++++++-- src/solver/search.rs | 15 ++++++++++----- 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index 4ef766f61..e2a94ccf7 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -28,7 +28,7 @@ macro_rules! var_assign { pub trait VarSelectIF { #[cfg(feature = "rephase")] /// select rephasing target - fn select_rephasing_target(&mut self); + fn select_rephasing_target(&mut self, assignment: Option>); #[cfg(feature = "rephase")] /// check the consistency fn check_consistency_of_best_phases(&mut self); @@ -42,7 +42,14 @@ pub trait VarSelectIF { impl VarSelectIF for AssignStack { #[cfg(feature = "rephase")] - fn select_rephasing_target(&mut self) { + fn select_rephasing_target(&mut self, assignment: Option>) { + if let Some(assignment) = assignment { + for (vi, b) in assignment.iter().enumerate().skip(1) { + let v = &mut self.var[vi]; + v.set(FlagVar::PHASE, *b); + } + return; + } if self.best_phases.is_empty() { return; } diff --git a/src/solver/search.rs b/src/solver/search.rs index d1c76c3aa..81f1aab79 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -291,14 +291,19 @@ fn search( #[cfg(feature = "stochastic_local_search")] { use cdb::StochasticLocalSearchIF; - let limit = 100; // FIXME: use entanglement - - let _assignment = cdb.stochastic_local_search(asg.assign_ref(), limit); - // asg.select_rephasing_target(Some(assignment)); + let entanglement = cdb.refer(cdb::property::TEma::Entanglement).get(); + if 16.0 < entanglement { + let limit = entanglement.powi(2) as usize; + let assignment = + cdb.stochastic_local_search(asg.assign_ref(), limit); + asg.select_rephasing_target(Some(assignment)); + } else { + asg.select_rephasing_target(None); + } } #[cfg(not(feature = "stochastic_local_search"))] { - asg.select_rephasing_target(); + asg.select_rephasing_target(None); } } if cfg!(feature = "clause_vivification") { From d10a3a211ea3bee1128305153a31274ba29c6275 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 13 Oct 2022 08:04:07 +0900 Subject: [PATCH 05/29] a snapshot --- Cargo.toml | 2 +- src/assign/select.rs | 33 ++++++++++++--- src/cdb/sls.rs | 95 +++++++++++++++++++++++++++++++++++--------- src/solver/search.rs | 49 +++++++++++++---------- src/solver/stage.rs | 2 +- src/state.rs | 13 ++++-- 6 files changed, 145 insertions(+), 49 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index dcec191ec..33614a966 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -28,7 +28,7 @@ default = [ # "maintain_watch_cache", # for DEBUG "reason_side_rewarding", "rephase", - # "reward_annealing", # for big problems since 0.17(need to evalate with larger timeout) + "reward_annealing", # for big problems since 0.17(need to evalate with larger timeout) "stochastic_local_search", # since 0.17 # "suppress_reason_chain", "trail_saving", diff --git a/src/assign/select.rs b/src/assign/select.rs index e2a94ccf7..d72a48630 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -1,7 +1,7 @@ /// Decision var selection #[cfg(feature = "rephase")] -use super::property; +use {super::property, std::collections::HashMap}; use { super::{AssignStack, VarHeapIF}, @@ -26,9 +26,12 @@ macro_rules! var_assign { /// API for var selection, depending on an internal heap. pub trait VarSelectIF { + #[cfg(feature = "rephase")] + /// return best phases + fn best_phases_ref(&mut self) -> HashMap; #[cfg(feature = "rephase")] /// select rephasing target - fn select_rephasing_target(&mut self, assignment: Option>); + fn select_rephasing_target(&mut self, assignment: Option>); #[cfg(feature = "rephase")] /// check the consistency fn check_consistency_of_best_phases(&mut self); @@ -42,11 +45,31 @@ pub trait VarSelectIF { impl VarSelectIF for AssignStack { #[cfg(feature = "rephase")] - fn select_rephasing_target(&mut self, assignment: Option>) { + fn best_phases_ref(&mut self) -> HashMap { + self.var + .iter() + .enumerate() + .filter_map(|(vi, v)| { + if self.level[vi] == self.root_level || self.var[vi].is(FlagVar::ELIMINATED) { + None + } else { + Some(( + vi, + self.best_phases + .get(&vi) + .map_or(v.is(FlagVar::PHASE), |(b, _)| *b), + )) + } + }) + .collect::>() + } + #[cfg(feature = "rephase")] + fn select_rephasing_target(&mut self, assignment: Option>) { if let Some(assignment) = assignment { - for (vi, b) in assignment.iter().enumerate().skip(1) { - let v = &mut self.var[vi]; + for (vi, b) in assignment.iter() { + let v = &mut self.var[*vi]; v.set(FlagVar::PHASE, *b); + self.best_phases.insert(*vi, (*b, AssignReason::None)); } return; } diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs index 752deee98..03dc8d717 100644 --- a/src/cdb/sls.rs +++ b/src/cdb/sls.rs @@ -2,44 +2,101 @@ use {crate::types::*, std::collections::HashMap}; pub trait StochasticLocalSearchIF { - fn stochastic_local_search(&mut self, start: &[Option], limit: usize) -> Vec; + fn stochastic_local_search( + &mut self, + start: &mut HashMap, + limit: usize, + ) -> (usize, usize); } impl StochasticLocalSearchIF for ClauseDB { - fn stochastic_local_search(&mut self, start: &[Option], limit: usize) -> Vec { - let mut assignment: Vec = start - .iter() - .map(|a| a.map_or(false, |b| b)) - .collect::>(); - for _ in 0..limit { + fn stochastic_local_search( + &mut self, + assignment: &mut HashMap, + limit: usize, + ) -> (usize, usize) { + let mut returns = (0, 0); + let mut last_flip = 0; + for step in 0..limit { + let mut unsat_clauses = 0; let mut flip_target: HashMap = HashMap::new(); - let mut satisfied = true; + let mut target_clause: Option<&Clause> = None; for c in self .clause .iter() .skip(1) - .filter(|c| !c.is(FlagClause::LEARNT)) + .rev() + .filter(|c| /* !c.is(FlagClause::LEARNT) && */ !c.is_dead()) { - satisfied &= c.check_parity(&assignment, &mut flip_target); + let result = c.check_parity(assignment, &mut flip_target); + if let Some(c) = result { + unsat_clauses += 1; + if target_clause.is_none() || unsat_clauses == step { + target_clause = result; + for l in c.lits.iter() { + flip_target.entry(l.vi()).or_insert(0); + } + } + } } - if satisfied { - return assignment; + if step == 1 { + returns = (unsat_clauses, unsat_clauses); + } + returns.1 = unsat_clauses; + if let Some(c) = target_clause { + let factor = |vi| 1.4_f64.powf(-(*flip_target.get(vi).unwrap() as f64)); + let vars = c.lits.iter().map(|l| l.vi()).collect::>(); + let index = (((step + last_flip) & 63) as f64 / 63.0) + * vars.iter().map(factor).sum::(); + let mut sum: f64 = 0.0; + for vi in vars.iter() { + sum += factor(vi); + if index <= sum { + // print!( + // "step {step}: flip {} of {}| {}", + // vi, + // c.lits.len(), + // assignment[vi] + // ); + assignment.entry(*vi).and_modify(|e| *e = !*e); + // print1ln!(" -> {}", assignment[vi]); + last_flip = *vi; + break; + } + } + } else { + return returns; } - let i: usize = flip_target.iter().map(|(k, v)| (*v, *k)).max().unwrap().1; - assignment[i] = !assignment[i]; } - assignment + returns } } impl Clause { - fn check_parity(&self, assignment: &[bool], flip_target: &mut HashMap) -> bool { + fn check_parity( + &self, + assignment: &mut HashMap, + flip_target: &mut HashMap, + ) -> Option<&Self> { + let mut num_sat = 0; + let mut sat_vi = 0; for l in self.iter() { let vi = l.vi(); - if assignment[vi] != l.as_bool() { - *flip_target.entry(vi).or_insert(0) += 1; + match assignment.get(&vi) { + None => { + // println!("{:?}|{:?}", l, self); + return None; + } + Some(b) if *b == l.as_bool() => { + num_sat += 1; + sat_vi = vi; + } + _ => (), } } - todo!(); + if num_sat == 1 { + *flip_target.entry(sat_vi).or_insert(0) += 1; + } + (0 == num_sat).then_some(self) } } diff --git a/src/solver/search.rs b/src/solver/search.rs index 81f1aab79..875904ca8 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -286,26 +286,7 @@ fn search( asg.update_activity_decay(decay); } if let Some(new_segment) = next_stage { - #[cfg(feature = "rephase")] - { - #[cfg(feature = "stochastic_local_search")] - { - use cdb::StochasticLocalSearchIF; - let entanglement = cdb.refer(cdb::property::TEma::Entanglement).get(); - if 16.0 < entanglement { - let limit = entanglement.powi(2) as usize; - let assignment = - cdb.stochastic_local_search(asg.assign_ref(), limit); - asg.select_rephasing_target(Some(assignment)); - } else { - asg.select_rephasing_target(None); - } - } - #[cfg(not(feature = "stochastic_local_search"))] - { - asg.select_rephasing_target(None); - } - } + // a beginning of a new cycle if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; } @@ -323,6 +304,34 @@ fn search( state.restart.set_segment_parameters(max_scale); } } + #[cfg(feature = "rephase")] + if new_segment + || 2.5 < asg.refer(assign::property::TEma::DecisionPerConflict).get() + { + #[cfg(feature = "stochastic_local_search")] + { + use cdb::StochasticLocalSearchIF; + let num_falsified = &mut state.stats[Stat::UnsatsBySLS]; + let entanglement = cdb.refer(cdb::property::TEma::Entanglement).get(); + if 120.0 / (*num_falsified as f64).log2() < entanglement { + let limit = entanglement as usize; + // debug_assert_eq!(asg.decision_level(), asg.root_level()); + let mut assignment = asg.best_phases_ref(); + let stats = cdb.stochastic_local_search(&mut assignment, limit); + *num_falsified = stats.1; + state.log(None, format!("SLS:: {} => {}", stats.0, stats.1)); + asg.select_rephasing_target( + (stats.1 < stats.0).then_some(assignment), + ); + } else { + asg.select_rephasing_target(None); + } + } + #[cfg(not(feature = "stochastic_local_search"))] + { + asg.select_rephasing_target(None); + } + } } asg.clear_asserted_literals(cdb)?; state.progress(asg, cdb); diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 429c5670c..6e2836dec 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -50,7 +50,7 @@ impl StageManager { self.end_of_stage = unit_size; } /// returns: - /// - Some(true): it's a beginning of a new cycle and a new cycle, a 2nd-level group. + /// - Some(true): it's a beginning of a new cycle and a new segment, a 2nd-level group. /// - Some(false): a beginning of a new cycle. /// - None: the other case. pub fn prepare_new_stage(&mut self, rescale: usize, now: usize) -> Option { diff --git a/src/state.rs b/src/state.rs index 3d979c16c..899a0e353 100644 --- a/src/state.rs +++ b/src/state.rs @@ -51,6 +51,8 @@ pub enum Stat { Simplify, /// the number of subsumed clause by processor SubsumedClause, + /// SLS core + UnsatsBySLS, /// don't use this dummy (sentinel at the tail). EndOfStatIndex, } @@ -512,7 +514,7 @@ impl StateIF for State { ), ); println!( - "\x1B[2K misc|vivC:{}, subC:{}, core:{}, /ppc:{}", + "\x1B[2K misc|vivC:{}, -SLS:{}, core:{}, /ppc:{}", im!( "{:>9}", self, @@ -522,8 +524,8 @@ impl StateIF for State { im!( "{:>9}", self, - LogUsizeId::SubsumedClause, - self[Stat::SubsumedClause] + LogUsizeId::UnsatsBySLS, + self[Stat::UnsatsBySLS] ), im!( "{:>9}", @@ -835,6 +837,11 @@ pub enum LogUsizeId { VivifiedVar, Vivify, + // + //## Stochastic Local Search + // + UnsatsBySLS, + // the sentinel End, } From 3b9dc5d42565d951496981d70ab99f457b3ed7c3 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 13 Oct 2022 22:30:47 +0900 Subject: [PATCH 06/29] Better results --- src/solver/search.rs | 52 +++++++++++++++++++++----------------------- 1 file changed, 25 insertions(+), 27 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index 875904ca8..707ee2da1 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -305,32 +305,8 @@ fn search( } } #[cfg(feature = "rephase")] - if new_segment - || 2.5 < asg.refer(assign::property::TEma::DecisionPerConflict).get() { - #[cfg(feature = "stochastic_local_search")] - { - use cdb::StochasticLocalSearchIF; - let num_falsified = &mut state.stats[Stat::UnsatsBySLS]; - let entanglement = cdb.refer(cdb::property::TEma::Entanglement).get(); - if 120.0 / (*num_falsified as f64).log2() < entanglement { - let limit = entanglement as usize; - // debug_assert_eq!(asg.decision_level(), asg.root_level()); - let mut assignment = asg.best_phases_ref(); - let stats = cdb.stochastic_local_search(&mut assignment, limit); - *num_falsified = stats.1; - state.log(None, format!("SLS:: {} => {}", stats.0, stats.1)); - asg.select_rephasing_target( - (stats.1 < stats.0).then_some(assignment), - ); - } else { - asg.select_rephasing_target(None); - } - } - #[cfg(not(feature = "stochastic_local_search"))] - { - asg.select_rephasing_target(None); - } + asg.select_rephasing_target(None); } } asg.clear_asserted_literals(cdb)?; @@ -345,8 +321,30 @@ fn search( RESTART!(asg, cdb, state); } if let Some(na) = asg.best_assigned() { - state.flush(""); - state.flush(format!("unreachable core: {}", na)); + #[cfg(feature = "stochastic_local_search")] + { + use cdb::StochasticLocalSearchIF; + let mut assignment = asg.best_phases_ref(); + let stats = cdb.stochastic_local_search(&mut assignment, 80); + state.flush(""); + if stats.1 < stats.0 { + state.stats[Stat::UnsatsBySLS] = stats.1; + state.flush(format!( + "unreachable core: {}, SLS: {} -> {}", + na, stats.0, stats.1 + )); + // We need to restart in order to try the whole assignment by SLS + RESTART!(asg, cdb, state); + asg.select_rephasing_target(Some(assignment)); + } else { + state.flush(format!("unreachable core: {}", na)); + } + } + #[cfg(not(feature = "stochastic_local_search"))] + { + state.flush(""); + state.flush(format!("unreachable core: {}", na)); + } } } } From 2d664422f7af89e5a73ee5925de435e97c8a636e Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Fri, 14 Oct 2022 20:12:25 +0900 Subject: [PATCH 07/29] a snapshot --- src/assign/select.rs | 8 ++++--- src/cdb/activity.rs | 4 ++++ src/cdb/db.rs | 2 +- src/cdb/sls.rs | 10 +++----- src/solver/search.rs | 57 ++++++++++++++++++++++---------------------- 5 files changed, 41 insertions(+), 40 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index d72a48630..0b400b5cd 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -55,9 +55,10 @@ impl VarSelectIF for AssignStack { } else { Some(( vi, - self.best_phases - .get(&vi) - .map_or(v.is(FlagVar::PHASE), |(b, _)| *b), + self.best_phases.get(&vi).map_or( + self.assign[vi].unwrap_or_else(|| v.is(FlagVar::PHASE)), + |(b, _)| *b, + ), )) } }) @@ -71,6 +72,7 @@ impl VarSelectIF for AssignStack { v.set(FlagVar::PHASE, *b); self.best_phases.insert(*vi, (*b, AssignReason::None)); } + self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars; return; } if self.best_phases.is_empty() { diff --git a/src/cdb/activity.rs b/src/cdb/activity.rs index e8c9fd900..67fb178fc 100644 --- a/src/cdb/activity.rs +++ b/src/cdb/activity.rs @@ -20,6 +20,10 @@ impl ActivityIF for ClauseDB { fn update_activity_tick(&mut self) { self.tick += 1; } + fn update_activity_decay(&mut self, decay: f64) { + self.activity_decay = decay; + self.activity_anti_decay = 1.0 - decay; + } } impl Clause { diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 7f6832a2a..4cf2cdeba 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -953,8 +953,8 @@ impl ClauseDBIF for ClauseDB { let act_c = self.reward; #[cfg(not(feature = "clause_rewarding"))] let act_c = 0.25; - self.rank as f64 / (act_c + act_v) + // (self.rank as f64).log2().powf(1.0 - act_v) } #[cfg(feature = "just_used")] fn weight(&mut self, asg: &mut impl AssignIF) -> f64 { diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs index 03dc8d717..0bcc7e0d4 100644 --- a/src/cdb/sls.rs +++ b/src/cdb/sls.rs @@ -44,7 +44,7 @@ impl StochasticLocalSearchIF for ClauseDB { } returns.1 = unsat_clauses; if let Some(c) = target_clause { - let factor = |vi| 1.4_f64.powf(-(*flip_target.get(vi).unwrap() as f64)); + let factor = |vi| 3.2_f64.powf(-(*flip_target.get(vi).unwrap() as f64)); let vars = c.lits.iter().map(|l| l.vi()).collect::>(); let index = (((step + last_flip) & 63) as f64 / 63.0) * vars.iter().map(factor).sum::(); @@ -59,7 +59,6 @@ impl StochasticLocalSearchIF for ClauseDB { // assignment[vi] // ); assignment.entry(*vi).and_modify(|e| *e = !*e); - // print1ln!(" -> {}", assignment[vi]); last_flip = *vi; break; } @@ -75,7 +74,7 @@ impl StochasticLocalSearchIF for ClauseDB { impl Clause { fn check_parity( &self, - assignment: &mut HashMap, + assignment: &HashMap, flip_target: &mut HashMap, ) -> Option<&Self> { let mut num_sat = 0; @@ -83,14 +82,11 @@ impl Clause { for l in self.iter() { let vi = l.vi(); match assignment.get(&vi) { - None => { - // println!("{:?}|{:?}", l, self); - return None; - } Some(b) if *b == l.as_bool() => { num_sat += 1; sat_vi = vi; } + None => unreachable!(), _ => (), } } diff --git a/src/solver/search.rs b/src/solver/search.rs index 707ee2da1..ef009fe53 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,6 +239,7 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; + let mut best_phase_updated = false; state.stm.initialize( (asg.derefer(assign::property::Tusize::NumUnassertedVar) as f64).sqrt() as usize, @@ -267,6 +268,7 @@ fn search( return Err(SolverError::UndescribedError); } RESTART!(asg, cdb, state); + asg.clear_asserted_literals(cdb)?; cdb.reduce(asg, state.stm.num_reducible()); #[cfg(feature = "trace_equivalency")] cdb.check_consistency(asg, "before simplify"); @@ -290,6 +292,29 @@ fn search( if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; } + #[cfg(feature = "rephase")] + { + #[cfg(feature = "stochastic_local_search")] + if best_phase_updated { + best_phase_updated = false; + use cdb::StochasticLocalSearchIF; + let mut assignment = asg.best_phases_ref(); + let stats = cdb.stochastic_local_search(&mut assignment, 100); + if stats.1 < stats.0 { + state.stats[Stat::UnsatsBySLS] = stats.1; + state.flush(format!("SLS: {} -> {}", stats.0, stats.1)); + // We need to restart in order to try the whole assignment by SLS + RESTART!(asg, cdb, state); + asg.select_rephasing_target(Some(assignment)); + } + } else { + asg.select_rephasing_target(None); + } + #[cfg(not(feature = "stochastic_local_search"))] + { + asg.select_rephasing_target(None); + } + } if new_segment { #[cfg(not(feature = "reward_annealing"))] asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); @@ -304,12 +329,7 @@ fn search( state.restart.set_segment_parameters(max_scale); } } - #[cfg(feature = "rephase")] - { - asg.select_rephasing_target(None); - } } - asg.clear_asserted_literals(cdb)?; state.progress(asg, cdb); asg.handle(SolverEvent::Stage(scale)); state.restart.set_stage_parameters(scale); @@ -321,30 +341,9 @@ fn search( RESTART!(asg, cdb, state); } if let Some(na) = asg.best_assigned() { - #[cfg(feature = "stochastic_local_search")] - { - use cdb::StochasticLocalSearchIF; - let mut assignment = asg.best_phases_ref(); - let stats = cdb.stochastic_local_search(&mut assignment, 80); - state.flush(""); - if stats.1 < stats.0 { - state.stats[Stat::UnsatsBySLS] = stats.1; - state.flush(format!( - "unreachable core: {}, SLS: {} -> {}", - na, stats.0, stats.1 - )); - // We need to restart in order to try the whole assignment by SLS - RESTART!(asg, cdb, state); - asg.select_rephasing_target(Some(assignment)); - } else { - state.flush(format!("unreachable core: {}", na)); - } - } - #[cfg(not(feature = "stochastic_local_search"))] - { - state.flush(""); - state.flush(format!("unreachable core: {}", na)); - } + best_phase_updated = true; + state.flush(""); + state.flush(format!("unreachable core: {}", na)); } } } From 9b68d120cfc3803197fe4ae7e3fa73b5343359c2 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 16 Oct 2022 10:18:17 +0900 Subject: [PATCH 08/29] revert a meaningless change --- src/cdb/db.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 4cf2cdeba..7f6832a2a 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -953,8 +953,8 @@ impl ClauseDBIF for ClauseDB { let act_c = self.reward; #[cfg(not(feature = "clause_rewarding"))] let act_c = 0.25; + self.rank as f64 / (act_c + act_v) - // (self.rank as f64).log2().powf(1.0 - act_v) } #[cfg(feature = "just_used")] fn weight(&mut self, asg: &mut impl AssignIF) -> f64 { From ab87abcc51a8242e8fd03e2c46f0aa1a4f7e64df Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 16 Oct 2022 10:25:07 +0900 Subject: [PATCH 09/29] Cargo.toml: explain each of features --- Cargo.toml | 72 +++++++++++++++++++++++++++++------------------------- 1 file changed, 39 insertions(+), 33 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 33614a966..e97fce6d0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -17,51 +17,57 @@ bitflags = "^1.3" [features] default = [ - # "boundary_check", # for DEBUG - # "bi_clause_completion", # increase memory pressure + # "boundary_check", # for DEBUG + # "bi_clause_completion", # "no_clause_elimination", # "clause_rewarding", "clause_vivification", "dynamic_restart_threshold", # "incremental_solver", "LRB_rewarding", - # "maintain_watch_cache", # for DEBUG + # "maintain_watch_cache", # for DEBUG "reason_side_rewarding", "rephase", - "reward_annealing", # for big problems since 0.17(need to evalate with larger timeout) - "stochastic_local_search", # since 0.17 + "reward_annealing", + "stochastic_local_search", # "suppress_reason_chain", "trail_saving", "unsafe_access" ] -assign_rate = [] -best_phases_tracking = [] -bi_clause_completion = [] -boundary_check = [] -chrono_BT = [] -no_clause_elimination = [] -clause_rewarding = [] -clause_vivification = [] -debug_propagation = [] -dynamic_restart_threshold = [] -EMA_calibration = [] -EVSIDS = [] -incremental_solver = ["no_clause_elimination"] -just_used = [] -LRB_rewarding = [] -maintain_watch_cache = [] -no_IO = [] -reason_side_rewarding = [] -rephase = ["best_phases_tracking"] -reward_annealing = [] -stochastic_local_search = [] -support_user_assumption = [] -suppress_reason_chain = [] -trace_analysis = [] -trace_elimination = [] -trace_equivalency = [] -trail_saving = [] -unsafe_access = [] +assign_rate = [] # for debug and study +best_phases_tracking = [] # save the best-so-far assignment, used by 'rephase' +bi_clause_completion = [] # increase memory pressure +boundary_check = [] # for debug +chrono_BT = [] # NOT WORK +no_clause_elimination = [] # pre(in)-processor setting +clause_rewarding = [] # clauses have activities w/ decay rate +clause_vivification = [] # pre(in)-processor setting +debug_propagation = [] # for debug +dynamic_restart_threshold = [] # control restart spans like Glucose +EMA_calibration = [] # each exponential moving average has a calbration value +EVSIDS = [] # Eponential Variable State Independent Decaying Sum +incremental_solver = [ # for all solution SAT sover + "no_clause_elimination" + ] +just_used = [] # Var and clause have 'just_used' flags +LRB_rewarding = [] # Vearning Rate Based rewarding, a new var activity criteria +maintain_watch_cache = [] # for DEBUG +no_IO = [] # to embed Splr into non-std environments +reason_side_rewarding = [] # an idea used in Learning-rate based rewarding +rephase = [ # search around the best-so-far candidate repeatedly + "best_phases_tracking" + ] +reward_annealing = [] # use bigger and smaller decay rates cycliclly +stochastic_local_search = [ # since 0.17 + "reward_annealing" + ] +support_user_assumption = [] # NOT WORK (defined in Glucose) +suppress_reason_chain = [] # make direct links between a dicision var and its implications +trace_analysis = [] # for debug +trace_elimination = [] # for debug +trace_equivalency = [] # for debug +trail_saving = [] # reduce propagation cost by reusing propagation chain +unsafe_access = [] # access elements of vectors without boundary checking [profile.release] lto = "fat" From 528c5da82582068fcd6cddb5c8f0775e5f2dd632 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 16 Oct 2022 19:37:38 +0900 Subject: [PATCH 10/29] Cargo.toml: reorganize default features --- Cargo.toml | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index e97fce6d0..9667c6bf5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -17,22 +17,29 @@ bitflags = "^1.3" [features] default = [ - # "boundary_check", # for DEBUG - # "bi_clause_completion", - # "no_clause_elimination", - # "clause_rewarding", - "clause_vivification", - "dynamic_restart_threshold", + ### Essential # "incremental_solver", "LRB_rewarding", - # "maintain_watch_cache", # for DEBUG "reason_side_rewarding", + "unsafe_access", + "trail_saving", + + ### heuristics + # "bi_clause_completion", + # "clause_rewarding", + "dynamic_restart_threshold", "rephase", - "reward_annealing", + # "reward_annealing", "stochastic_local_search", # "suppress_reason_chain", - "trail_saving", - "unsafe_access" + + ### proceccor + # "no_clause_elimination", + "clause_vivification", + + ### for DEBUG + # "boundary_check", + # "maintain_watch_cache", ] assign_rate = [] # for debug and study best_phases_tracking = [] # save the best-so-far assignment, used by 'rephase' From e0d769d2b431ac7e03a6ffb75cff56da2655ccb4 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 16 Oct 2022 19:38:45 +0900 Subject: [PATCH 11/29] src/cdb/sls.rs: revised --- src/cdb/sls.rs | 45 +++++++++++++++++++++------------------------ 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs index 0bcc7e0d4..8b4337230 100644 --- a/src/cdb/sls.rs +++ b/src/cdb/sls.rs @@ -16,35 +16,33 @@ impl StochasticLocalSearchIF for ClauseDB { limit: usize, ) -> (usize, usize) { let mut returns = (0, 0); - let mut last_flip = 0; + let mut last_flip = self.num_clause; for step in 0..limit { let mut unsat_clauses = 0; let mut flip_target: HashMap = HashMap::new(); let mut target_clause: Option<&Clause> = None; - for c in self - .clause - .iter() - .skip(1) - .rev() - .filter(|c| /* !c.is(FlagClause::LEARNT) && */ !c.is_dead()) - { - let result = c.check_parity(assignment, &mut flip_target); - if let Some(c) = result { + for c in self.clause.iter().skip(1).filter(|c| !c.is_dead()) { + if c.is_falsified(assignment, &mut flip_target) { unsat_clauses += 1; if target_clause.is_none() || unsat_clauses == step { - target_clause = result; + target_clause = Some(c); for l in c.lits.iter() { flip_target.entry(l.vi()).or_insert(0); } } } } - if step == 1 { - returns = (unsat_clauses, unsat_clauses); + if step == 0 { + returns.0 = unsat_clauses; } returns.1 = unsat_clauses; + if unsat_clauses == 0 { + return returns; + } if let Some(c) = target_clause { - let factor = |vi| 3.2_f64.powf(-(*flip_target.get(vi).unwrap() as f64)); + let beta: f64 = 2.5 - 1.5 / (1.0 + unsat_clauses as f64).log(2.0); + // let beta: f64 = if unsat_clauses <= 3 { 1.0 } else { 3.0 }; + let factor = |vi| beta.powf(-(*flip_target.get(vi).unwrap() as f64)); let vars = c.lits.iter().map(|l| l.vi()).collect::>(); let index = (((step + last_flip) & 63) as f64 / 63.0) * vars.iter().map(factor).sum::(); @@ -52,12 +50,6 @@ impl StochasticLocalSearchIF for ClauseDB { for vi in vars.iter() { sum += factor(vi); if index <= sum { - // print!( - // "step {step}: flip {} of {}| {}", - // vi, - // c.lits.len(), - // assignment[vi] - // ); assignment.entry(*vi).and_modify(|e| *e = !*e); last_flip = *vi; break; @@ -72,17 +64,20 @@ impl StochasticLocalSearchIF for ClauseDB { } impl Clause { - fn check_parity( + fn is_falsified( &self, assignment: &HashMap, flip_target: &mut HashMap, - ) -> Option<&Self> { + ) -> bool { let mut num_sat = 0; let mut sat_vi = 0; for l in self.iter() { let vi = l.vi(); match assignment.get(&vi) { Some(b) if *b == l.as_bool() => { + if num_sat == 1 { + return false; + } num_sat += 1; sat_vi = vi; } @@ -90,9 +85,11 @@ impl Clause { _ => (), } } - if num_sat == 1 { + if num_sat == 0 { + true + } else { *flip_target.entry(sat_vi).or_insert(0) += 1; + false } - (0 == num_sat).then_some(self) } } From e375e2ee72d9aa74409d2d33c6779562a6518dbf Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sun, 16 Oct 2022 19:41:03 +0900 Subject: [PATCH 12/29] (search) reset StageManager whenever a new assertion is found --- src/assign/select.rs | 39 ++++++++++++++++++-------- src/solver/search.rs | 66 +++++++++++++++++++++++++------------------- src/solver/stage.rs | 5 ++++ src/state.rs | 13 +++------ 4 files changed, 73 insertions(+), 50 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index 0b400b5cd..43a24e263 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -1,7 +1,9 @@ /// Decision var selection #[cfg(feature = "rephase")] -use {super::property, std::collections::HashMap}; +use super::property; +#[cfg(feature = "stochastic_local_search")] +use std::collections::HashMap; use { super::{AssignStack, VarHeapIF}, @@ -26,12 +28,15 @@ macro_rules! var_assign { /// API for var selection, depending on an internal heap. pub trait VarSelectIF { - #[cfg(feature = "rephase")] + #[cfg(feature = "stochastic_local_search")] /// return best phases fn best_phases_ref(&mut self) -> HashMap; + #[cfg(feature = "stochastic_local_search")] + /// force an assignment obtained by SLS + fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize; #[cfg(feature = "rephase")] /// select rephasing target - fn select_rephasing_target(&mut self, assignment: Option>); + fn select_rephasing_target(&mut self); #[cfg(feature = "rephase")] /// check the consistency fn check_consistency_of_best_phases(&mut self); @@ -44,7 +49,7 @@ pub trait VarSelectIF { } impl VarSelectIF for AssignStack { - #[cfg(feature = "rephase")] + #[cfg(feature = "stochastic_local_search")] fn best_phases_ref(&mut self) -> HashMap { self.var .iter() @@ -64,17 +69,27 @@ impl VarSelectIF for AssignStack { }) .collect::>() } - #[cfg(feature = "rephase")] - fn select_rephasing_target(&mut self, assignment: Option>) { - if let Some(assignment) = assignment { - for (vi, b) in assignment.iter() { - let v = &mut self.var[*vi]; + #[cfg(feature = "stochastic_local_search")] + fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize { + let mut num_fliped = 0; + for (vi, b) in assignment.iter() { + let v = &mut self.var[*vi]; + if v.is(FlagVar::PHASE) != *b { v.set(FlagVar::PHASE, *b); - self.best_phases.insert(*vi, (*b, AssignReason::None)); + // v.reward *= self.activity_decay; + // v.reward += self.activity_anti_decay; + // self.update_heap(*vi); + } + if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { + num_fliped += 1; + // self.best_phases.insert(*vi, (*b, AssignReason::None)); } - self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars; - return; } + // self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars; + num_fliped + } + #[cfg(feature = "rephase")] + fn select_rephasing_target(&mut self) { if self.best_phases.is_empty() { return; } diff --git a/src/solver/search.rs b/src/solver/search.rs index ef009fe53..30da6204e 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,7 +239,6 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; - let mut best_phase_updated = false; state.stm.initialize( (asg.derefer(assign::property::Tusize::NumUnassertedVar) as f64).sqrt() as usize, @@ -256,8 +255,13 @@ fn search( asg.update_activity_tick(); #[cfg(feature = "clause_rewarding")] cdb.update_activity_tick(); - if 1 < handle_conflict(asg, cdb, state, &cc)? { - num_learnt += 1; + // if 1 < handle_conflict(asg, cdb, state, &cc)? { + // num_learnt += 1; + // } + match handle_conflict(asg, cdb, state, &cc)? { + 0 => state.stm.reset(), + 1 => (), + _ => num_learnt += 1, } if state.stm.stage_ended(num_learnt) { if let Some(p) = state.elapsed() { @@ -292,32 +296,9 @@ fn search( if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; } - #[cfg(feature = "rephase")] - { - #[cfg(feature = "stochastic_local_search")] - if best_phase_updated { - best_phase_updated = false; - use cdb::StochasticLocalSearchIF; - let mut assignment = asg.best_phases_ref(); - let stats = cdb.stochastic_local_search(&mut assignment, 100); - if stats.1 < stats.0 { - state.stats[Stat::UnsatsBySLS] = stats.1; - state.flush(format!("SLS: {} -> {}", stats.0, stats.1)); - // We need to restart in order to try the whole assignment by SLS - RESTART!(asg, cdb, state); - asg.select_rephasing_target(Some(assignment)); - } - } else { - asg.select_rephasing_target(None); - } - #[cfg(not(feature = "stochastic_local_search"))] - { - asg.select_rephasing_target(None); - } - } if new_segment { - #[cfg(not(feature = "reward_annealing"))] - asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); + // #[cfg(not(feature = "reward_annealing"))] + // asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); if !cfg!(feature = "no_clause_elimination") { let mut elim = Eliminator::instantiate(&state.config, &state.cnf); elim.simplify(asg, cdb, state, false)?; @@ -329,6 +310,34 @@ fn search( state.restart.set_segment_parameters(max_scale); } } + #[cfg(feature = "rephase")] + { + #[cfg(feature = "stochastic_local_search")] + if new_segment { + use cdb::StochasticLocalSearchIF; + state.flush("SLS"); + let mut assignment = asg.best_phases_ref(); + let limit = 10 * state.stm.current_segment(); + let stats = cdb.stochastic_local_search(&mut assignment, limit); + // Note: `stats.1 == 1` is a local minimum and it's NOT a solution. + // But if the problem is UNSAT, it might be a good point close + // to a root-level conflict. + // Note: to force the new assignemnt effectivety, it maybe be a good idea + // to relax var decay rate (temporally). So do 'reward_annealing.' + /* || stats.1 == 1 */ + if stats.1 < stats.0 && 1 < stats.1 { + state.flush(format!(": {} -> {}, ", stats.0, stats.1)); + state.stats[Stat::SLS] = asg.override_rephasing_target(&assignment); + // } else { + // asg.select_rephasing_target(); + } + // } else { + // asg.select_rephasing_target(); + } + asg.select_rephasing_target(); + #[cfg(not(feature = "stochastic_local_search"))] + asg.select_rephasing_target(); + } } state.progress(asg, cdb); asg.handle(SolverEvent::Stage(scale)); @@ -341,7 +350,6 @@ fn search( RESTART!(asg, cdb, state); } if let Some(na) = asg.best_assigned() { - best_phase_updated = true; state.flush(""); state.flush(format!("unreachable core: {}", na)); } diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 6e2836dec..c5a685f8d 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -49,6 +49,11 @@ impl StageManager { self.scale = 1; self.end_of_stage = unit_size; } + pub fn reset(&mut self) { + self.cycle = 0; + self.scale = 1; + self.end_of_stage = self.unit_size; + } /// returns: /// - Some(true): it's a beginning of a new cycle and a new segment, a 2nd-level group. /// - Some(false): a beginning of a new cycle. diff --git a/src/state.rs b/src/state.rs index 899a0e353..4948b2615 100644 --- a/src/state.rs +++ b/src/state.rs @@ -52,7 +52,7 @@ pub enum Stat { /// the number of subsumed clause by processor SubsumedClause, /// SLS core - UnsatsBySLS, + SLS, /// don't use this dummy (sentinel at the tail). EndOfStatIndex, } @@ -514,19 +514,14 @@ impl StateIF for State { ), ); println!( - "\x1B[2K misc|vivC:{}, -SLS:{}, core:{}, /ppc:{}", + "\x1B[2K misc|vivC:{}, !SLS:{}, core:{}, /ppc:{}", im!( "{:>9}", self, LogUsizeId::VivifiedClause, self[Stat::VivifiedClause] ), - im!( - "{:>9}", - self, - LogUsizeId::UnsatsBySLS, - self[Stat::UnsatsBySLS] - ), + im!("{:>9}", self, LogUsizeId::SLS, self[Stat::SLS]), im!( "{:>9}", self, @@ -840,7 +835,7 @@ pub enum LogUsizeId { // //## Stochastic Local Search // - UnsatsBySLS, + SLS, // the sentinel End, From f878f3f03fe35b4ad45ecf73ba8593c0fcad6959 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 17 Oct 2022 19:49:40 +0900 Subject: [PATCH 13/29] fix typos --- src/assign/select.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index 43a24e263..55eba9cf5 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -71,7 +71,7 @@ impl VarSelectIF for AssignStack { } #[cfg(feature = "stochastic_local_search")] fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize { - let mut num_fliped = 0; + let mut num_flipped = 0; for (vi, b) in assignment.iter() { let v = &mut self.var[*vi]; if v.is(FlagVar::PHASE) != *b { @@ -81,12 +81,12 @@ impl VarSelectIF for AssignStack { // self.update_heap(*vi); } if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { - num_fliped += 1; - // self.best_phases.insert(*vi, (*b, AssignReason::None)); + num_flipped += 1; + self.best_phases.insert(*vi, (*b, AssignReason::None)); } } // self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars; - num_fliped + num_flipped } #[cfg(feature = "rephase")] fn select_rephasing_target(&mut self) { From 2bc49bd09baa6dd954d4e836d3de4c5c11cc048b Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 17 Oct 2022 19:51:39 +0900 Subject: [PATCH 14/29] revise progress report --- src/cdb/vivify.rs | 2 +- src/solver/search.rs | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index 548118113..8554a64e8 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -163,7 +163,7 @@ impl VivifyIF for ClauseDB { debug_assert!(asg.stack_is_empty() || !asg.remains()); state.flush(""); state.flush(format!( - "vivified(assert:{} shorten:{}), ", + "vivification(assert:{} shorten:{}), ", num_assert, num_shrink )); // state.log( diff --git a/src/solver/search.rs b/src/solver/search.rs index 30da6204e..1fbeb7d84 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -301,6 +301,7 @@ fn search( // asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); if !cfg!(feature = "no_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()); state[Stat::Simplify] += 1; From 6021477d217ae5888c941a4585e94c3ebaea0e2f Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 17 Oct 2022 19:53:05 +0900 Subject: [PATCH 15/29] modified: src/cdb/sls.rs --- src/cdb/sls.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs index 8b4337230..0caf79f1e 100644 --- a/src/cdb/sls.rs +++ b/src/cdb/sls.rs @@ -17,8 +17,10 @@ impl StochasticLocalSearchIF for ClauseDB { ) -> (usize, usize) { let mut returns = (0, 0); let mut last_flip = self.num_clause; - for step in 0..limit { + let mut seed = 38_721_103; + for step in 1..=limit { let mut unsat_clauses = 0; + // CONSIDER: counting only given (permanent) clauses. let mut flip_target: HashMap = HashMap::new(); let mut target_clause: Option<&Clause> = None; for c in self.clause.iter().skip(1).filter(|c| !c.is_dead()) { @@ -32,20 +34,20 @@ impl StochasticLocalSearchIF for ClauseDB { } } } - if step == 0 { + if step == 1 { returns.0 = unsat_clauses; } returns.1 = unsat_clauses; if unsat_clauses == 0 { return returns; } + seed = ((((!seed * 11_304_001) % 22_003_811) ^ (!last_flip * seed)) % 31_754_873) >> 4; if let Some(c) = target_clause { - let beta: f64 = 2.5 - 1.5 / (1.0 + unsat_clauses as f64).log(2.0); + let beta: f64 = 3.2 - 2.1 / (1.0 + unsat_clauses as f64).log(2.0); // let beta: f64 = if unsat_clauses <= 3 { 1.0 } else { 3.0 }; let factor = |vi| beta.powf(-(*flip_target.get(vi).unwrap() as f64)); let vars = c.lits.iter().map(|l| l.vi()).collect::>(); - let index = (((step + last_flip) & 63) as f64 / 63.0) - * vars.iter().map(factor).sum::(); + let index = ((seed % 100) as f64 / 100.0) * vars.iter().map(factor).sum::(); let mut sum: f64 = 0.0; for vi in vars.iter() { sum += factor(vi); From 0469c7278a887d054a1baa55eca6712345cdde5b Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Mon, 17 Oct 2022 19:53:28 +0900 Subject: [PATCH 16/29] (search) revise the stocastic_local_search invocation condition --- src/solver/search.rs | 81 +++++++++++++++++++++++++++++--------------- 1 file changed, 54 insertions(+), 27 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index 1fbeb7d84..77ded40e7 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,6 +239,12 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; + #[cfg(feature = "stochastic_local_search")] + let mut best_core = asg.num_vars; + #[cfg(feature = "stochastic_local_search")] + let mut best_core_updated = None; + #[cfg(feature = "stochastic_local_search")] + let mut best_sls = cdb.derefer(cdb::property::Tusize::NumClause); state.stm.initialize( (asg.derefer(assign::property::Tusize::NumUnassertedVar) as f64).sqrt() as usize, @@ -255,14 +261,14 @@ fn search( asg.update_activity_tick(); #[cfg(feature = "clause_rewarding")] cdb.update_activity_tick(); - // if 1 < handle_conflict(asg, cdb, state, &cc)? { - // num_learnt += 1; - // } - match handle_conflict(asg, cdb, state, &cc)? { - 0 => state.stm.reset(), - 1 => (), - _ => num_learnt += 1, + if 1 < handle_conflict(asg, cdb, state, &cc)? { + num_learnt += 1; } + // match handle_conflict(asg, cdb, state, &cc)? { + // 0 => state.stm.reset(), + // 1 => (), + // _ => num_learnt += 1, + // } if state.stm.stage_ended(num_learnt) { if let Some(p) = state.elapsed() { if 1.0 <= p { @@ -314,30 +320,45 @@ fn search( #[cfg(feature = "rephase")] { #[cfg(feature = "stochastic_local_search")] - if new_segment { + { use cdb::StochasticLocalSearchIF; - state.flush("SLS"); - let mut assignment = asg.best_phases_ref(); - let limit = 10 * state.stm.current_segment(); - let stats = cdb.stochastic_local_search(&mut assignment, limit); - // Note: `stats.1 == 1` is a local minimum and it's NOT a solution. - // But if the problem is UNSAT, it might be a good point close - // to a root-level conflict. - // Note: to force the new assignemnt effectivety, it maybe be a good idea - // to relax var decay rate (temporally). So do 'reward_annealing.' - /* || stats.1 == 1 */ - if stats.1 < stats.0 && 1 < stats.1 { - state.flush(format!(": {} -> {}, ", stats.0, stats.1)); - state.stats[Stat::SLS] = asg.override_rephasing_target(&assignment); - // } else { - // asg.select_rephasing_target(); + macro_rules! sls { + ($assign: expr, $improved: expr, $limit: expr) => { + state.flush("SLS"); + let stats = cdb.stochastic_local_search(&mut $assign, $limit); + if $improved(stats) { + best_sls = stats.1; + state.stats[Stat::SLS] = stats.1; + let num_flipped = asg.override_rephasing_target(&$assign); + state.flush(format!( + "({} clauses, {} flips), ", + stats.1, num_flipped + )); + } else { + state.flush(", "); + } + }; + } + match (state.stm.current_cycle() % 4, best_core_updated) { + (_, Some(mut assignment)) => { + let limit = 100 * state.stm.current_segment(); + sls!(assignment, |c: (usize, usize)| c.1 <= c.0, limit); + } + (0, _) => { + let mut assignment = asg.best_phases_ref(); + sls!(assignment, |c: (usize, usize)| c.1 <= best_sls, 100); + } + (1, _) => { + asg.select_rephasing_target(); + } + _ => (), } - // } else { - // asg.select_rephasing_target(); + best_core_updated = None; } - asg.select_rephasing_target(); #[cfg(not(feature = "stochastic_local_search"))] - asg.select_rephasing_target(); + { + asg.select_rephasing_target(); + } } } state.progress(asg, cdb); @@ -353,6 +374,12 @@ fn search( if let Some(na) = asg.best_assigned() { state.flush(""); state.flush(format!("unreachable core: {}", na)); + #[cfg(feature = "stochastic_local_search")] + if na < best_core { + best_core = na; + best_core_updated = Some(asg.best_phases_ref()); + best_sls = cdb.derefer(cdb::property::Tusize::NumClause); + } } } } From c81c11db5d4c8878021a8ea2e0f711d207475a1c Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 18 Oct 2022 19:52:27 +0900 Subject: [PATCH 17/29] Add AssignIF::best_phases_invalid --- src/assign/mod.rs | 2 ++ src/assign/stack.rs | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/assign/mod.rs b/src/assign/mod.rs index dc2c8d3b0..97a8a861c 100644 --- a/src/assign/mod.rs +++ b/src/assign/mod.rs @@ -76,6 +76,8 @@ pub trait AssignIF: /// return a reference to `level`. fn level_ref(&self) -> &[DecisionLevel]; fn best_assigned(&mut self) -> Option; + /// return true if no best_phases + fn best_phases_invalid(&self) -> bool; /// inject assignments for eliminated vars. fn extend_model(&mut self, c: &mut impl ClauseDBIF) -> Vec>; /// return `true` if the set of literals is satisfiable under the current assignment. diff --git a/src/assign/stack.rs b/src/assign/stack.rs index 6a873e8f0..cef66807e 100644 --- a/src/assign/stack.rs +++ b/src/assign/stack.rs @@ -196,6 +196,9 @@ impl AssignIF for AssignStack { fn best_assigned(&mut self) -> Option { (self.build_best_at == self.num_propagation).then_some(self.num_vars - self.num_best_assign) } + fn best_phases_invalid(&self) -> bool { + self.best_phases.is_empty() + } #[allow(unused_variables)] fn extend_model(&mut self, cdb: &mut impl ClauseDBIF) -> Vec> { let lits = &self.eliminated; From 8e78975e8768da7fd77ab62e02d220f8c2523aaa Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 18 Oct 2022 19:53:23 +0900 Subject: [PATCH 18/29] a snapshot --- src/assign/select.rs | 15 +++---- src/cdb/sls.rs | 31 ++++++++++++--- src/solver/search.rs | 95 ++++++++++++++++++++------------------------ src/state.rs | 15 ++++++- 4 files changed, 89 insertions(+), 67 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index 55eba9cf5..d6d1ba0cd 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -30,7 +30,7 @@ macro_rules! var_assign { pub trait VarSelectIF { #[cfg(feature = "stochastic_local_search")] /// return best phases - fn best_phases_ref(&mut self) -> HashMap; + fn best_phases_ref(&mut self, default_value: Option) -> HashMap; #[cfg(feature = "stochastic_local_search")] /// force an assignment obtained by SLS fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize; @@ -50,13 +50,13 @@ pub trait VarSelectIF { impl VarSelectIF for AssignStack { #[cfg(feature = "stochastic_local_search")] - fn best_phases_ref(&mut self) -> HashMap { + fn best_phases_ref(&mut self, default_value: Option) -> HashMap { self.var .iter() .enumerate() .filter_map(|(vi, v)| { if self.level[vi] == self.root_level || self.var[vi].is(FlagVar::ELIMINATED) { - None + default_value.map(|b| (vi, b)) } else { Some(( vi, @@ -75,15 +75,16 @@ impl VarSelectIF for AssignStack { for (vi, b) in assignment.iter() { let v = &mut self.var[*vi]; if v.is(FlagVar::PHASE) != *b { + num_flipped += 1; v.set(FlagVar::PHASE, *b); // v.reward *= self.activity_decay; // v.reward += self.activity_anti_decay; // self.update_heap(*vi); } - if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { - num_flipped += 1; - self.best_phases.insert(*vi, (*b, AssignReason::None)); - } + // if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { + // num_flipped += 1; + // self.best_phases.insert(*vi, (*b, AssignReason::None)); + // } } // self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars; num_flipped diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs index 0caf79f1e..71c25fddd 100644 --- a/src/cdb/sls.rs +++ b/src/cdb/sls.rs @@ -1,9 +1,17 @@ /// Implementation of Stochastic Local Search -use {crate::types::*, std::collections::HashMap}; +use { + crate::{assign::AssignIF, types::*}, + std::collections::HashMap, +}; pub trait StochasticLocalSearchIF { + /// returns the decision level of the given assignment and the one of the final assignment. + /// Note: the lower level a set of clauses make a conflict at, + /// the higher learning rate a solver can keep and the better learnt clauses we will have. + /// This would be a better criteria that can be used in CDCL solvers. fn stochastic_local_search( &mut self, + asg: &impl AssignIF, start: &mut HashMap, limit: usize, ) -> (usize, usize); @@ -12,20 +20,27 @@ pub trait StochasticLocalSearchIF { impl StochasticLocalSearchIF for ClauseDB { fn stochastic_local_search( &mut self, + _asg: &impl AssignIF, assignment: &mut HashMap, limit: usize, ) -> (usize, usize) { - let mut returns = (0, 0); + let mut returns: (usize, usize) = (0, 0); let mut last_flip = self.num_clause; let mut seed = 38_721_103; for step in 1..=limit { let mut unsat_clauses = 0; + // let mut level: DecisionLevel = 0; // CONSIDER: counting only given (permanent) clauses. let mut flip_target: HashMap = HashMap::new(); let mut target_clause: Option<&Clause> = None; for c in self.clause.iter().skip(1).filter(|c| !c.is_dead()) { + // let mut cls_lvl: DecisionLevel = 0; if c.is_falsified(assignment, &mut flip_target) { unsat_clauses += 1; + // for l in c.lits.iter() { + // cls_lvl = cls_lvl.max(asg.level(l.vi())); + // } + // level = level.max(cls_lvl); if target_clause.is_none() || unsat_clauses == step { target_clause = Some(c); for l in c.lits.iter() { @@ -36,12 +51,16 @@ impl StochasticLocalSearchIF for ClauseDB { } if step == 1 { returns.0 = unsat_clauses; + // returns.0 = level as usize; } returns.1 = unsat_clauses; - if unsat_clauses == 0 { - return returns; + // returns.1 = level as usize; + if unsat_clauses == 0 || step == limit { + break; } - seed = ((((!seed * 11_304_001) % 22_003_811) ^ (!last_flip * seed)) % 31_754_873) >> 4; + seed = (((((!seed % 10_000_000) * 11_304_001) % 22_003_811) ^ (!last_flip * seed)) + % 31_754_873) + >> 4; if let Some(c) = target_clause { let beta: f64 = 3.2 - 2.1 / (1.0 + unsat_clauses as f64).log(2.0); // let beta: f64 = if unsat_clauses <= 3 { 1.0 } else { 3.0 }; @@ -58,7 +77,7 @@ impl StochasticLocalSearchIF for ClauseDB { } } } else { - return returns; + break; } } returns diff --git a/src/solver/search.rs b/src/solver/search.rs index 77ded40e7..9358c1ac2 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,12 +239,12 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; + // #[cfg(feature = "stochastic_local_search")] + // let mut best_core = asg.num_vars; + // #[cfg(feature = "stochastic_local_search")] + // let mut best_core_updated = None; #[cfg(feature = "stochastic_local_search")] - let mut best_core = asg.num_vars; - #[cfg(feature = "stochastic_local_search")] - let mut best_core_updated = None; - #[cfg(feature = "stochastic_local_search")] - let mut best_sls = cdb.derefer(cdb::property::Tusize::NumClause); + let mut best_phases_invalid = true; state.stm.initialize( (asg.derefer(assign::property::Tusize::NumUnassertedVar) as f64).sqrt() as usize, @@ -261,14 +261,17 @@ fn search( asg.update_activity_tick(); #[cfg(feature = "clause_rewarding")] cdb.update_activity_tick(); - if 1 < handle_conflict(asg, cdb, state, &cc)? { - num_learnt += 1; - } - // match handle_conflict(asg, cdb, state, &cc)? { - // 0 => state.stm.reset(), - // 1 => (), - // _ => num_learnt += 1, + // if 1 < handle_conflict(asg, cdb, state, &cc)? { + // num_learnt += 1; // } + match handle_conflict(asg, cdb, state, &cc)? { + 0 => { + best_phases_invalid = true; + state.stm.reset(); + } + 1 => (), + _ => num_learnt += 1, + } if state.stm.stage_ended(num_learnt) { if let Some(p) = state.elapsed() { if 1.0 <= p { @@ -299,24 +302,6 @@ fn search( } if let Some(new_segment) = next_stage { // a beginning of a new cycle - if cfg!(feature = "clause_vivification") { - cdb.vivify(asg, state)?; - } - if new_segment { - // #[cfg(not(feature = "reward_annealing"))] - // asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); - if !cfg!(feature = "no_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()); - state[Stat::Simplify] += 1; - state[Stat::SubsumedClause] = elim.num_subsumed; - } - if cfg!(feature = "dynamic_restart_threshold") { - state.restart.set_segment_parameters(max_scale); - } - } #[cfg(feature = "rephase")] { #[cfg(feature = "stochastic_local_search")] @@ -325,10 +310,10 @@ fn search( macro_rules! sls { ($assign: expr, $improved: expr, $limit: expr) => { state.flush("SLS"); - let stats = cdb.stochastic_local_search(&mut $assign, $limit); + let stats = + cdb.stochastic_local_search(asg, &mut $assign, $limit); if $improved(stats) { - best_sls = stats.1; - state.stats[Stat::SLS] = stats.1; + state.sls_index = stats.1; let num_flipped = asg.override_rephasing_target(&$assign); state.flush(format!( "({} clauses, {} flips), ", @@ -339,27 +324,37 @@ fn search( } }; } - match (state.stm.current_cycle() % 4, best_core_updated) { - (_, Some(mut assignment)) => { - let limit = 100 * state.stm.current_segment(); - sls!(assignment, |c: (usize, usize)| c.1 <= c.0, limit); - } - (0, _) => { - let mut assignment = asg.best_phases_ref(); - sls!(assignment, |c: (usize, usize)| c.1 <= best_sls, 100); - } - (1, _) => { - asg.select_rephasing_target(); - } - _ => (), + if best_phases_invalid { + best_phases_invalid = false; + let mut assignment = asg.best_phases_ref(Some(false)); + sls!(assignment, |_: (usize, usize)| true, 200); + } else { + asg.select_rephasing_target(); } - best_core_updated = None; } #[cfg(not(feature = "stochastic_local_search"))] { asg.select_rephasing_target(); } } + if cfg!(feature = "clause_vivification") { + cdb.vivify(asg, state)?; + } + if new_segment { + #[cfg(not(feature = "reward_annealing"))] + asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); + if !cfg!(feature = "no_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()); + state[Stat::Simplify] += 1; + state[Stat::SubsumedClause] = elim.num_subsumed; + } + if cfg!(feature = "dynamic_restart_threshold") { + state.restart.set_segment_parameters(max_scale); + } + } } state.progress(asg, cdb); asg.handle(SolverEvent::Stage(scale)); @@ -374,12 +369,6 @@ fn search( if let Some(na) = asg.best_assigned() { state.flush(""); state.flush(format!("unreachable core: {}", na)); - #[cfg(feature = "stochastic_local_search")] - if na < best_core { - best_core = na; - best_core_updated = Some(asg.best_phases_ref()); - best_sls = cdb.derefer(cdb::property::Tusize::NumClause); - } } } } diff --git a/src/state.rs b/src/state.rs index 4948b2615..bf3553511 100644 --- a/src/state.rs +++ b/src/state.rs @@ -112,8 +112,14 @@ pub struct State { /// hold conflicting user-defined *assumed* literals for UNSAT problems pub conflicts: Vec, + #[cfg(feature = "chronoBT")] /// chronoBT threshold pub chrono_bt_threshold: DecisionLevel, + + #[cfg(feature = "stochastic_local_search")] + /// criteria for SLS + pub sls_index: usize, + /// hold the previous number of non-conflicting assignment pub last_asg: usize, /// working place to build learnt clauses @@ -148,7 +154,13 @@ impl Default for State { #[cfg(feature = "support_user_assumption")] conflicts: Vec::new(), + + #[cfg(feature = "chronoBT")] chrono_bt_threshold: 100, + + #[cfg(feature = "stochastic_local_search")] + sls_index: 9_999_999, + last_asg: 0, new_learnt: Vec::new(), derive20: Vec::new(), @@ -521,7 +533,7 @@ impl StateIF for State { LogUsizeId::VivifiedClause, self[Stat::VivifiedClause] ), - im!("{:>9}", self, LogUsizeId::SLS, self[Stat::SLS]), + im!("{:>9}", self, LogUsizeId::SLS, self.sls_index), im!( "{:>9}", self, @@ -858,6 +870,7 @@ pub enum LogF64Id { PropagationPerConflict, LiteralBlockEntanglement, RestartEnergy, + End, } From 3a5e0d913697de1bb854cc392d15c6d178c76f1a Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 18 Oct 2022 20:34:28 +0900 Subject: [PATCH 19/29] (stochastic_local_search) shrink a pseudo random number range --- src/cdb/sls.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs index 71c25fddd..d47b7de19 100644 --- a/src/cdb/sls.rs +++ b/src/cdb/sls.rs @@ -26,7 +26,7 @@ impl StochasticLocalSearchIF for ClauseDB { ) -> (usize, usize) { let mut returns: (usize, usize) = (0, 0); let mut last_flip = self.num_clause; - let mut seed = 38_721_103; + let mut seed = 721_109; for step in 1..=limit { let mut unsat_clauses = 0; // let mut level: DecisionLevel = 0; @@ -58,9 +58,9 @@ impl StochasticLocalSearchIF for ClauseDB { if unsat_clauses == 0 || step == limit { break; } - seed = (((((!seed % 10_000_000) * 11_304_001) % 22_003_811) ^ (!last_flip * seed)) - % 31_754_873) - >> 4; + seed = ((((!seed & 0x0000_0000_ffff_ffff) * 1_304_003) % 2_003_819) + ^ ((!last_flip & 0x0000_0000_ffff_ffff) * seed)) + % 3_754_873; if let Some(c) = target_clause { let beta: f64 = 3.2 - 2.1 / (1.0 + unsat_clauses as f64).log(2.0); // let beta: f64 = if unsat_clauses <= 3 { 1.0 } else { 3.0 }; From 7e3ebf68b985dec15788d1e3c5a66fdfc7264cf4 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Tue, 18 Oct 2022 22:31:17 +0900 Subject: [PATCH 20/29] A snapshot --- src/assign/select.rs | 20 ++++++++++---------- src/solver/search.rs | 16 ++++++---------- src/state.rs | 2 +- 3 files changed, 17 insertions(+), 21 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index d6d1ba0cd..114aee117 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -73,18 +73,18 @@ impl VarSelectIF for AssignStack { fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize { let mut num_flipped = 0; for (vi, b) in assignment.iter() { - let v = &mut self.var[*vi]; - if v.is(FlagVar::PHASE) != *b { - num_flipped += 1; - v.set(FlagVar::PHASE, *b); - // v.reward *= self.activity_decay; - // v.reward += self.activity_anti_decay; - // self.update_heap(*vi); - } - // if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { + // let v = &mut self.var[*vi]; + // if v.is(FlagVar::PHASE) != *b { // num_flipped += 1; - // self.best_phases.insert(*vi, (*b, AssignReason::None)); + // v.set(FlagVar::PHASE, *b); + // // v.reward *= self.activity_decay; + // // v.reward += self.activity_anti_decay; + // // self.update_heap(*vi); // } + if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { + num_flipped += 1; + self.best_phases.insert(*vi, (*b, AssignReason::None)); + } } // self.num_best_assign = self.num_asserted_vars + self.num_eliminated_vars; num_flipped diff --git a/src/solver/search.rs b/src/solver/search.rs index 9358c1ac2..139c0bd9b 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -266,8 +266,8 @@ fn search( // } match handle_conflict(asg, cdb, state, &cc)? { 0 => { - best_phases_invalid = true; - state.stm.reset(); + best_phases_invalid = asg.best_phases_invalid(); + // state.stm.reset(); } 1 => (), _ => num_learnt += 1, @@ -313,7 +313,8 @@ fn search( let stats = cdb.stochastic_local_search(asg, &mut $assign, $limit); if $improved(stats) { - state.sls_index = stats.1; + state.sls_index += 1; + // state.sls_index = stats.1; let num_flipped = asg.override_rephasing_target(&$assign); state.flush(format!( "({} clauses, {} flips), ", @@ -324,18 +325,13 @@ fn search( } }; } - if best_phases_invalid { + if best_phases_invalid || new_segment { best_phases_invalid = false; let mut assignment = asg.best_phases_ref(Some(false)); sls!(assignment, |_: (usize, usize)| true, 200); - } else { - asg.select_rephasing_target(); } } - #[cfg(not(feature = "stochastic_local_search"))] - { - asg.select_rephasing_target(); - } + asg.select_rephasing_target(); } if cfg!(feature = "clause_vivification") { cdb.vivify(asg, state)?; diff --git a/src/state.rs b/src/state.rs index bf3553511..0112b57ab 100644 --- a/src/state.rs +++ b/src/state.rs @@ -159,7 +159,7 @@ impl Default for State { chrono_bt_threshold: 100, #[cfg(feature = "stochastic_local_search")] - sls_index: 9_999_999, + sls_index: 0, last_asg: 0, new_learnt: Vec::new(), From 09a1739fe44d3f06ab7b3d3e26b4b0b3d279eb31 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Wed, 19 Oct 2022 09:31:16 +0900 Subject: [PATCH 21/29] make stochastic_local_search essential --- src/assign/select.rs | 7 +------ src/cdb/mod.rs | 4 +--- src/solver/search.rs | 28 +++++++++++++++------------- 3 files changed, 17 insertions(+), 22 deletions(-) diff --git a/src/assign/select.rs b/src/assign/select.rs index 114aee117..8e439c4fe 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -2,12 +2,11 @@ #[cfg(feature = "rephase")] use super::property; -#[cfg(feature = "stochastic_local_search")] -use std::collections::HashMap; use { super::{AssignStack, VarHeapIF}, crate::types::*, + std::collections::HashMap, }; /// ```ignore @@ -28,10 +27,8 @@ macro_rules! var_assign { /// API for var selection, depending on an internal heap. pub trait VarSelectIF { - #[cfg(feature = "stochastic_local_search")] /// return best phases fn best_phases_ref(&mut self, default_value: Option) -> HashMap; - #[cfg(feature = "stochastic_local_search")] /// force an assignment obtained by SLS fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize; #[cfg(feature = "rephase")] @@ -49,7 +46,6 @@ pub trait VarSelectIF { } impl VarSelectIF for AssignStack { - #[cfg(feature = "stochastic_local_search")] fn best_phases_ref(&mut self, default_value: Option) -> HashMap { self.var .iter() @@ -69,7 +65,6 @@ impl VarSelectIF for AssignStack { }) .collect::>() } - #[cfg(feature = "stochastic_local_search")] fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize { let mut num_flipped = 0; for (vi, b) in assignment.iter() { diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index cd53af263..d2576eb05 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -10,7 +10,6 @@ mod clause; mod db; /// EMA mod ema; -#[cfg(feature = "stochastic_local_search")] /// methods for Stochastic Local Search mod sls; /// methods for UNSAT certification @@ -24,11 +23,10 @@ pub use self::{ binary::{BinaryLinkDB, BinaryLinkList}, cid::ClauseIdIF, property::*, + sls::StochasticLocalSearchIF, unsat_certificate::CertificationStore, vivify::VivifyIF, }; -#[cfg(feature = "stochastic_local_search")] -pub use sls::StochasticLocalSearchIF; use { self::ema::ProgressLBD, diff --git a/src/solver/search.rs b/src/solver/search.rs index 139c0bd9b..592db5127 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,11 +239,6 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; - // #[cfg(feature = "stochastic_local_search")] - // let mut best_core = asg.num_vars; - // #[cfg(feature = "stochastic_local_search")] - // let mut best_core_updated = None; - #[cfg(feature = "stochastic_local_search")] let mut best_phases_invalid = true; state.stm.initialize( @@ -293,8 +288,7 @@ fn search( ); let scale = state.stm.current_scale(); let max_scale = state.stm.max_scale(); - #[cfg(feature = "reward_annealing")] - { + if cfg!(feature = "reward_annealing") { let base = (1 << (state.stm.current_segment() - 1)) - 1; let decay_index = state.stm.current_cycle() - base; let decay = (decay_index as f64 - 1.0) / decay_index as f64; @@ -304,10 +298,17 @@ fn search( // a beginning of a new cycle #[cfg(feature = "rephase")] { - #[cfg(feature = "stochastic_local_search")] - { + if cfg!(feature = "stochastic_local_search") { use cdb::StochasticLocalSearchIF; macro_rules! sls { + ($assign: expr, $limit: expr) => { + state.flush("SLS "); + let cls = + cdb.stochastic_local_search(asg, &mut $assign, $limit); + state.sls_index += 1; + let flips = asg.override_rephasing_target(&$assign); + state.flush(format!("({} clauses, {} flips), ", cls.1, flips)); + }; ($assign: expr, $improved: expr, $limit: expr) => { state.flush("SLS"); let stats = @@ -328,7 +329,7 @@ fn search( if best_phases_invalid || new_segment { best_phases_invalid = false; let mut assignment = asg.best_phases_ref(Some(false)); - sls!(assignment, |_: (usize, usize)| true, 200); + sls!(assignment, 100); } } asg.select_rephasing_target(); @@ -337,8 +338,9 @@ fn search( cdb.vivify(asg, state)?; } if new_segment { - #[cfg(not(feature = "reward_annealing"))] - asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); + if !cfg!(feature = "reward_annealing") { + asg.rescale_activity((max_scale - scale) as f64 / max_scale as f64); + } if !cfg!(feature = "no_clause_elimination") { let mut elim = Eliminator::instantiate(&state.config, &state.cnf); state.flush("clause subsumption, "); @@ -364,7 +366,7 @@ fn search( } if let Some(na) = asg.best_assigned() { state.flush(""); - state.flush(format!("unreachable core: {}", na)); + state.flush(format!("unreachable core: {} ", na)); } } } From a5502338ae276c74766a73c8c95a2db2b381e506 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Wed, 19 Oct 2022 19:38:09 +0900 Subject: [PATCH 22/29] (reduce) change reduction parameters to keep much clauses if the total amount is small --- src/cdb/db.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 7f6832a2a..ade1f7677 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -1025,7 +1025,9 @@ impl ClauseDBIF for ClauseDB { // there're exception. Since this is the pre-stage of clause vivification, // we want keep usefull clauses as many as possible. // Therefore I save the clauses which will become vivification targets. - let thr = (self.lb_entanglement.get_slow() + 1.0).min(self.lbd.get_fast().max(5.0)) as u16; + // let thr = (self.lb_entanglement.get_slow() + 1.0).min(self.lbd.get_fast().max(5.0)) as u16; + let extra = 100.0 / (self.num_learnt as f64).log2(); + let thr = ((self.lb_entanglement.get_slow() + self.lbd.get_slow()).log2() + extra) as u16; for i in &perm[keep..] { let c = &self.clause[i.to()]; if !c.is_vivify_target() || thr < c.rank { From cfdc7aafe95cfaa4989fe7b723f0df7d9264651a Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 15:23:20 +0900 Subject: [PATCH 23/29] (reduce) memory-pressure --- src/cdb/db.rs | 12 ++++++++---- src/cdb/mod.rs | 9 +++++++-- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index ade1f7677..7ebe5001a 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -48,6 +48,7 @@ impl Default for ClauseDB { num_reduction: 0, num_reregistration: 0, lb_entanglement: Ema2::new(1_000).with_slow(80_000).with_value(2.0), + last_reduction_threshold: 0, eliminated_permanent: Vec::new(), } } @@ -1022,18 +1023,21 @@ impl ClauseDBIF for ClauseDB { } perm.sort(); // Worse half of `perm` should be discarded now. But many people thought - // there're exception. Since this is the pre-stage of clause vivification, + // there're exceptions. Since this is the pre-stage of clause vivification, // we want keep usefull clauses as many as possible. // Therefore I save the clauses which will become vivification targets. - // let thr = (self.lb_entanglement.get_slow() + 1.0).min(self.lbd.get_fast().max(5.0)) as u16; - let extra = 100.0 / (self.num_learnt as f64).log2(); - let thr = ((self.lb_entanglement.get_slow() + self.lbd.get_slow()).log2() + extra) as u16; + // And since the current Splr adopts stage-based GC policy, I drop this simple halve'em if doubled, + // based on memomy pressure and clause sizes used in conflict analysis. + let entanglement = 1.5 * (self.lb_entanglement.get_slow() + self.lbd.get_slow()).powf(0.5); + let memory_pressure = 2000.0 * (self.num_learnt as f64).powf(-0.5); + let thr = (entanglement + memory_pressure).min(entanglement) as u16; for i in &perm[keep..] { let c = &self.clause[i.to()]; if !c.is_vivify_target() || thr < c.rank { self.remove_clause(ClauseId::from(i.to())); } } + self.last_reduction_threshold = thr as usize; } fn reset(&mut self) { debug_assert!(1 < self.clause.len()); diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index d2576eb05..363ac43ca 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -289,7 +289,9 @@ pub struct ClauseDB { num_reregistration: usize, /// Literal Block Entanglement /// EMA of LBD of clauses used in conflict analysis (dependency graph) - pub lb_entanglement: Ema2, + lb_entanglement: Ema2, + /// the decision level used in th last invocation of `reduce` + last_reduction_threshold: usize, // //## incremental solving @@ -311,10 +313,11 @@ pub mod property { NumLearnt, NumReduction, NumReRegistration, + ReductionThreshold, Timestamp, } - pub const USIZES: [Tusize; 9] = [ + pub const USIZES: [Tusize; 10] = [ Tusize::NumBiClause, Tusize::NumBiClauseCompletion, Tusize::NumBiLearnt, @@ -323,6 +326,7 @@ pub mod property { Tusize::NumLearnt, Tusize::NumReduction, Tusize::NumReRegistration, + Tusize::ReductionThreshold, Tusize::Timestamp, ]; @@ -338,6 +342,7 @@ pub mod property { Tusize::NumLearnt => self.num_learnt, Tusize::NumReduction => self.num_reduction, Tusize::NumReRegistration => self.num_reregistration, + Tusize::ReductionThreshold => self.last_reduction_threshold, #[cfg(feature = "clause_rewarding")] Tusize::Timestamp => self.tick, From 29e82608499d35237791b48ac26e6b84ca3cc71f Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 15:29:22 +0900 Subject: [PATCH 24/29] (search) a snapshot --- src/solver/search.rs | 75 ++++++++++++++++++++++++++++++-------------- 1 file changed, 52 insertions(+), 23 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index 592db5127..ed1a303d9 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,7 +239,9 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; - let mut best_phases_invalid = true; + let mut current_core: usize = 999_999; + let mut core_was_rebuilt: Option = None; + let mut sls_core = cdb.derefer(cdb::property::Tusize::NumClause); state.stm.initialize( (asg.derefer(assign::property::Tusize::NumUnassertedVar) as f64).sqrt() as usize, @@ -261,7 +263,7 @@ fn search( // } match handle_conflict(asg, cdb, state, &cc)? { 0 => { - best_phases_invalid = asg.best_phases_invalid(); + // best_phases_invalid = asg.best_phases_invalid(); // state.stm.reset(); } 1 => (), @@ -280,7 +282,7 @@ fn search( cdb.reduce(asg, state.stm.num_reducible()); #[cfg(feature = "trace_equivalency")] cdb.check_consistency(asg, "before simplify"); - dump_stage(state, asg, current_stage); + dump_stage(asg, cdb, state, current_stage); let next_stage: Option = state.stm.prepare_new_stage( (asg.derefer(assign::property::Tusize::NumUnassignedVar) as f64).sqrt() as usize, @@ -302,34 +304,53 @@ fn search( use cdb::StochasticLocalSearchIF; macro_rules! sls { ($assign: expr, $limit: expr) => { - state.flush("SLS "); + state.sls_index += 1; + state.flush(format!( + "SLS(#{}, core: {}, steps: {})", + state.sls_index, sls_core, $limit + )); let cls = cdb.stochastic_local_search(asg, &mut $assign, $limit); - state.sls_index += 1; - let flips = asg.override_rephasing_target(&$assign); - state.flush(format!("({} clauses, {} flips), ", cls.1, flips)); + asg.override_rephasing_target(&$assign); + sls_core = sls_core.min(cls.1); }; ($assign: expr, $improved: expr, $limit: expr) => { - state.flush("SLS"); - let stats = + state.sls_index += 1; + state.flush(format!( + "SLS(#{}, core: {}, steps: {})", + state.sls_index, sls_core, $limit + )); + let cls = cdb.stochastic_local_search(asg, &mut $assign, $limit); - if $improved(stats) { - state.sls_index += 1; + if $improved(cls) { // state.sls_index = stats.1; - let num_flipped = asg.override_rephasing_target(&$assign); - state.flush(format!( - "({} clauses, {} flips), ", - stats.1, num_flipped - )); - } else { - state.flush(", "); + asg.override_rephasing_target(&$assign); } + sls_core = sls_core.min(cls.1); + }; + } + macro_rules! scale { + ($a: expr, $b: expr) => { + ($a.saturating_sub($b.next_power_of_two().trailing_zeros()) + as f64) + .powf(1.75) as usize + + 1 }; } - if best_phases_invalid || new_segment { - best_phases_invalid = false; + let ent = cdb.refer(cdb::property::TEma::Entanglement).get() as usize; + let n = cdb.derefer(cdb::property::Tusize::NumClause); + if let Some(c) = core_was_rebuilt { + core_was_rebuilt = None; + if c < current_core { + let steps = scale!(27_u32, c) * scale!(24_u32, n) / ent; + let mut assignment = asg.best_phases_ref(Some(false)); + sls!(assignment, steps); + } + } else if new_segment { + let n = cdb.derefer(cdb::property::Tusize::NumClause); + let steps = scale!(27_u32, current_core) * scale!(24_u32, n) / ent; let mut assignment = asg.best_phases_ref(Some(false)); - sls!(assignment, 100); + sls!(assignment, steps); } } asg.select_rephasing_target(); @@ -365,6 +386,10 @@ fn search( RESTART!(asg, cdb, state); } if let Some(na) = asg.best_assigned() { + if current_core < na && core_was_rebuilt.is_none() { + core_was_rebuilt = Some(current_core); + } + current_core = na; state.flush(""); state.flush(format!("unreachable core: {} ", na)); } @@ -385,13 +410,14 @@ fn search( } /// display the current stats. before updating stabiliation parameters -fn dump_stage(state: &mut State, asg: &AssignStack, current_stage: Option) { +fn dump_stage(asg: &AssignStack, cdb: &ClauseDB, state: &mut State, current_stage: Option) { let active = true; // state.rst.enable; let cycle = state.stm.current_cycle(); let scale = state.stm.current_scale(); let stage = state.stm.current_stage(); let segment = state.stm.current_segment(); let cpr = asg.refer(assign::property::TEma::ConflictPerRestart).get(); + let reduction_threshold = cdb.derefer(cdb::property::Tusize::ReductionThreshold); let fuel = if active { state.restart.penetration_energy_charged } else { @@ -403,7 +429,10 @@ fn dump_stage(state: &mut State, asg: &AssignStack, current_stage: Option) Some(false) => Some((None, Some(cycle), stage)), Some(true) => Some((Some(segment), Some(cycle), stage)), }, - format!("scale: {:>4}, fuel:{:>9.2}, cpr:{:>8.2}", scale, fuel, cpr), + format!( + "scale: {:>4}, fuel:{:>9.2}, cpr:{:>8.2}, thr:{:>5}", + scale, fuel, cpr, reduction_threshold + ), ); } From a689e42fbd51f098446c925f7e18c15f98da14a8 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 15:31:20 +0900 Subject: [PATCH 25/29] change the definition of a 'cylcle' from an increasing sequence to a non-decreasing one --- src/solver/stage.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/solver/stage.rs b/src/solver/stage.rs index c5a685f8d..452325f1c 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -71,7 +71,8 @@ impl StageManager { self.scale = self.luby_iter.next_unchecked(); if self.scale == 1 { self.cycle += 1; - new_cycle = true; + // new_cycle = true; + new_cycle = self.cycle % 2 == 0; if self.next_is_new_segment { self.segment += 1; self.next_is_new_segment = false; @@ -89,13 +90,15 @@ impl StageManager { } /// returns the number of conflicts in the current stage pub fn current_span(&self) -> usize { - self.cycle * self.unit_size + // self.cycle * self.unit_size + (self.cycle / 2 + 1) * self.unit_size } pub fn current_stage(&self) -> usize { self.stage } pub fn current_cycle(&self) -> usize { - self.cycle + // self.cycle + self.cycle / 2 } /// returns the scaling factor used in the current span pub fn current_scale(&self) -> usize { From 392801e91226ce14dd28a094833c1475f7e7c4c6 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 19:29:03 +0900 Subject: [PATCH 26/29] Fix calculation bugs on segment number and stage span --- src/solver/stage.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 452325f1c..3342a1d6f 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -23,7 +23,7 @@ impl Instantiate for StageManager { unit_size, scale: 1, end_of_stage: unit_size, - next_is_new_segment: true, + next_is_new_segment: false, ..StageManager::default() } } @@ -40,7 +40,7 @@ impl StageManager { luby_iter: LubySeries::default(), scale: 1, end_of_stage: unit_size, - next_is_new_segment: true, + next_is_new_segment: false, } } pub fn initialize(&mut self, unit_size: usize) { From 0b5242afc41783130aa2367b323410dbe5a2e923 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 19:31:48 +0900 Subject: [PATCH 27/29] (search) fix a calculation bug on stage index in cycle --- src/solver/search.rs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/solver/search.rs b/src/solver/search.rs index ed1a303d9..21aa5cbc7 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -291,9 +291,16 @@ fn search( let scale = state.stm.current_scale(); let max_scale = state.stm.max_scale(); if cfg!(feature = "reward_annealing") { - let base = (1 << (state.stm.current_segment() - 1)) - 1; - let decay_index = state.stm.current_cycle() - base; - let decay = (decay_index as f64 - 1.0) / decay_index as f64; + let base = { + let seg = state.stm.current_segment(); + if seg == 0 { + state.stm.current_cycle() + } else { + state.stm.current_cycle() - (1 << (seg - 1)) + } + }; + let decay_index: f64 = 1.25 + base as f64; + let decay = (decay_index - 1.0) / decay_index; asg.update_activity_decay(decay); } if let Some(new_segment) = next_stage { From df18bd19e9f0111c291a44758343a0b298d6f685 Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 19:33:35 +0900 Subject: [PATCH 28/29] fix a compilation error without 'stochastic_local_search' --- src/state.rs | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/state.rs b/src/state.rs index 0112b57ab..2e0f3fea3 100644 --- a/src/state.rs +++ b/src/state.rs @@ -116,10 +116,6 @@ pub struct State { /// chronoBT threshold pub chrono_bt_threshold: DecisionLevel, - #[cfg(feature = "stochastic_local_search")] - /// criteria for SLS - pub sls_index: usize, - /// hold the previous number of non-conflicting assignment pub last_asg: usize, /// working place to build learnt clauses @@ -130,6 +126,8 @@ pub struct State { pub progress_cnt: usize, /// keep the previous statistics values pub record: ProgressRecord, + /// criteria for SLS + pub sls_index: usize, /// start clock for timeout handling pub start: Instant, /// upper limit for timeout handling @@ -158,14 +156,12 @@ impl Default for State { #[cfg(feature = "chronoBT")] chrono_bt_threshold: 100, - #[cfg(feature = "stochastic_local_search")] - sls_index: 0, - last_asg: 0, new_learnt: Vec::new(), derive20: Vec::new(), progress_cnt: 0, record: ProgressRecord::default(), + sls_index: 0, start: Instant::now(), time_limit: 0.0, log_messages: Vec::new(), From dbf2e9bcfd2e63db6ff9bd4e4cc5b0aea09436ed Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Sat, 22 Oct 2022 19:34:26 +0900 Subject: [PATCH 29/29] (reduce) a parameter tuning --- src/cdb/db.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdb/db.rs b/src/cdb/db.rs index 7ebe5001a..be7ff0c34 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -1028,7 +1028,7 @@ impl ClauseDBIF for ClauseDB { // Therefore I save the clauses which will become vivification targets. // And since the current Splr adopts stage-based GC policy, I drop this simple halve'em if doubled, // based on memomy pressure and clause sizes used in conflict analysis. - let entanglement = 1.5 * (self.lb_entanglement.get_slow() + self.lbd.get_slow()).powf(0.5); + let entanglement = 1.75 * (self.lb_entanglement.get_slow() + self.lbd.get_slow()).powf(0.5); let memory_pressure = 2000.0 * (self.num_learnt as f64).powf(-0.5); let thr = (entanglement + memory_pressure).min(entanglement) as u16; for i in &perm[keep..] {