diff --git a/Cargo.toml b/Cargo.toml index a26420159..9667c6bf5 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" @@ -17,49 +17,64 @@ bitflags = "^1.3" [features] default = [ - # "boundary_check", # for DEBUG - # "bi_clause_completion", # increase memory pressure - # "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", # for big problems since 0.17(need to evalate with larger timeout) + # "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' +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" ] -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 = [] -support_user_assumption = [] -suppress_reason_chain = [] -trace_analysis = [] -trace_elimination = [] -trace_equivalency = [] -trail_saving = [] -unsafe_access = [] +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" 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/select.rs b/src/assign/select.rs index 4ef766f61..8e439c4fe 100644 --- a/src/assign/select.rs +++ b/src/assign/select.rs @@ -6,6 +6,7 @@ use super::property; use { super::{AssignStack, VarHeapIF}, crate::types::*, + std::collections::HashMap, }; /// ```ignore @@ -26,6 +27,10 @@ macro_rules! var_assign { /// API for var selection, depending on an internal heap. pub trait VarSelectIF { + /// return best phases + fn best_phases_ref(&mut self, default_value: Option) -> HashMap; + /// 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); @@ -41,6 +46,44 @@ pub trait VarSelectIF { } impl VarSelectIF for AssignStack { + 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) { + default_value.map(|b| (vi, b)) + } else { + Some(( + vi, + self.best_phases.get(&vi).map_or( + self.assign[vi].unwrap_or_else(|| v.is(FlagVar::PHASE)), + |(b, _)| *b, + ), + )) + } + }) + .collect::>() + } + 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) { + 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 + } #[cfg(feature = "rephase")] fn select_rephasing_target(&mut self) { if self.best_phases.is_empty() { 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; 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..be7ff0c34 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,16 +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; + // 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.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..] { 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 2eb084fed..363ac43ca 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 @@ -21,9 +23,11 @@ pub use self::{ binary::{BinaryLinkDB, BinaryLinkList}, cid::ClauseIdIF, property::*, + sls::StochasticLocalSearchIF, unsat_certificate::CertificationStore, vivify::VivifyIF, }; + use { self::ema::ProgressLBD, crate::{assign::AssignIF, types::*}, @@ -285,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 @@ -307,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, @@ -319,6 +326,7 @@ pub mod property { Tusize::NumLearnt, Tusize::NumReduction, Tusize::NumReRegistration, + Tusize::ReductionThreshold, Tusize::Timestamp, ]; @@ -334,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, diff --git a/src/cdb/sls.rs b/src/cdb/sls.rs new file mode 100644 index 000000000..d47b7de19 --- /dev/null +++ b/src/cdb/sls.rs @@ -0,0 +1,116 @@ +/// Implementation of Stochastic Local Search +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); +} + +impl StochasticLocalSearchIF for ClauseDB { + fn stochastic_local_search( + &mut self, + _asg: &impl AssignIF, + assignment: &mut HashMap, + limit: usize, + ) -> (usize, usize) { + let mut returns: (usize, usize) = (0, 0); + let mut last_flip = self.num_clause; + let mut seed = 721_109; + 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() { + flip_target.entry(l.vi()).or_insert(0); + } + } + } + } + if step == 1 { + returns.0 = unsat_clauses; + // returns.0 = level as usize; + } + returns.1 = unsat_clauses; + // returns.1 = level as usize; + if unsat_clauses == 0 || step == limit { + break; + } + 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 }; + let factor = |vi| beta.powf(-(*flip_target.get(vi).unwrap() as f64)); + let vars = c.lits.iter().map(|l| l.vi()).collect::>(); + 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); + if index <= sum { + assignment.entry(*vi).and_modify(|e| *e = !*e); + last_flip = *vi; + break; + } + } + } else { + break; + } + } + returns + } +} + +impl Clause { + fn is_falsified( + &self, + assignment: &HashMap, + flip_target: &mut HashMap, + ) -> 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; + } + None => unreachable!(), + _ => (), + } + } + if num_sat == 0 { + true + } else { + *flip_target.entry(sat_vi).or_insert(0) += 1; + false + } + } +} 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 3e2492607..21aa5cbc7 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -239,6 +239,9 @@ fn search( ) -> Result { let mut current_stage: Option = Some(true); let mut num_learnt = 0; + 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, @@ -255,8 +258,16 @@ 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 => { + // best_phases_invalid = asg.best_phases_invalid(); + // state.stm.reset(); + } + 1 => (), + _ => num_learnt += 1, } if state.stm.stage_ended(num_learnt) { if let Some(p) = state.elapsed() { @@ -267,10 +278,11 @@ 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"); - 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, @@ -278,24 +290,88 @@ fn search( ); let scale = state.stm.current_scale(); let max_scale = state.stm.max_scale(); - #[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; + if cfg!(feature = "reward_annealing") { + 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 { + // a beginning of a new cycle #[cfg(feature = "rephase")] - asg.select_rephasing_target(); + { + if cfg!(feature = "stochastic_local_search") { + use cdb::StochasticLocalSearchIF; + macro_rules! sls { + ($assign: expr, $limit: expr) => { + 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); + asg.override_rephasing_target(&$assign); + sls_core = sls_core.min(cls.1); + }; + ($assign: expr, $improved: expr, $limit: expr) => { + 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(cls) { + // state.sls_index = stats.1; + 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 + }; + } + 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, steps); + } + } + 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 = "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; @@ -306,7 +382,6 @@ fn search( } } } - asg.clear_asserted_literals(cdb)?; state.progress(asg, cdb); asg.handle(SolverEvent::Stage(scale)); state.restart.set_stage_parameters(scale); @@ -318,8 +393,12 @@ 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)); + state.flush(format!("unreachable core: {} ", na)); } } } @@ -338,13 +417,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 { @@ -356,7 +436,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 + ), ); } diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 429c5670c..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) { @@ -49,8 +49,13 @@ 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 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 { @@ -66,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; @@ -84,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 { diff --git a/src/state.rs b/src/state.rs index 3d979c16c..2e0f3fea3 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 + SLS, /// don't use this dummy (sentinel at the tail). EndOfStatIndex, } @@ -110,8 +112,10 @@ 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, + /// hold the previous number of non-conflicting assignment pub last_asg: usize, /// working place to build learnt clauses @@ -122,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 @@ -146,12 +152,16 @@ impl Default for State { #[cfg(feature = "support_user_assumption")] conflicts: Vec::new(), + + #[cfg(feature = "chronoBT")] chrono_bt_threshold: 100, + 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(), @@ -512,19 +522,14 @@ impl StateIF for State { ), ); println!( - "\x1B[2K misc|vivC:{}, subC:{}, core:{}, /ppc:{}", + "\x1B[2K misc|vivC:{}, !SLS:{}, core:{}, /ppc:{}", im!( "{:>9}", self, LogUsizeId::VivifiedClause, self[Stat::VivifiedClause] ), - im!( - "{:>9}", - self, - LogUsizeId::SubsumedClause, - self[Stat::SubsumedClause] - ), + im!("{:>9}", self, LogUsizeId::SLS, self.sls_index), im!( "{:>9}", self, @@ -835,6 +840,11 @@ pub enum LogUsizeId { VivifiedVar, Vivify, + // + //## Stochastic Local Search + // + SLS, + // the sentinel End, } @@ -856,6 +866,7 @@ pub enum LogF64Id { PropagationPerConflict, LiteralBlockEntanglement, RestartEnergy, + End, }