diff --git a/Cargo.toml b/Cargo.toml index 4d6801272..ea3aad11e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -29,8 +29,7 @@ default = [ ### Heuristics # "bi_clause_completion", # "clause_rewarding", - # "dynamic_restart_threshold", - "just_used", + "keep_just_used_clauses", "LRB_rewarding", "reason_side_rewarding", # "rephase", @@ -62,7 +61,6 @@ 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 graph_view = [ @@ -73,7 +71,7 @@ graph_view = [ ] incremental_solver = [] # for all solution SAT sover; requires no cluse_elimination interleave = [] # switch to multi-step search IF -just_used = [] # Var and clause have 'just_used' flags +keep_just_used_clauses = [] # Var and clause have 'just_used' flags LRB_rewarding = [] # Vearning Rate Based rewarding, a new var activity criteria no_IO = [] # to embed Splr into non-std environments platform_wasm = [ @@ -84,7 +82,7 @@ rephase = [ # search around the best-so-far candidate repeat "best_phases_tracking", ] reward_annealing = [] # use bigger and smaller decay rates cycliclly -spin = [] +spin = [] # [experimental] a sort of criteria for var categorization stochastic_local_search = [ # since 0.17 # "reward_annealing", "rephase", diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index f252e9ffe..de8362115 100644 --- a/src/assign/propagate.rs +++ b/src/assign/propagate.rs @@ -375,7 +375,7 @@ impl PropagateIF for AssignStack { .unwrap_or(self.root_level); debug_assert_eq!(self.assigned(other), None); - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] c.turn_on(FlagClause::USED); self.assign_by_implication( other, diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index d40772fa1..0728dbd5a 100644 --- a/src/cdb/mod.rs +++ b/src/cdb/mod.rs @@ -290,7 +290,7 @@ impl ClauseDBIF for ClauseDB { self.clause[ci].activity = 0.0; self.clause[ci].timestamp = self.tick; } - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] { self.clause[ci].turn_on(FlagClause::USED); } @@ -518,7 +518,7 @@ impl ClauseDBIF for ClauseDB { let rank = c.update_lbd(asg, lbd_temp); let learnt = c.is(FlagClause::LEARNT); if learnt { - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] c.turn_on(FlagClause::USED); #[cfg(feature = "clause_rewarding")] self.reward_at_analysis(ci); @@ -529,7 +529,7 @@ impl ClauseDBIF for ClauseDB { learnt } /// reduce the number of 'learnt' or *removable* clauses. - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] fn reduce(&mut self, asg: &mut impl AssignIF, _setting: ReductionType) { // let ClauseDB { // ref mut clause, @@ -586,7 +586,7 @@ impl ClauseDBIF for ClauseDB { // self.delete_clause(i.to()); // } } - #[cfg(not(feature = "just_used"))] + #[cfg(not(feature = "keep_just_used_clauses"))] #[allow(unreachable_code, unused_variables)] fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType) { impl Clause { @@ -619,7 +619,7 @@ impl ClauseDBIF for ClauseDB { ReductionType::LBDonALL(_, _) => true, #[cfg(feature = "clause_rewarding")] ReductionType::ClauseActivity => false, - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] ReductionType::ClauseUsed => false, }; for (ci, c) in clause @@ -659,7 +659,7 @@ impl ClauseDBIF for ClauseDB { } #[cfg(feature = "clause_rewarding")] ReductionType::ClauseActivity => perm.push(OrderedProxy::new(ci, -c.activity)), - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] ReductionType::ClauseUsed => unreachable!(), } } @@ -670,7 +670,7 @@ impl ClauseDBIF for ClauseDB { ReductionType::LBDonALL(_, scale) => (perm.len() as f64).powf(1.0 - scale) as usize, #[cfg(feature = "clause_rewarding")] ReductionType::ClauseActivity => (perm.len() as f64).powf(0.75) as usize, - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] ReductionType::ClauseUsed => unreachable!(), }; if perm.is_empty() { @@ -685,7 +685,7 @@ impl ClauseDBIF for ClauseDB { } #[cfg(feature = "clause_rewarding")] ReductionType::ClauseActivity => keep as f64 / alives as f64, - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] ReductionType::ClauseUsed => unreachable!(), }; perm.sort(); @@ -1242,7 +1242,7 @@ pub enum ReductionType { LBDonALL(u16, f64), #[cfg(feature = "clause_rewarding")] ClauseActivity, - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] ClauseUsed, } @@ -1373,7 +1373,7 @@ mod tests { assert!(!c.is_dead()); assert!(!c.is(FlagClause::LEARNT)); - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] assert!(c.is(FlagClause::USED)); let c2 = cdb .new_clause(&mut asg, &mut vec![lit(-1), lit(2), lit(3)], true) @@ -1381,7 +1381,7 @@ mod tests { let c = &cdb[c2]; assert!(!c.is_dead()); assert!(c.is(FlagClause::LEARNT)); - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] assert!(c.is(FlagClause::USED)); } #[test] diff --git a/src/cdb/vivify.rs b/src/cdb/vivify.rs index 1fd333b83..5a5ae9270 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -102,7 +102,7 @@ impl VivifyIF for ClauseDB { } AssignReason::Implication(wli) => { if wli.as_ci() == ci && clits.len() == decisions.len() { - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] self.clause[wli.as_ci()].turn_on(FlagClause::USED); asg.backtrack_sandbox(); continue 'next_clause; @@ -280,7 +280,7 @@ impl AssignStack { seen[bil.vi()] = key; } AssignReason::Implication(wli) => { - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] cdb.clause[wli.as_ci()].turn_on(FlagClause::USED); for (i, r) in cdb[wli.as_ci()].iter().enumerate() { if i == wli.as_wi() { diff --git a/src/config.rs b/src/config.rs index 8284baccf..f9a133178 100644 --- a/src/config.rs +++ b/src/config.rs @@ -267,8 +267,6 @@ impl Config { "stage-based clause elimination", #[cfg(feature = "clause_vivification")] "stage-based clause vivification", - #[cfg(feature = "dynamic_restart_threshold")] - "stage-based dynamic restart threshold", #[cfg(feature = "EMA_calibration")] "EMA calibration", #[cfg(feature = "EVSIDS")] @@ -277,8 +275,8 @@ impl Config { "incremental solver", #[cfg(feature = "interleave")] "interleaving slover", - #[cfg(feature = "just_used")] - "use 'just used' flag", + #[cfg(feature = "keep_just_used_clauses")] + "keep clauses used in the last cycle", #[cfg(feature = "LRB_rewarding")] "Learning-Rate Based rewarding", #[cfg(feature = "reason_side_rewarding")] diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index af9e9e556..4766834e1 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -158,7 +158,6 @@ pub fn eliminate_var( */ elim[vi].clear(); asg.handle(SolverEvent::Eliminate(vi)); - state.restart.handle(SolverEvent::Eliminate(vi)); elim.backward_subsumption_check(asg, cdb) } diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index 3165dbd50..5c6999bc0 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -113,7 +113,6 @@ pub fn handle_conflict( unreachable!("handle_conflict::root_level_conflict_by_assertion"); } let vi = l0.vi(); - state.restart.handle(SolverEvent::Assert(vi)); state.stm.handle(SolverEvent::Assert(vi)); cdb.handle(SolverEvent::Assert(vi)); return Ok(0); @@ -150,7 +149,7 @@ pub fn handle_conflict( } } AssignReason::Implication(r) => { - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] cdb[r.as_ci()].turn_on(FlagClause::USED); for l in cdb[r.as_ci()].iter() { let vi = l.vi(); @@ -353,7 +352,7 @@ fn conflict_analyze( if !cdb[ci].is(FlagClause::LEARNT) { state.derive20.push(ci); } else { - #[cfg(feature = "just_used")] + #[cfg(feature = "keep_just_used_clauses")] cdb[ci].turn_on(FlagClause::USED); } if max_lbd < cdb[ci].rank { diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 4fd5dc2f3..991a5b025 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -3,8 +3,6 @@ mod build; /// Module 'conflict' handles conflicts. mod conflict; -/// Module `restart` provides restart heuristics. -pub mod restart; /// CDCL search engine mod search; /// Stage manger (was Stabilizer) @@ -14,7 +12,6 @@ mod validate; pub use self::{ build::SatSolverIF, - restart::{RestartIF, RestartManager}, search::{SearchState, SolveIF}, stage::StageManager, validate::ValidateIF, diff --git a/src/solver/restart.rs b/src/solver/restart.rs deleted file mode 100644 index 6c445e5b3..000000000 --- a/src/solver/restart.rs +++ /dev/null @@ -1,62 +0,0 @@ -//! Module `restart` provides restart heuristics. -use crate::types::*; - -/// API for [`restart`](`crate::solver::RestartIF::restart`) -pub trait RestartIF: Instantiate { - /// check blocking and forcing restart condition. - fn restart(&mut self, ldb: &EmaView, ent: &EmaView) -> bool; - /// set stabilization parameters - fn set_stage_parameters(&mut self, step: usize); - /// adjust restart threshold - fn set_segment_parameters(&mut self, segment_scale: usize); -} - -const FUEL: f64 = 1.0; - -/// `RestartManager` provides restart API and holds data about restart conditions. -#[derive(Clone, Debug, Default)] -pub struct RestartManager { - penetration_energy: f64, - pub penetration_energy_charged: f64, - penetration_energy_unit: f64, -} - -impl Instantiate for RestartManager { - fn instantiate(_config: &Config, _cnf: &CNFDescription) -> Self { - RestartManager { - penetration_energy: FUEL, - penetration_energy_charged: FUEL, - penetration_energy_unit: FUEL, - } - } - fn handle(&mut self, e: SolverEvent) { - if e == SolverEvent::Restart { - self.penetration_energy = self.penetration_energy_charged; - } - } -} - -impl RestartIF for RestartManager { - fn restart(&mut self, lbd: &EmaView, _env: &EmaView) -> bool { - 1.15 < lbd.trend() - /* if 0.1 < self.penetration_energy { - // self.penetration_energy -= env.trend(); - self.penetration_energy -= 1.0 / 16.0; - false - } else { - 1.2 < lbd.trend() - } */ - /* self.penetration_energy = (self.penetration_energy - 0.3 * (lbd.trend() - 0.9)) - .min(self.penetration_energy_charged); - self.penetration_energy < 0.0 */ - } - fn set_segment_parameters(&mut self, _segment_scale: usize) { - // self.penetration_energy_unit *= 10.0_f64.powf(-0.1); - } - fn set_stage_parameters(&mut self, stage_scale: usize) { - // let e = self.penetration_energy_unit * (1.0 + stage_scale as f64).log2(); - let e = self.penetration_energy_unit * stage_scale as f64; - self.penetration_energy_charged = e; - self.penetration_energy = e; - } -} diff --git a/src/solver/search.rs b/src/solver/search.rs index a31e25746..d9d747426 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -1,9 +1,6 @@ //! Conflict-Driven Clause Learning Search engine use { - super::{ - conflict::handle_conflict, restart::RestartIF, Certificate, Solver, SolverEvent, - SolverResult, - }, + super::{conflict::handle_conflict, Certificate, Solver, SolverEvent, SolverResult}, crate::{ assign::{self, AssignIF, AssignStack, PropagateIF, VarManipulateIF, VarSelectIF}, cdb::{self, ClauseDB, ClauseDBIF, ReductionType, VivifyIF}, @@ -485,7 +482,6 @@ impl SolveIF for Solver { ss.current_span = state.stm.current_span(); let scale = state.stm.current_scale(); asg.handle(SolverEvent::Stage(scale)); - let max_scale = state.stm.max_scale(); if let Some(new_segment) = next_stage { // a beginning of a new cycle if cfg!(feature = "reward_annealing") { @@ -534,9 +530,6 @@ impl SolveIF for Solver { state[Stat::Simplify] += 1; state[Stat::SubsumedClause] = elim.num_subsumed; } - if cfg!(feature = "dynamic_restart_threshold") { - state.restart.set_segment_parameters(max_scale); - } } if new_segment { state.exploration_rate_ema.update(1.0); @@ -547,7 +540,6 @@ impl SolveIF for Solver { return Err(SolverError::TimeOut); } state.progress(asg, cdb); - state.restart.set_stage_parameters(scale); ss.previous_stage = next_stage; ss.elapsed_time = p; return Ok(None); @@ -654,7 +646,6 @@ impl SolveIF for Solver { /// display the current stats. before updating stabiliation parameters fn dump_stage(asg: &AssignStack, cdb: &mut ClauseDB, state: &mut State, shift: &Option) { - let active = true; // state.rst.enable; let cycle = state.stm.current_cycle(); let span = state.stm.current_span(); let stage = state.stm.current_stage(); @@ -662,18 +653,13 @@ fn dump_stage(asg: &AssignStack, cdb: &mut ClauseDB, state: &mut State, shift: & let cpr = asg.refer(assign::property::TEma::ConflictPerRestart).get(); let vdr = asg.derefer(assign::property::Tf64::VarDecayRate); let cdt = cdb.derefer(cdb::property::Tf64::ReductionThreshold); - let fuel = if active { - state.restart.penetration_energy_charged - } else { - f64::NAN - }; state.log( match shift { None => Some((None, None, stage)), Some(false) => Some((None, Some(cycle), stage)), Some(true) => Some((Some(segment), Some(cycle), stage)), }, - format!("{span:>7}, fuel:{fuel:>9.2}, cpr:{cpr:>8.2}, vdr:{vdr:>3.2}, cdt:{cdt:>5.2}"), + format!("{span:>7}, cpr:{cpr:>8.2}, vdr:{vdr:>3.2}, cdt:{cdt:>5.2}"), ); } diff --git a/src/state.rs b/src/state.rs index 837c56382..5f023d3a6 100644 --- a/src/state.rs +++ b/src/state.rs @@ -6,7 +6,7 @@ use std::time::{Duration, Instant}; use { crate::{ assign, cdb, - solver::{RestartManager, SolverEvent, StageManager}, + solver::{SolverEvent, StageManager}, types::*, }, std::{ @@ -83,8 +83,8 @@ pub struct State { pub cnf: CNFDescription, /// collection of statistics data pub stats: [usize; Stat::EndOfStatIndex as usize], - // Restart - pub restart: RestartManager, + // // Restart + // pub restart: RestartManager, /// StageManager pub stm: StageManager, /// problem description @@ -138,7 +138,7 @@ impl Default for State { config: Config::default(), cnf: CNFDescription::default(), stats: [0; Stat::EndOfStatIndex as usize], - restart: RestartManager::default(), + // restart: RestartManager::default(), stm: StageManager::default(), target: CNFDescription::default(), reflection_interval: 10_000, @@ -188,7 +188,7 @@ impl Instantiate for State { State { config: config.clone(), cnf: cnf.clone(), - restart: RestartManager::instantiate(config, cnf), + // restart: RestartManager::instantiate(config, cnf), stm: StageManager::instantiate(config, cnf), target: cnf.clone(), time_limit: config.c_timeout, @@ -207,7 +207,7 @@ impl Instantiate for State { SolverEvent::Reinitialize => (), SolverEvent::Restart => { self[Stat::Restart] += 1; - self.restart.handle(SolverEvent::Restart); + // self.restart.handle(SolverEvent::Restart); } SolverEvent::Stage(_) => (), @@ -446,7 +446,7 @@ impl StateIF for State { let rst_num_rst: usize = self[Stat::Restart]; let rst_asg: &EmaView = asg.refer(assign::property::TEma::AssignRate); let rst_lbd: &EmaView = cdb.refer(cdb::property::TEma::LBD); - let rst_eng: f64 = self.restart.penetration_energy_charged; + let rst_eng: f64 = 0.0; // self.restart.penetration_energy_charged; let stg_segment: usize = self.stm.current_segment(); if self.config.use_log {