diff --git a/Cargo.toml b/Cargo.toml index 44c212c90..9b876dea6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "splr" -version = "0.16.3" +version = "0.17.0" authors = ["Narazaki Shuji "] description = "A modern CDCL SAT solver in Rust" edition = "2021" @@ -11,53 +11,74 @@ homepage = "https://github.com/shnarazk/splr" keywords = ["SAT", "SAT-solver", "logic", "satisfiability"] categories = ["science", "mathematics"] default-run = "splr" +rust-version = "1.65" [dependencies] bitflags = "^1.3" [features] default = [ - # "boundary_check", # for DEBUG - # "bi_clause_completion", # increase memory pressure - # "no_clause_elimination", + ### Essential + # "incremental_solver", + "unsafe_access", + + ### Heuristics + # "bi_clause_completion", # "clause_rewarding", - "clause_vivification", "dynamic_restart_threshold", - # "incremental_solver", "LRB_rewarding", - # "maintain_watch_cache", # for DEBUG "reason_side_rewarding", "rephase", + "reward_annealing", + # "stochastic_local_search", # "suppress_reason_chain", + "two_mode_reduction", "trail_saving", - "unsafe_access" + + ### Logic formula processor + # "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 = [] # this will 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", + "rephase", ] -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"] -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 +two_mode_reduction = [] # exploration mode and exploitation mode since 0.17 +unsafe_access = [] # access elements of vectors without boundary checking [profile.release] lto = "fat" diff --git a/ChangeLog.md b/ChangeLog.md index 8840f27b2..47d1f7443 100644 --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,3 +1,16 @@ +## 0.17.0, 2023-01-30 + +- (Breaking change) `Certificate::try_from` returns `Ok` values even if a given vector + contains empty clauses. All expressions corresponding to valid CNFs should be + converted to `Certificate` successfully. On the other hand, `Solver::try_from` still + returns `SolverError::EmptyClause`. (#191, #196, #197) +- Add a new feature 'reward_annealing' (#187) +- Fix misc wrong calculations on Luby series and stage-cycle-segment model (#194) +- Fix build errors without feature 'trial_saving' or 'rephase' (#202, #205) +- clause reduction uses revised parameters matching a Luby series based parameter shifting + model (#195) +- add feature 'two_mode_reduction' + ## 0.16.3, 2022-09-16 - Fix another bug on `add_var` and `add_assignment` (#183) diff --git a/README.md b/README.md index f39b80a33..243d02c1e 100644 --- a/README.md +++ b/README.md @@ -21,11 +21,11 @@ Please check [ChangeLog](ChangeLog.md) about recent updates. Though Splr comes with **ABSOLUTELY NO WARRANTY**, I'd like to show some results. -#### Version 0.15.0 +#### Version 0.17.0 -- [SAT Competition 2021](https://satcompetition.github.io/2021/), [Benchmarks main truck](https://satcompetition.github.io/2021/benchmarks.html) -- splr-0.15.0 solved with a 300 sec timeout: - - 42 satisfiable problems: all the solutions were correct. - - 34 unsatisfiable problems: all the certifications were verified with [Grat toolchain](https://www21.in.tum.de/~lammich/grat/). +- [SAT Competition 2021](https://satcompetition.github.io/2021/), [Benchmarks main track](https://satcompetition.github.io/2021/benchmarks.html) -- splr-0.17.0 solved with a 300 sec timeout (this is one of the best of splr): + - 49 satisfiable problems: all the solutions were correct. + - 34 unsatisfiable problems: all certifications were verified with [Grat toolchain](https://www21.in.tum.de/~lammich/grat/) or [drat-trim](https://github.com/marijnheule/drat-trim). ## Install @@ -137,7 +137,7 @@ unif-k3-r4.25-v360-c1530-S1028159446-096.cnf 360,1530 |time: 204.09 s UNSATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf ``` -#### A: Verify with drat-trim +#### A: Verify with [drat-trim](https://github.com/marijnheule/drat-trim) ```plain $ drat-trim cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat @@ -283,6 +283,29 @@ for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() { } ``` +#### sample code from my [sudoku solver](https://github.com/shnarazk/sudoku_sat/) + +https://github.com/shnarazk/sudoku_sat/blob/4490b4358e5f3b72803a566323a6c8c196627f92/src/bin/sudoku400.rs#L36-L60 + +```rust + let mut solver = Solver::try_from((config, rules.as_ref())).expect("panic"); + for a in setting.iter() { + solver.add_assignment(*a).expect("panic"); + } + for ans in solver.iter().take(1) { + let mut picked = ans.iter().filter(|l| 0 < **l).collect::>(); + for _i in 1..=range { + for _j in 1..=range { + let (_i, _j, d, _b) = Cell::decode(*picked.remove(0)); + print!("{:>2} ", d); + } + println!(); + } + println!(); + } +} +``` + ### Mnemonics used in the progress message | mnemonic | meaning | @@ -319,7 +342,7 @@ for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() { ```plain A modern CDCL SAT solver in Rust -Activated features: best phase tracking, stage-based clause elimination, stage-based clause vivification, stage-based dynamic restart threshold, Learning-Rate Based rewarding, reason-side rewarding, stage-based re-phasing, trail saving, unsafe access +Activated features: best phase tracking, stage-based clause elimination, stage-based clause vivification, stage-based dynamic restart threshold, Learning-Rate Based rewarding, reason-side rewarding, stage-based re-phasing, two-mode reduction, trail saving, unsafe access USAGE: splr [FLAGS] [OPTIONS] @@ -333,13 +356,16 @@ FLAGS: -V, --version Prints version information OPTIONS: --cl Soft limit of #clauses (6MC/GB) 0 - -t, --timeout CPU time limit in sec. 5000 + --crl Clause reduction LBD threshold 5 + --cr1 Clause reduction ratio for mode1 0.20 + --cr2 Clause reduction ratio for mode2 0.05 --ecl Max #lit for clause subsume 64 --evl Grow limit of #cls in var elim. 0 --evo Max #cls for var elimination 20000 -o, --dir Output directory . -p, --proof DRAT Cert. filename proof.drat -r, --result Result filename/stdout + -t, --timeout CPU time limit in sec. 5000 --vdr Var reward decay rate 0.96 ARGS: DIMACS CNF file @@ -347,7 +373,7 @@ ARGS: ## Solver description -Splr-0.15.0 adopts the following features by default: +Splr-0.17.0 adopts the following features by default: - Learning-rate based (LRB) var rewarding and clause rewarding[4] - Reason-side var rewarding[4] @@ -360,12 +386,13 @@ Splr-0.15.0 adopts the following features by default: - re-configuration of var phases and var activities - re-configuration of trail saving extended with reason refinement based on clause quality[3]. -Splr-0.15.0 discarded various dynamic and heuristic-based control schemes used in 0.14.0. -The following figure shows the details. +(Splr-0.15.0 and upper try to discard various dynamic and heuristic-based control schemes used in the previous versions.) + +The following figure explains the flow used in the latest Splr. -![search algorithm in Splr 0.14](https://user-images.githubusercontent.com/997855/161426178-8264d3e2-e68a-4d64-86b4-906155a51039.png) +![search algorithm in Splr 0.17](https://user-images.githubusercontent.com/997855/215309646-1bfe3ea5-dcc3-42ee-9d76-99e1b07610c4.png) -Note: I use the following terms here: +I use the following terms here: - _a stage_ -- a span in which solver uses the same restart parameters - _a cycle_ -- a group of continuos spans of which the corresponding Luby values make a non-decreasing sequence - _a segment_ -- a group of continuos cycles which are separated by new maximum Luby values' occurrences diff --git a/cnfs/README.md b/cnfs/README.md new file mode 100644 index 000000000..4cc139498 --- /dev/null +++ b/cnfs/README.md @@ -0,0 +1,32 @@ +# A sample CNF collection + +### Corner cases + +If you try to build your SAT solver from scratch, they are corner cases you have to pay attention. + +- [empty-clause.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/empty-clause.cnf) +- [empty-form.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/empty-form.cnf) + +### Basic examples + +If you think to complete CDCL algorithm, check with them. + +- [sample.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/sample.cnf) +- [unsat.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unsat.cnf) +- [uf8.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf8.cnf) +- [uf20-01.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf20-01.cnf) + +### Midde scale problems + +And you think your solver is great, try them. 3-SAT problems (N=360) are hard. But your solver must solve them. + +- [uf100-010.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf100-010.cnf) +- [uf250-02.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/uf250-02.cnf) +- [unif-k3-r4.25-v360-c1530-S1028159446-096.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf) +- [unif-k3-r4.25-v360-c1530-S1293537826-039.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf) + +### Problems from the real competition + +If you catched up the implementations of modern solvers and reasech trend, try it. + +- [a_rphp035_05.cnf](https://github.com/shnarazk/splr/blob/main/cnfs/a_rphp035_05.cnf) diff --git a/flake.nix b/flake.nix index cf0d97fdb..8d6adec8f 100644 --- a/flake.nix +++ b/flake.nix @@ -14,7 +14,7 @@ stdenv.mkDerivation rec { name = "splr-${version}"; pname = "splr"; - version = "0.16.3-20220916"; + version = "0.17.0-20230129"; src = self; buildInputs = [ cargo libiconv rustc binutils ]; buildPhase = "cargo build --release"; diff --git a/misc/algorithm.tex b/misc/algorithm.tex index 1455bde4f..e5aa91526 100644 --- a/misc/algorithm.tex +++ b/misc/algorithm.tex @@ -24,19 +24,19 @@ \If{a new stage begins}{ REDUCE()\; update restart conditions\; - } - \If{a new cycle begins}{ - VIVIFY()\; - select var phases\; - } - \If{a new segment begins}{ - ELIMINATE()\; - rescale var activities\; + \If{a new cycle begins}{ + VIVIFY()\; + select var phases\; + \If{a new segment begins}{ + ELIMINATE()\; + rescale var activities\; + } + } } } } \Return{SAT}\; } -\caption{Main search loop in Splr-0.15 (src/solver/search.rs)} +\caption{Main search loop in Splr-0.17 (src/solver/search.rs)} \end{algorithm} \end{document} diff --git a/src/assign/evsids.rs b/src/assign/evsids.rs index cd47a9695..1f4f09ced 100644 --- a/src/assign/evsids.rs +++ b/src/assign/evsids.rs @@ -29,6 +29,12 @@ impl ActivityIF for AssignStack { self.activity_decay_step *= SCALE; } } + fn update_activity_decay(&mut self, _: f64) { + self.activity_decay = self + .activity_decay_default + .min(self.activity_decay + self.activity_decay_step); + self.activity_anti_decay = 1.0 - self.activity_decay; + } fn update_activity_tick(&mut self) { const INC_SCALE: f64 = 1.01; if self.ordinal == 0 { @@ -38,10 +44,4 @@ impl ActivityIF for AssignStack { self.ordinal += 1; self.activity_decay_step *= INC_SCALE; } - fn update_activity_decay(&mut self, _index: Option) { - self.activity_decay = self - .activity_decay_default - .min(self.activity_decay + self.activity_decay_step); - self.activity_anti_decay = 1.0 - self.activity_decay; - } } diff --git a/src/assign/heap.rs b/src/assign/heap.rs index dd97e1623..18f18c663 100644 --- a/src/assign/heap.rs +++ b/src/assign/heap.rs @@ -1,9 +1,10 @@ +/// /// Heap struct for selecting decision vars -use { - super::{AssignStack, TrailSavingIF}, - crate::types::*, - std::fmt, -}; +/// +use {super::AssignStack, crate::types::*, std::fmt}; + +#[cfg(feature = "trail_saving")] +use super::TrailSavingIF; /// Heap of VarId, based on var activity. // # Note @@ -187,8 +188,8 @@ impl VarOrderIF for VarIdHeap { let vs = self.heap[s]; let n = self.idxs[0]; let vn = self.heap[n as usize]; - debug_assert!(vn != 0, "Invalid VarId for heap: vn {}, n {}", vn, n); - debug_assert!(vs != 0, "Invalid VarId for heap: vs {}, n {}", vs, n); + debug_assert!(vn != 0, "Invalid VarId for heap: vn {vn}, n {n}"); + debug_assert!(vs != 0, "Invalid VarId for heap: vs {vs}, n {n}"); self.heap.swap(n as usize, s); self.idxs.swap(vn as usize, vs as usize); self.idxs[0] -= 1; @@ -197,6 +198,7 @@ impl VarOrderIF for VarIdHeap { fn len(&self) -> usize { self.idxs[0] as usize } + #[allow(clippy::unnecessary_cast)] fn insert(&mut self, vi: VarId) -> usize { if self.contains(vi) { return self.idxs[vi as usize] as usize; @@ -249,6 +251,6 @@ impl VarIdHeap { panic!("idxs {} {} {:?}", i, d[i], d); } } - println!(" - pass var_order test at {}", s); + println!(" - pass var_order test at {s}"); } } diff --git a/src/assign/learning_rate.rs b/src/assign/learning_rate.rs index 2abdc49df..5da6f8c03 100644 --- a/src/assign/learning_rate.rs +++ b/src/assign/learning_rate.rs @@ -9,6 +9,9 @@ impl ActivityIF for AssignStack { fn activity(&self, vi: VarId) -> f64 { self.var[vi].reward } + // fn activity_slow(&self, vi: VarId) -> f64 { + // self.var[vi].reward_ema.get() + // } fn set_activity(&mut self, vi: VarId, val: f64) { self.var[vi].reward = val; } @@ -23,6 +26,10 @@ impl ActivityIF for AssignStack { fn reward_at_unassign(&mut self, vi: VarId) { self.var[vi].update_activity(self.activity_decay, self.activity_anti_decay); } + fn update_activity_decay(&mut self, scaling: f64) { + self.activity_decay = scaling; + self.activity_anti_decay = 1.0 - scaling; + } // Note: `update_rewards` should be called before `cancel_until` #[inline] fn update_activity_tick(&mut self) { @@ -36,6 +43,27 @@ impl AssignStack { v.reward *= scaling; } } + // pub fn set_activity_trend(&mut self) -> f64 { + // let mut nv = 0; + // let mut inc = 0; + // let mut activity_sum: f64 = 0.0; + // // let mut dec = 1; + // for (vi, v) in self.var.iter_mut().enumerate().skip(1) { + // if v.is(FlagVar::ELIMINATED) || self.level[vi] == self.root_level { + // continue; + // } + // nv += 1; + // activity_sum += v.reward; + // let trend = v.reward_ema.trend(); + // if 1.0 < trend { + // inc += 1; + // } + // } + // self.activity_averaged = activity_sum / nv as f64; + // self.cwss = inc as f64 / nv as f64; + // // println!("inc rate:{:>6.4}", self.cwss); + // self.cwss + // } } impl Var { @@ -53,6 +81,7 @@ impl Var { self.reward += reward; self.turn_off(FlagVar::USED); } + // self.reward_ema.update(self.reward); self.reward } } diff --git a/src/assign/mod.rs b/src/assign/mod.rs index 3c8b8eef6..26d635914 100644 --- a/src/assign/mod.rs +++ b/src/assign/mod.rs @@ -20,12 +20,7 @@ mod trail_saving; /// var struct and its methods mod var; -pub use self::{ - propagate::PropagateIF, property::*, select::VarSelectIF, trail_saving::TrailSavingIF, - var::VarManipulateIF, -}; -#[cfg(any(feature = "best_phases_tracking", feature = "rephase"))] -use std::collections::HashMap; +pub use self::{propagate::PropagateIF, property::*, select::VarSelectIF, var::VarManipulateIF}; use { self::{ ema::ProgressASG, @@ -35,6 +30,12 @@ use { std::{fmt, ops::Range, slice::Iter}, }; +#[cfg(feature = "trail_saving")] +pub use self::trail_saving::TrailSavingIF; + +#[cfg(any(feature = "best_phases_tracking", feature = "rephase"))] +use std::collections::HashMap; + /// API about assignment like /// [`decision_level`](`crate::assign::AssignIF::decision_level`), /// [`stack`](`crate::assign::AssignIF::stack`), @@ -76,12 +77,13 @@ 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 + #[cfg(feature = "rephase")] + 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. fn satisfies(&self, c: &[Lit]) -> bool; - /// dump the status as a CNF - fn dump_cnf(&mut self, cdb: &impl ClauseDBIF, fname: &str); } /// Reasons of assignments @@ -102,8 +104,8 @@ impl fmt::Display for AssignReason { match self { &AssignReason::BinaryLink(_) => write!(f, "Implied by a binary clause"), AssignReason::Decision(0) => write!(f, "Asserted"), - AssignReason::Decision(lvl) => write!(f, "Decided at level {}", lvl), - AssignReason::Implication(cid) => write!(f, "Implied by {}", cid), + AssignReason::Decision(lvl) => write!(f, "Decided at level {lvl}"), + AssignReason::Implication(cid) => write!(f, "Implied by {cid}"), AssignReason::None => write!(f, "Not assigned"), } } @@ -116,7 +118,7 @@ pub struct Var { flags: FlagVar, /// a dynamic evaluation criterion like EVSIDS or ACID. reward: f64, - + // reward_ema: Ema2, #[cfg(feature = "boundary_check")] pub propagated_at: usize, #[cfg(feature = "boundary_check")] @@ -354,6 +356,30 @@ pub mod property { } } + #[derive(Clone, Copy, Debug, Eq, PartialEq)] + pub enum Tf64 { + AverageVarActivity, + CurrentWorkingSetSize, + VarDecayRate, + } + + pub const F64S: [Tf64; 3] = [ + Tf64::AverageVarActivity, + Tf64::CurrentWorkingSetSize, + Tf64::VarDecayRate, + ]; + + impl PropertyDereference for AssignStack { + #[inline] + fn derefer(&self, k: Tf64) -> f64 { + match k { + Tf64::AverageVarActivity => 0.0, // self.activity_averaged, + Tf64::CurrentWorkingSetSize => 0.0, // self.cwss, + Tf64::VarDecayRate => self.activity_decay, + } + } + } + #[derive(Clone, Copy, Debug, Eq, PartialEq)] pub enum TEma { AssignRate, diff --git a/src/assign/propagate.rs b/src/assign/propagate.rs index f969ef267..b2a432558 100644 --- a/src/assign/propagate.rs +++ b/src/assign/propagate.rs @@ -1,10 +1,13 @@ /// implement boolean constraint propagation, backjump /// This version can handle Chronological and Non Chronological Backtrack. use { - super::{AssignIF, AssignStack, TrailSavingIF, VarHeapIF, VarManipulateIF}, + super::{AssignIF, AssignStack, VarHeapIF, VarManipulateIF}, crate::{cdb::ClauseDBIF, types::*}, }; +#[cfg(feature = "trail_saving")] +use super::TrailSavingIF; + /// API for Boolean Constraint Propagation like /// [`propagate`](`crate::assign::PropagateIF::propagate`), /// [`assign_by_decision`](`crate::assign::PropagateIF::assign_by_decision`), @@ -639,7 +642,7 @@ impl PropagateIF for AssignStack { debug_assert!(!self.var[cached.vi()].is(FlagVar::ELIMINATED)); let mut other_watch_value = lit_assign!(self, cached); let mut updated_cache: Option = None; - if let Some(true) = other_watch_value { + if matches!(other_watch_value, Some(true)) { cdb.transform_by_restoring_watch_cache(propagating, &mut source, None); check_in!(cid, Propagate::SandboxCacheSatisfied(self.num_conflict)); continue 'next_clause; @@ -685,7 +688,7 @@ impl PropagateIF for AssignStack { cdb[cid].search_from = (k as u16).saturating_add(1); debug_assert!( self.assigned(!new_watch) == Some(true) - || self.assigned(!new_watch) == None + || self.assigned(!new_watch).is_none() ); check_in!( cid, diff --git a/src/assign/select.rs b/src/assign/select.rs index 4ef766f61..7d2ae8279 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,14 @@ 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, default_value: Option) -> HashMap; + #[cfg(feature = "rephase")] + /// force an assignment obtained by SLS + fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize; + /// give rewards to vars selected by SLS + fn reward_by_sls(&mut self, assignment: &HashMap) -> usize; #[cfg(feature = "rephase")] /// select rephasing target fn select_rephasing_target(&mut self); @@ -41,6 +50,51 @@ pub trait VarSelectIF { } impl VarSelectIF for AssignStack { + #[cfg(feature = "rephase")] + 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::>() + } + #[cfg(feature = "rephase")] + fn override_rephasing_target(&mut self, assignment: &HashMap) -> usize { + let mut num_flipped = 0; + for (vi, b) in assignment.iter() { + if !self.best_phases.get(vi).map_or(false, |(p, _)| *p == *b) { + num_flipped += 1; + self.best_phases.insert(*vi, (*b, AssignReason::None)); + } + } + num_flipped + } + fn reward_by_sls(&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); + } + } + 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 61f4167d9..3181ce12c 100644 --- a/src/assign/stack.rs +++ b/src/assign/stack.rs @@ -1,20 +1,18 @@ /// main struct AssignStack -#[cfg(any(feature = "best_phases_tracking", feature = "rephase"))] -use std::collections::HashMap; use { super::{ - ema::ProgressASG, AssignIF, AssignStack, PropagateIF, TrailSavingIF, Var, VarHeapIF, - VarIdHeap, VarManipulateIF, + ema::ProgressASG, AssignIF, AssignStack, PropagateIF, Var, VarHeapIF, VarIdHeap, + VarManipulateIF, }, crate::{cdb::ClauseDBIF, types::*}, std::{fmt, ops::Range, slice::Iter}, }; -#[cfg(not(feature = "no_IO"))] -use std::{ - fs::File, - io::{BufWriter, Write}, -}; +#[cfg(any(feature = "best_phases_tracking", feature = "rephase"))] +use std::collections::HashMap; + +#[cfg(feature = "trail_saving")] +use super::TrailSavingIF; impl Default for AssignStack { fn default() -> AssignStack { @@ -112,6 +110,9 @@ impl Instantiate for AssignStack { #[cfg(feature = "EVSIDS")] activity_decay: config.vrw_dcy_rat * 0.6, + #[cfg(not(feature = "EVSIDS"))] + activity_decay: config.vrw_dcy_rat, + #[cfg(feature = "EVSIDS")] activity_decay_default: config.vrw_dcy_rat, @@ -149,6 +150,7 @@ impl Instantiate for AssignStack { SolverEvent::Reinitialize => { self.cancel_until(self.root_level); debug_assert_eq!(self.decision_level(), self.root_level); + #[cfg(feature = "trail_saving")] self.clear_saved_trail(); // self.num_eliminated_vars = self // .var @@ -156,7 +158,7 @@ impl Instantiate for AssignStack { // .filter(|v| v.is(FlagVar::ELIMINATED)) // .count(); } - e => panic!("don't call asg with {:?}", e), + e => panic!("don't call asg with {e:?}"), } } } @@ -202,6 +204,10 @@ 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) } + #[cfg(feature = "rephase")] + 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; @@ -279,40 +285,6 @@ impl AssignIF for AssignStack { } false } - /// dump all active clauses and assertions as a CNF file. - #[cfg(not(feature = "no_IO"))] - fn dump_cnf(&mut self, cdb: &impl ClauseDBIF, fname: &str) { - for vi in 1..self.var.len() { - if self.var(vi).is(FlagVar::ELIMINATED) && self.assign[vi].is_some() { - panic!("conflicting var {} {:?}", vi, self.assign[vi]); - } - } - if let Ok(out) = File::create(&fname) { - let mut buf = BufWriter::new(out); - let nv = self.num_vars; - let na = self.len_upto(0); - // let nc: usize = cdb.derefer(cdb::property::Tusize::NumClause); - let nc = cdb.iter().skip(1).filter(|c| !c.is_dead()).count(); - - buf.write_all(format!("p cnf {} {}\n", nv, nc + na).as_bytes()) - .unwrap(); - for c in cdb.iter().skip(1) { - if c.is_dead() { - continue; - } - for l in c.iter() { - buf.write_all(format!("{} ", i32::from(*l)).as_bytes()) - .unwrap(); - } - buf.write_all(b"0\n").unwrap(); - } - buf.write_all(b"c from trail\n").unwrap(); - for x in self.trail.iter().take(self.len_upto(0)) { - buf.write_all(format!("{} 0\n", i32::from(*x)).as_bytes()) - .unwrap(); - } - } - } } impl fmt::Display for AssignStack { diff --git a/src/assign/var.rs b/src/assign/var.rs index 18c9dcda9..93fc0a297 100644 --- a/src/assign/var.rs +++ b/src/assign/var.rs @@ -11,9 +11,9 @@ use { impl Default for Var { fn default() -> Var { Var { - reward: 0.0, flags: FlagVar::empty(), - + reward: 0.0, + // reward_ema: Ema2::new(200).with_slow(4_000), #[cfg(feature = "boundary_check")] propagated_at: 0, #[cfg(feature = "boundary_check")] diff --git a/src/bin/dmcr.rs b/src/bin/dmcr.rs index de5991aa3..af53acd1a 100644 --- a/src/bin/dmcr.rs +++ b/src/bin/dmcr.rs @@ -55,7 +55,7 @@ impl TargetOpts { "no-color" => self.no_color = true, "help" => help = true, "version" => version = true, - _ => panic!("invalid flag: {}", name), + _ => panic!("invalid flag: {name}"), } } else if options_path.contains(&name) { if options_path.contains(&name) { @@ -65,10 +65,10 @@ impl TargetOpts { _ => panic!("not"), } } else { - panic!("no argument for {}", name); + panic!("no argument for {name}"); } } else { - panic!("invalid argument: {}", name); + panic!("invalid argument: {name}"); } } } else if let Some(name) = arg.strip_prefix('-') { @@ -85,18 +85,18 @@ impl TargetOpts { if let Some(val) = iter.next() { match name { "a" => self.assign = Some(PathBuf::from(val)), - _ => panic!("invalid option: {}", name), + _ => panic!("invalid option: {name}"), } } else { - panic!("no argument for {}", name); + panic!("no argument for {name}"); } } } else if !self.problem.exists() || self.problem.to_string_lossy() != arg { - panic!("invalid argument: {}", arg); + panic!("invalid argument: {arg}"); } } if help { - println!("{}\n{}", ABOUT, HELP_MESSAGE); + println!("{ABOUT}\n{HELP_MESSAGE}"); std::process::exit(0); } if version { @@ -138,7 +138,7 @@ fn main() { (RED, GREEN, BLUE) }; let mut s = Solver::build(&config).expect("failed to load"); - if args.assign == None { + if args.assign.is_none() { args.assign = Some(PathBuf::from(format!( "ans_{}", Path::new(&args.problem) @@ -225,7 +225,7 @@ fn read_assignment(rs: &mut dyn BufRead, cnf: &str, assign: &Option) -> buf.clear(); continue; } else if buf.starts_with("s UNSATISFIABLE") { - println!("{} seems an unsatisfiable problem. I can't handle it.", cnf); + println!("{cnf} seems an unsatisfiable problem. I can't handle it."); return None; } else if let Some(asg) = assign { println!("{} seems an illegal format file.", asg.to_str().unwrap(),); @@ -240,12 +240,12 @@ fn read_assignment(rs: &mut dyn BufRead, cnf: &str, assign: &Option) -> match s.parse::() { Ok(0) => break, Ok(x) => v.push(x), - Err(e) => panic!("{} by {}", e, s), + Err(e) => panic!("{e} by {s}"), } } return Some(v); } - panic!("Failed to parse here: {}", buf); + panic!("Failed to parse here: {buf}"); } Err(e) => panic!("{}", e), } diff --git a/src/bin/splr.rs b/src/bin/splr.rs index 184dc36b0..07d42ade1 100644 --- a/src/bin/splr.rs +++ b/src/bin/splr.rs @@ -32,9 +32,9 @@ fn colored(v: Result, no_color: bool) -> Cow<'static, str> { } } else { match v { - Ok(false) => Cow::from(format!("{}s UNSATISFIABLE{}", BLUE, RESET)), - Ok(true) => Cow::from(format!("{}s SATISFIABLE{}", GREEN, RESET)), - Err(_) => Cow::from(format!("{}s UNKNOWN{}", RED, RESET)), + Ok(false) => Cow::from(format!("{BLUE}s UNSATISFIABLE{RESET}")), + Ok(true) => Cow::from(format!("{GREEN}s SATISFIABLE{RESET}")), + Err(_) => Cow::from(format!("{RED}s UNKNOWN{RESET}")), } } } @@ -90,7 +90,7 @@ fn main() { std::process::exit(20); } Err(e) => { - panic!("{:?}", e); + panic!("{e:?}"); } Ok(solver) => solver, }; @@ -143,20 +143,17 @@ fn save_result + std::fmt::Display>( println!("{}: {}", colored(Ok(true), s.state.config.no_color), input); if let Err(why) = (|| { buf.write_all( - format!( - "c This file was generated by splr-{} for {}\nc \n", - VERSION, input, - ) - .as_bytes(), + format!("c This file was generated by splr-{VERSION} for {input}\nc \n") + .as_bytes(), )?; report(s, buf)?; buf.write_all(b"s SATISFIABLE\nv ")?; for x in v { - buf.write_all(format!("{} ", x).as_bytes())?; + buf.write_all(format!("{x} ").as_bytes())?; } buf.write(b"0\n") })() { - println!("Abort: failed to save by {}!", why); + println!("Abort: failed to save by {why}!"); } } Ok(Certificate::UNSAT) => { @@ -181,8 +178,7 @@ fn save_result + std::fmt::Display>( if let Err(why) = (|| { buf.write_all( format!( - "c The empty assignment set generated by splr-{} for {}\nc \n", - VERSION, input, + "c The empty assignment set generated by splr-{VERSION} for {input}\nc \n", ) .as_bytes(), )?; @@ -190,7 +186,7 @@ fn save_result + std::fmt::Display>( buf.write_all(b"s UNSATISFIABLE\n")?; buf.write_all(b"0\n") })() { - println!("Abort: failed to save by {}!", why); + println!("Abort: failed to save by {why}!"); } } Err(e) => { @@ -212,17 +208,14 @@ fn save_result + std::fmt::Display>( ); if let Err(why) = (|| { buf.write_all( - format!( - "c An assignment set generated by splr-{} for {}\nc \n", - VERSION, input, - ) - .as_bytes(), + format!("c An assignment set generated by splr-{VERSION} for {input}\nc \n",) + .as_bytes(), )?; report(s, buf)?; buf.write_all(format!("c {}\n{}\n", e, colored(Err(e), true)).as_bytes())?; buf.write(b"0\n") })() { - println!("Abort: failed to save by {}!", why); + println!("Abort: failed to save by {why}!"); } } } @@ -305,13 +298,13 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { ) .as_bytes(), )?; - out.write_all(format!("c Strategy|mode: generic, time:{:9.2},\n", tm).as_bytes())?; + out.write_all(format!("c Strategy|mode: generic, time:{tm:9.2},\n").as_bytes())?; out.write_all("c \n".as_bytes())?; for key in &config::property::F64S { out.write_all( format!( "c config::{:<27}{:>19.3}\n", - format!("{:?}", key), + format!("{key:?}"), s.state.config.derefer(*key), ) .as_bytes(), @@ -321,7 +314,7 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { out.write_all( format!( "c assign::{:<27}{:>15}\n", - format!("{:?}", key), + format!("{key:?}"), s.asg.derefer(*key), ) .as_bytes(), @@ -331,7 +324,7 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { out.write_all( format!( "c assign::{:<27}{:>19.3}\n", - format!("{:?}", key), + format!("{key:?}"), s.asg.refer(*key).get(), ) .as_bytes(), @@ -341,7 +334,7 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { out.write_all( format!( "c clause::{:<27}{:>15}\n", - format!("{:?}", key), + format!("{key:?}"), s.cdb.derefer(*key), ) .as_bytes(), @@ -351,7 +344,7 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { out.write_all( format!( "c clause::{:<27}{:>19.3}\n", - format!("{:?}", key), + format!("{key:?}"), s.cdb.derefer(*key), ) .as_bytes(), @@ -361,7 +354,7 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { out.write_all( format!( "c state::{:<28}{:>15}\n", - format!("{:?}", key), + format!("{key:?}"), s.state.derefer(*key), ) .as_bytes(), @@ -371,7 +364,7 @@ fn report(s: &Solver, out: &mut dyn Write) -> std::io::Result<()> { out.write_all( format!( "c state::{:<28}{:>19.3}\n", - format!("{:?}", key), + format!("{key:?}"), s.state.refer(*key).get(), ) .as_bytes(), diff --git a/src/cdb/activity.rs b/src/cdb/activity.rs index e8c9fd900..277bf3a9d 100644 --- a/src/cdb/activity.rs +++ b/src/cdb/activity.rs @@ -1,7 +1,9 @@ #![cfg(feature = "clause_rewarding")] use {super::ClauseId, crate::types::*, std::num::NonZeroU32}; -// Note: vivifier has its own conflict analyzer, which never call reward functions. +/// clause activity +/// Note: vivifier has its own conflict analyzer, which never call reward functions. + impl ActivityIF for ClauseDB { fn activity(&self, _cid: ClauseId) -> f64 { unreachable!() @@ -20,6 +22,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 7ffa1553d..26c7e96d1 100644 --- a/src/cdb/db.rs +++ b/src/cdb/db.rs @@ -4,7 +4,8 @@ use { ema::ProgressLBD, property, watch_cache::*, - BinaryLinkDB, CertificationStore, Clause, ClauseDB, ClauseDBIF, ClauseId, RefClause, + BinaryLinkDB, CertificationStore, Clause, ClauseDB, ClauseDBIF, ClauseId, ReductionType, + RefClause, }, crate::{assign::AssignIF, types::*}, std::{ @@ -14,6 +15,9 @@ use { }, }; +#[cfg(not(feature = "no_IO"))] +use std::{fs::File, io::Write, path::Path}; + impl Default for ClauseDB { fn default() -> ClauseDB { ClauseDB { @@ -45,6 +49,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), + reduction_threshold: 0.0, eliminated_permanent: Vec::new(), } } @@ -250,7 +255,7 @@ impl ClauseDBIF for ClauseDB { ) -> RefClause { debug_assert!(!vec.is_empty()); debug_assert!(1 < vec.len()); - debug_assert!(vec.iter().all(|l| !vec.contains(&!*l)), "{:?}", vec,); + debug_assert!(vec.iter().all(|l| !vec.contains(&!*l)), "{vec:?}"); if vec.len() == 2 { if let Some(&cid) = self.link_to_cid(vec[0], vec[1]) { self.num_reregistration += 1; @@ -517,7 +522,7 @@ impl ClauseDBIF for ClauseDB { return RefClause::UnitClause(lits[0]); } - (*c).search_from = 2; + c.search_from = 2; let mut new_lits: Vec = lits .iter() .filter(|&l| *l != p) @@ -799,7 +804,10 @@ impl ClauseDBIF for ClauseDB { binary_link.add(l0, l1, cid); std::mem::swap(&mut c.lits, &mut new_lits); self.num_bi_clause += 1; - c.turn_off(FlagClause::LEARNT); + if c.is(FlagClause::LEARNT) { + self.num_learnt -= 1; + c.turn_off(FlagClause::LEARNT); + } if certification_store.is_active() { certification_store.add_clause(&c.lits); @@ -936,37 +944,13 @@ impl ClauseDBIF for ClauseDB { learnt } /// reduce the number of 'learnt' or *removable* clauses. - fn reduce(&mut self, asg: &mut impl AssignIF, portion: usize) { + fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType) { impl Clause { - fn pure_weight(&self, asg: &mut impl AssignIF) -> f64 { - let act_v = self - .iter() - .fold(0.0f64, |acc, l| acc.max(asg.activity(l.vi()))); - - #[cfg(feature = "clause_rewarding")] - let act_c = self.reward; - #[cfg(not(feature = "clause_rewarding"))] - let act_c = 0.25; - - self.rank as f64 / (act_c + act_v) - } - #[cfg(feature = "just_used")] - fn weight(&mut self, asg: &mut impl AssignIF) -> f64 { - let w = c.pure_weight(asg); - if self.is(FlagClause::USED) { - self.turn_off(FlagClause::USED); - 0.8 * w - } else { - w - } - } - #[cfg(not(feature = "just_used"))] - fn weight(&self, asg: &mut impl AssignIF) -> f64 { - self.pure_weight(asg) + fn reverse_activity_sum(&self, asg: &impl AssignIF) -> f64 { + self.iter().map(|l| 1.0 - asg.activity(l.vi())).sum() } - // copied from vivify.rs - fn is_vivify_target(&self) -> bool { - self.rank * 2 <= self.rank_old + fn lbd(&self) -> f64 { + self.rank as f64 } } let ClauseDB { @@ -983,6 +967,7 @@ impl ClauseDBIF for ClauseDB { *num_reduction += 1; let mut perm: Vec> = Vec::with_capacity(clause.len()); + let mut alives = 0; for (i, c) in clause .iter_mut() .enumerate() @@ -1007,24 +992,45 @@ impl ClauseDBIF for ClauseDB { if !c.is(FlagClause::LEARNT) { continue; } - perm.push(OrderedProxy::new(i, c.weight(asg))); - } - // let keep = perm.len().min(nc) / portion; - let keep = perm.len().saturating_sub(portion + 1); - if perm.is_empty() { - return; + alives += 1; + match setting { + ReductionType::RASonADD(_) => { + perm.push(OrderedProxy::new(i, c.reverse_activity_sum(asg))); + } + ReductionType::RASonALL(cutoff, _) => { + let value = c.reverse_activity_sum(asg); + if cutoff < value.min(c.rank_old as f64) { + perm.push(OrderedProxy::new(i, value)); + } + } + ReductionType::LBDonADD(_) => { + perm.push(OrderedProxy::new(i, c.lbd())); + } + ReductionType::LBDonALL(cutoff, _) => { + let value = c.rank.min(c.rank_old); + if cutoff < value { + perm.push(OrderedProxy::new(i, value as f64)); + } + } + } } - 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, - // 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; - 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())); + let keep = match setting { + ReductionType::RASonADD(size) => perm.len().saturating_sub(size), + ReductionType::RASonALL(_, scale) => (perm.len() as f64).powf(1.0 - scale) as usize, + ReductionType::LBDonADD(size) => perm.len().saturating_sub(size), + ReductionType::LBDonALL(_, scale) => (perm.len() as f64).powf(1.0 - scale) as usize, + }; + self.reduction_threshold = match setting { + ReductionType::RASonADD(_) | ReductionType::RASonALL(_, _) => { + keep as f64 / alives as f64 + } + ReductionType::LBDonADD(_) | ReductionType::LBDonALL(_, _) => { + -(keep as f64) / alives as f64 } + }; + perm.sort(); + for i in perm.iter().skip(keep) { + self.remove_clause(ClauseId::from(i.to())); } } fn reset(&mut self) { @@ -1074,6 +1080,7 @@ impl ClauseDBIF for ClauseDB { } None } + #[allow(clippy::unnecessary_cast)] fn minimize_with_bi_clauses(&mut self, asg: &impl AssignIF, vec: &mut Vec) { if vec.len() <= 1 { return; @@ -1188,6 +1195,37 @@ impl ClauseDBIF for ClauseDB { fn is_garbage_collected(&mut self, cid: ClauseId) -> Option { self[cid].is_dead().then(|| self.freelist.contains(&cid)) } + #[cfg(not(feature = "no_IO"))] + /// dump all active clauses and assertions as a CNF file. + fn dump_cnf(&self, asg: &impl AssignIF, fname: &Path) { + let nv = asg.derefer(crate::assign::property::Tusize::NumVar); + for vi in 1..nv { + if asg.var(vi).is(FlagVar::ELIMINATED) && asg.assign(vi).is_some() { + panic!("conflicting var {} {:?}", vi, asg.assign(vi)); + } + } + let Ok(out) = File::create(fname) else { return; }; + let mut buf = std::io::BufWriter::new(out); + let na = asg.derefer(crate::assign::property::Tusize::NumAssertedVar); + let nc = self.iter().skip(1).filter(|c| !c.is_dead()).count(); + buf.write_all(format!("p cnf {} {}\n", nv, nc + na).as_bytes()) + .unwrap(); + for c in self.iter().skip(1) { + if c.is_dead() { + continue; + } + for l in c.iter() { + buf.write_all(format!("{} ", i32::from(*l)).as_bytes()) + .unwrap(); + } + buf.write_all(b"0\n").unwrap(); + } + buf.write_all(b"c from trail\n").unwrap(); + for x in asg.stack_iter().take(asg.len_upto(0)) { + buf.write_all(format!("{} 0\n", i32::from(*x)).as_bytes()) + .unwrap(); + } + } } impl ClauseDB { diff --git a/src/cdb/mod.rs b/src/cdb/mod.rs index 0b8317aac..de9a6da73 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::*}, @@ -35,6 +39,9 @@ use { watch_cache::*, }; +#[cfg(not(feature = "no_IO"))] +use std::path::Path; + /// API for Clause, providing literal accessors. pub trait ClauseIF { /// return true if it contains no literals; a clause after unit propagation. @@ -131,7 +138,7 @@ pub trait ClauseDBIF: /// reduce learnt clauses /// # CAVEAT /// *precondition*: decision level == 0. - fn reduce(&mut self, asg: &mut impl AssignIF, portion: usize); + fn reduce(&mut self, asg: &mut impl AssignIF, setting: ReductionType); /// remove all learnt clauses. fn reset(&mut self); /// update flags. @@ -170,6 +177,9 @@ pub trait ClauseDBIF: fn watch_caches(&self, cid: ClauseId, message: &str) -> (Vec, Vec); #[cfg(feature = "boundary_check")] fn is_garbage_collected(&mut self, cid: ClauseId) -> Option; + #[cfg(not(feature = "no_IO"))] + /// dump all active clauses and assertions as a CNF file. + fn dump_cnf(&self, asg: &impl AssignIF, fname: &Path); } /// Clause identifier, or clause index, starting with one. @@ -279,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, + /// cutoff value used in the last `reduce` + reduction_threshold: f64, // //## incremental solving @@ -287,6 +299,18 @@ pub struct ClauseDB { pub eliminated_permanent: Vec>, } +#[derive(Clone, Debug)] +pub enum ReductionType { + /// weight by Reverse Activity Sum over the added clauses + RASonADD(usize), + /// weight by Reverse Activito Sum over all learnt clauses + RASonALL(f64, f64), + /// weight by Literal Block Distance over the added clauses + LBDonADD(usize), + /// weight by Literal Block Distance over all learnt clauses + LBDonALL(u16, f64), +} + pub mod property { use super::ClauseDB; use crate::types::*; @@ -341,9 +365,14 @@ pub mod property { pub enum Tf64 { LiteralBlockDistance, LiteralBlockEntanglement, + ReductionThreshold, } - pub const F64: [Tf64; 2] = [Tf64::LiteralBlockDistance, Tf64::LiteralBlockEntanglement]; + pub const F64: [Tf64; 3] = [ + Tf64::LiteralBlockDistance, + Tf64::LiteralBlockEntanglement, + Tf64::ReductionThreshold, + ]; impl PropertyDereference for ClauseDB { #[inline] @@ -351,6 +380,7 @@ pub mod property { match k { Tf64::LiteralBlockDistance => self.lbd.get(), Tf64::LiteralBlockEntanglement => self.lb_entanglement.get(), + Tf64::ReductionThreshold => self.reduction_threshold, } } } 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..acd6685ae 100644 --- a/src/cdb/vivify.rs +++ b/src/cdb/vivify.rs @@ -59,8 +59,7 @@ impl VivifyIF for ClauseDB { if to_display <= num_check { state.flush(""); state.flush(format!( - "clause vivifying(assert:{} shorten:{}, check:{}/{})...", - num_assert, num_shrink, num_check, num_target, + "clause vivifying(assert:{num_assert} shorten:{num_shrink}, check:{num_check}/{num_target})..." )); to_display = num_check + display_step; } @@ -163,8 +162,7 @@ impl VivifyIF for ClauseDB { debug_assert!(asg.stack_is_empty() || !asg.remains()); state.flush(""); state.flush(format!( - "vivified(assert:{} shorten:{}), ", - num_assert, num_shrink + "vivification(assert:{num_assert} shorten:{num_shrink}), " )); // state.log( // asg.num_conflict, @@ -311,15 +309,11 @@ impl AssignStack { // make sure the decision var is at the top of list debug_assert!( !learnt.is_empty(), - "empty learnt, conflict: {:?}, assumed: {:?}", - conflicting, - decisions + "empty learnt, conflict: {conflicting:?}, assumed: {decisions:?}" ); debug_assert!( learnt.contains(&!*last_decision), - "\nThe negation of the last decision {} isn't contained in {:?}", - last_decision, - learnt, + "\nThe negation of the last decision {last_decision} isn't contained in {learnt:?}" ); // Since we don't assign the right value of the 'reason' literal after conflict analysis, // we need not to swap locations. @@ -327,10 +321,7 @@ impl AssignStack { // assert!(matches!(self.reason(learnt[0].vi()), AssignReason::None)); debug_assert!( learnt.iter().all(|l| !learnt.contains(&!*l)), - "res: {:?} from: {:?} and trail: {:?}", - learnt, - decisions, - assumes, + "res: {learnt:?} from: {decisions:?} and trail: {assumes:?}" ); learnt } diff --git a/src/config.rs b/src/config.rs index 8c2a12992..ff3a29c64 100644 --- a/src/config.rs +++ b/src/config.rs @@ -52,9 +52,16 @@ pub struct Config { pub use_log: bool, // - //## clause rewarding + //## clause management // + // clause reward dacay rate pub crw_dcy_rat: f64, + // clause reduction LBD threshold for mode 2: exploration + pub cls_rdc_lbd: u16, + // clause reduction ratio for mode 1: exploitation + pub cls_rdc_rm1: f64, + // clause reduction ratio for mode 2: exploration + pub cls_rdc_rm2: f64, // //## eliminator @@ -101,6 +108,9 @@ impl Default for Config { use_log: false, crw_dcy_rat: 0.95, + cls_rdc_lbd: 5, + cls_rdc_rm1: 0.2, + cls_rdc_rm2: 0.05, enable_eliminator: !cfg!(feature = "no_clause_elimination"), elm_cls_lim: 64, @@ -136,8 +146,8 @@ impl Config { let flags = [ "no-color", "quiet", "certify", "journal", "log", "help", "version", ]; - let options_usize = ["cl", "stat", "ecl", "evl", "evo"]; - let options_f64 = ["timeout", "cdr", "vdr", "vds"]; + let options_usize = ["cl", "crl", "stat", "ecl", "evl", "evo"]; + let options_f64 = ["timeout", "cdr", "cr1", "cr2", "vdr", "vds"]; let options_path = ["dir", "proof", "result"]; let seg: Vec<&str> = stripped.split('=').collect(); match seg.len() { @@ -152,23 +162,24 @@ impl Config { "log" => self.use_log = true, "help" => help = true, "version" => version = true, - _ => panic!("invalid flag: {}", name), + _ => panic!("invalid flag: {name}"), } } else if options_usize.contains(&name) { if let Some(str) = iter.next() { if let Ok(val) = str.parse::() { match name { "cl" => self.c_cls_lim = val, + "crl" => self.cls_rdc_lbd = val as u16, "ecl" => self.elm_cls_lim = val, "evl" => self.elm_grw_lim = val, "evo" => self.elm_var_occ = val, - _ => panic!("invalid option: {}", name), + _ => panic!("invalid option: {name}"), } } else { - panic!("invalid value {}", name); + panic!("invalid value {name}"); } } else { - panic!("no argument for {}", name); + panic!("no argument for {name}"); } } else if options_f64.contains(&name) { if let Some(str) = iter.next() { @@ -176,16 +187,18 @@ impl Config { match name { "timeout" => self.c_timeout = val, "cdr" => self.crw_dcy_rat = val, + "cr1" => self.cls_rdc_rm1 = val, + "cr2" => self.cls_rdc_rm2 = val, "vdr" => self.vrw_dcy_rat = val, "vds" => self.vrw_dcy_stp = val, - _ => panic!("invalid option: {}", name), + _ => panic!("invalid option: {name}"), } } else { - panic!("invalid value {}", name); + panic!("invalid value {name}"); } } else { - panic!("no argument for {}", name); + panic!("no argument for {name}"); } } else if options_path.contains(&name) { if let Some(val) = iter.next() { @@ -193,13 +206,13 @@ impl Config { "dir" => self.io_odir = PathBuf::from(val), "proof" => self.io_pfile = PathBuf::from(val), "result" => self.io_rfile = PathBuf::from(val), - _ => panic!("invalid option: {}", name), + _ => panic!("invalid option: {name}"), } } else { - panic!("invalid value {}", name); + panic!("invalid value {name}"); } } else { - panic!("unknown option name {}", name); + panic!("unknown option name {name}"); } } _ => { @@ -218,7 +231,7 @@ impl Config { "l" => self.use_log = true, "h" => help = true, "V" => version = true, - _ => panic!("invalid flag: {}", name), + _ => panic!("invalid flag: {name}"), } } else if options_path.contains(&name) { if let Some(val) = iter.next() { @@ -229,16 +242,16 @@ impl Config { "t" => { self.c_timeout = val.parse::().expect("-t requires a number") } - _ => panic!("invalid option: {}", name), + _ => panic!("invalid option: {name}"), } } else { - panic!("no argument for {}", name); + panic!("no argument for {name}"); } } else { - panic!("unknown option name {}", name); + panic!("unknown option name {name}"); } } else if self.cnf_file.to_string_lossy() != arg { - panic!("invalid argument: {}", arg); + panic!("invalid argument: {arg}"); } } if help { @@ -271,6 +284,8 @@ impl Config { "stage-based re-phasing", #[cfg(feature = "suppress_reason_chain")] "suppress reason chain", + #[cfg(feature = "two_mode_reduction")] + "two-mode reduction", #[cfg(feature = "trail_saving")] "trail saving", #[cfg(feature = "unsafe_access")] @@ -323,31 +338,46 @@ FLAGS: -l, --log Uses Glucose-like progress report -V, --version Prints version information OPTIONS: -{} --cl Soft limit of #clauses (6MC/GB){:>10} - -t, --timeout CPU time limit in sec. {:>10} - --ecl Max #lit for clause subsume {:>10} + --cl Soft limit of #clauses (6MC/GB){:>10} +{}{}{}{} --ecl Max #lit for clause subsume {:>10} --evl Grow limit of #cls in var elim.{:>10} --evo Max #cls for var elimination {:>10} -o, --dir Output directory {:>10} -p, --proof DRAT Cert. filename {:>10} - -r, --result Result filename/stdout {:>10} + -r, --result Result filename/stdout {:>10} + -t, --timeout CPU time limit in sec. {:>10} --vdr Var reward decay rate {:>10.2} {}ARGS: DIMACS CNF file ", + config.c_cls_lim, OPTION!( "clause_rewarding", config.crw_dcy_rat, - " -cdr Clause reward decay rate {:>10.2}\n" + " --cdr Clause reward decay rate {:>10.2}\n" + ), + OPTION!( + "two_mode_reduction", + config.cls_rdc_lbd, + " --crl Clause reduction LBD threshold {:>10}\n" + ), + OPTION!( + "two_mode_reduction", + config.cls_rdc_rm1, + " --cr1 Clause reduction ratio for mode1 {:>10.2}\n" + ), + OPTION!( + "two_mode_reduction", + config.cls_rdc_rm2, + " --cr2 Clause reduction ratio for mode2 {:>10.2}\n" ), - config.c_cls_lim, - config.c_timeout, config.elm_cls_lim, config.elm_grw_lim, config.elm_var_occ, config.io_odir.to_string_lossy(), config.io_pfile.to_string_lossy(), config.io_rfile.to_string_lossy(), + config.c_timeout, config.vrw_dcy_rat, OPTION!( "EVSIDS", diff --git a/src/processor/eliminate.rs b/src/processor/eliminate.rs index 5e2124326..93235f8e3 100644 --- a/src/processor/eliminate.rs +++ b/src/processor/eliminate.rs @@ -51,7 +51,7 @@ pub fn eliminate_var( #[cfg(feature = "trace_elimination")] println!("# eliminate_var {}", vi); // OK, eliminate the literal and build constraints on it. - make_eliminated_clauses(cdb, &mut elim.elim_lits, vi, &*pos, &*neg); + make_eliminated_clauses(cdb, &mut elim.elim_lits, vi, &pos, &neg); let vec = &mut state.new_learnt; // println!("eliminate_var {}: |p|: {} and |n|: {}", vi, (*pos).len(), (*neg).len()); // Produce clauses in cross product: diff --git a/src/processor/simplify.rs b/src/processor/simplify.rs index dde9731b5..180c34f6d 100644 --- a/src/processor/simplify.rs +++ b/src/processor/simplify.rs @@ -339,8 +339,7 @@ impl Eliminator { let v = &mut asg.var_mut(vi); debug_assert!( !checked.contains(&vi), - "eliminator::add_cid_occur356: {:?}", - c, + "eliminator::add_cid_occur356: {c:?}" ); checked.push(vi); let w = &mut self[l.vi()]; diff --git a/src/solver/build.rs b/src/solver/build.rs index 8dbb890ef..664e9e47e 100644 --- a/src/solver/build.rs +++ b/src/solver/build.rs @@ -11,7 +11,7 @@ use { #[cfg(not(feature = "no_IO"))] use std::{ fs::File, - io::{BufRead, BufReader, Write}, + io::{BufRead, BufReader}, path::Path, }; @@ -22,7 +22,7 @@ pub trait SatSolverIF: Instantiate { /// # Errors /// /// * `SolverError::Inconsistent` if it conflicts with existing assignments. - /// * `SolverError::OutOfRange` if it is out of range for var index. + /// * `SolverError::InvalidLiteral` if it is out of range for var index. /// /// # Example /// @@ -40,8 +40,8 @@ pub trait SatSolverIF: Instantiate { /// assert!(s.add_assignment(5).is_ok()); /// assert!(s.add_assignment(8).is_ok()); /// assert!(matches!(s.add_assignment(-1), Err(SolverError::RootLevelConflict(_)))); - /// assert!(matches!(s.add_assignment(10), Err(SolverError::OutOfRange))); - /// assert!(matches!(s.add_assignment(0), Err(SolverError::OutOfRange))); + /// assert!(matches!(s.add_assignment(10), Err(SolverError::InvalidLiteral))); + /// assert!(matches!(s.add_assignment(0), Err(SolverError::InvalidLiteral))); /// assert_eq!(s.solve(), Ok(Certificate::SAT(vec![1, 2, 3, 4, 5, -6, 7, 8]))); /// ``` fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>; @@ -50,7 +50,7 @@ pub trait SatSolverIF: Instantiate { /// # Errors /// /// * `SolverError::Inconsistent` if a given clause is unit and conflicts with existing assignments. - /// * `SolverError::OutOfRange` if a literal in it is out of range for var index. + /// * `SolverError::InvalidLiteral` if a literal in it is out of range for var index. /// /// # Example ///``` @@ -65,8 +65,8 @@ pub trait SatSolverIF: Instantiate { /// assert!(s.add_clause(vec![-4, 5]).is_ok()); /// assert!(s.add_clause(vec![-5, 6]).is_ok()); /// assert!(s.add_clause(vec![-7, 8]).is_ok()); - /// assert!(matches!(s.add_clause(vec![10, 11]), Err(SolverError::OutOfRange))); - /// assert!(matches!(s.add_clause(vec![0, 8]), Err(SolverError::OutOfRange))); + /// assert!(matches!(s.add_clause(vec![10, 11]), Err(SolverError::InvalidLiteral))); + /// assert!(matches!(s.add_clause(vec![0, 8]), Err(SolverError::InvalidLiteral))); /// assert_eq!(s.solve(), Ok(Certificate::UNSAT)); ///``` fn add_clause(&mut self, vec: V) -> Result<&mut Solver, SolverError> @@ -81,7 +81,7 @@ pub trait SatSolverIF: Instantiate { /// /// let mut s = Solver::try_from(Path::new("cnfs/uf8.cnf")).expect("can't load"); /// assert_eq!(s.asg.num_vars, 8); - /// assert!(matches!(s.add_assignment(9), Err(SolverError::OutOfRange))); + /// assert!(matches!(s.add_assignment(9), Err(SolverError::InvalidLiteral))); /// s.add_assignment(1).expect("panic"); /// s.add_assignment(2).expect("panic"); /// s.add_assignment(3).expect("panic"); @@ -100,7 +100,7 @@ pub trait SatSolverIF: Instantiate { /// /// * `SolverError::IOError` if it failed to load a CNF file. /// * `SolverError::Inconsistent` if the CNF is conflicting. - /// * `SolverError::OutOfRange` if any literal used in the CNF is out of range for var index. + /// * `SolverError::InvalidLiteral` if any literal used in the CNF is out of range for var index. fn build(config: &Config) -> Result; /// reinitialize a solver for incremental solving. **Requires 'incremental_solver' feature** fn reset(&mut self); @@ -109,7 +109,7 @@ pub trait SatSolverIF: Instantiate { fn save_certification(&mut self); #[cfg(not(feature = "no_IO"))] /// dump the current status as a CNF - fn dump_cnf(&self, fname: &str); + fn dump_cnf(&self, fname: &Path); } impl Instantiate for Solver { @@ -127,6 +127,20 @@ impl Instantiate for Solver { } } +/// Example +///``` +/// use crate::splr::*; +/// +/// let v: Vec> = vec![]; +/// assert!(matches!( +/// Solver::try_from((Config::default(), v.as_ref())), +/// Ok(_) +/// )); +/// assert!(matches!( +/// Solver::try_from((Config::default(), vec![vec![0_i32]].as_ref())), +/// Err(Err(SolverError::InvalidLiteral)) +/// )); +///``` impl TryFrom<(Config, &[V])> for Solver where V: AsRef<[i32]>, @@ -163,7 +177,7 @@ impl TryFrom<&Path> for Solver { impl SatSolverIF for Solver { fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError> { if val == 0 || self.asg.num_vars < val.unsigned_abs() as usize { - return Err(SolverError::OutOfRange); + return Err(SolverError::InvalidLiteral); } let lit = Lit::from(val); self.cdb.certificate_add_assertion(lit); @@ -182,7 +196,7 @@ impl SatSolverIF for Solver { { for i in vec.as_ref().iter() { if *i == 0 || self.asg.num_vars < i.unsigned_abs() as usize { - return Err(SolverError::OutOfRange); + return Err(SolverError::InvalidLiteral); } } let mut clause = vec @@ -251,37 +265,10 @@ impl SatSolverIF for Solver { self.cdb.certificate_save(); } #[cfg(not(feature = "no_IO"))] - fn dump_cnf(&self, fname: &str) { - let nv = self.asg.derefer(crate::assign::property::Tusize::NumVar); - for vi in 1..nv { - if self.asg.var(vi).is(FlagVar::ELIMINATED) && self.asg.assign(vi).is_some() { - panic!("conflicting var {} {:?}", vi, self.asg.assign(vi)); - } - } - if let Ok(out) = File::create(&fname) { - let mut buf = std::io::BufWriter::new(out); - let na = self - .asg - .derefer(crate::assign::property::Tusize::NumAssertedVar); - let nc = self.cdb.iter().skip(1).filter(|c| !c.is_dead()).count(); - buf.write_all(format!("p cnf {} {}\n", nv, nc + na).as_bytes()) - .unwrap(); - for c in self.cdb.iter().skip(1) { - if c.is_dead() { - continue; - } - for l in c.iter() { - buf.write_all(format!("{} ", i32::from(*l)).as_bytes()) - .unwrap(); - } - buf.write_all(b"0\n").unwrap(); - } - buf.write_all(b"c from trail\n").unwrap(); - for x in self.asg.stack_iter().take(self.asg.len_upto(0)) { - buf.write_all(format!("{} 0\n", i32::from(*x)).as_bytes()) - .unwrap(); - } - } + /// dump all active clauses and assertions as a CNF file. + fn dump_cnf(&self, fname: &Path) { + let Solver { asg, cdb, .. } = self; + cdb.dump_cnf(asg, fname) } } @@ -374,7 +361,7 @@ impl Solver { for ints in v.iter() { for i in ints.as_ref().iter() { if *i == 0 || self.asg.num_vars < i.unsigned_abs() as usize { - return Err(SolverError::OutOfRange); + return Err(SolverError::InvalidLiteral); } } let mut lits = ints @@ -406,7 +393,10 @@ mod tests { fn test_add_var() { let mut s = Solver::try_from(Path::new("cnfs/uf8.cnf")).expect("can't load"); assert_eq!(s.asg.num_vars, 8); - assert!(matches!(s.add_assignment(9), Err(SolverError::OutOfRange))); + assert!(matches!( + s.add_assignment(9), + Err(SolverError::InvalidLiteral) + )); s.add_assignment(1).expect("panic"); s.add_assignment(2).expect("panic"); s.add_assignment(3).expect("panic"); diff --git a/src/solver/conflict.rs b/src/solver/conflict.rs index f7c3cb7c9..4f7fea293 100644 --- a/src/solver/conflict.rs +++ b/src/solver/conflict.rs @@ -240,6 +240,9 @@ pub fn handle_conflict( } state.c_lvl.update(conflicting_level as f64); state.b_lvl.update(assign_level as f64); + state + .e_mode + .update(conflicting_level as f64 - assign_level as f64); state.derive20.clear(); Ok(rank) } @@ -503,7 +506,7 @@ impl Lit { clear: &mut Vec, levels: &[bool], ) -> bool { - if let AssignReason::Decision(_) = asg.reason(self.vi()) { + if matches!(asg.reason(self.vi()), AssignReason::Decision(_)) { return false; } let mut stack = vec![self]; @@ -580,7 +583,7 @@ fn lit_level( cdb: &ClauseDB, lit: Lit, bag: &mut Vec, - mes: &str, + _mes: &str, ) -> DecisionLevel { if bag.contains(&lit) { return 0; @@ -612,12 +615,12 @@ fn lit_level( cdb[cid] .iter() .skip(1) - .map(|l| lit_level(asg, cdb, !*l, bag, mes)) + .map(|l| lit_level(asg, cdb, !*l, bag, _mes)) .max() .unwrap() } - AssignReason::BinaryLink(b) => lit_level(asg, cdb, b, bag, mes), - AssignReason::None => panic!("One of root of {} isn't assigned.", lit), + AssignReason::BinaryLink(b) => lit_level(asg, cdb, b, bag, _mes), + AssignReason::None => panic!("One of root of {lit} isn't assigned."), } } @@ -655,27 +658,26 @@ fn tracer(asg: &AssignStack, cdb: &ClauseDB) { if input.is_empty() { break; } - if let Ok(cid) = input.trim().parse::() { - if cid == 0 { - break; - } - println!( - "{}", - cdb[ClauseId::from(cid)] - .report(asg) - .iter() - .map(|r| format!( - " {}{:?}", - asg.var(Lit::from(r.lit).vi()) - .is(FlagVar::CA_SEEN) - .then(|| "S") - .unwrap_or(" "), - r - )) - .collect::>() - .join("\n"), - ); + let Ok(cid) = input.trim().parse::() else { continue;}; + if cid == 0 { + break; } + println!( + "{}", + cdb[ClauseId::from(cid)] + .report(asg) + .iter() + .map(|r| format!( + " {}{:?}", + asg.var(Lit::from(r.lit).vi()) + .is(FlagVar::CA_SEEN) + .then(|| "S") + .unwrap_or(" "), + r + )) + .collect::>() + .join("\n"), + ); } panic!("done"); } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 5d72d1a01..64f0366b9 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -91,11 +91,37 @@ pub struct Solver { pub state: State, } +/// Example +///``` +/// use crate::splr::*; +/// +/// let v: Vec> = vec![]; +/// assert!(matches!( +/// Certificate::try_from(v), +/// Ok(Certificate::SAT(_)) +/// )); +/// assert!(matches!( +/// Certificate::try_from(vec![vec![0_i32]]), +/// Err(SolverError::InvalidLiteral) +/// )); +/// +/// // `Solver` has another interface. +/// assert!(matches!( +/// Solver::try_from((Config::default(), vec![vec![0_i32]].as_ref())), +/// Err(Err(SolverError::InvalidLiteral)) +/// )); +///``` impl> TryFrom> for Certificate { type Error = SolverError; fn try_from(vec: Vec) -> SolverResult { - let s = Solver::try_from((Config::default(), vec.as_ref())); - s.map_or_else(|e| e, |mut solver| solver.solve()) + Solver::try_from((Config::default(), vec.as_ref())).map_or_else( + |e: SolverResult| match e { + Ok(cert) => Ok(cert), + Err(SolverError::EmptyClause) => Ok(Certificate::UNSAT), + Err(e) => Err(e), + }, + |mut solver| solver.solve(), + ) } } @@ -190,6 +216,12 @@ mod tests { } macro_rules! sat { + ($vec: expr, $should_be: pat) => { + println!("{:>46} =| ", format!("{:?}", $vec)); + let result = Certificate::try_from($vec); + println!("{:?}", result); + assert!(matches!(result, $should_be)); + }; ($vec: expr) => { println!( "{:>46} =| {:?}", @@ -235,12 +267,12 @@ mod tests { // Ok(Certificate::UNSAT) => println!("s UNSATISFIABLE"), // Err(e) => panic!("{}", e), // } - let v0: Vec> = Vec::new(); - sat!(v0); - let v1: Vec> = Vec::new(); - sat!(v1); - sat!(vec![vec![1i32]]); - sat!(vec![vec![1i32], vec![-1]]); + let v0: Vec> = vec![]; + sat!(v0, Ok(Certificate::SAT(_))); + let v1: Vec> = vec![vec![]]; + sat!(v1, Ok(Certificate::UNSAT)); + sat!(vec![vec![1i32]], Ok(Certificate::SAT(_))); + sat!(vec![vec![1i32], vec![-1]], Ok(Certificate::UNSAT)); sat!(vec![vec![1i32, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]); sat!(vec![ vec![1i32, 2], diff --git a/src/solver/search.rs b/src/solver/search.rs index 772e981b8..c07909221 100644 --- a/src/solver/search.rs +++ b/src/solver/search.rs @@ -6,7 +6,7 @@ use { }, crate::{ assign::{self, AssignIF, AssignStack, PropagateIF, VarManipulateIF, VarSelectIF}, - cdb::{self, ClauseDB, ClauseDBIF, VivifyIF}, + cdb::{self, ClauseDB, ClauseDBIF, ReductionType, VivifyIF}, processor::{EliminateIF, Eliminator}, state::{Stat, State, StateIF}, types::*, @@ -237,81 +237,180 @@ fn search( cdb: &mut ClauseDB, state: &mut State, ) -> Result { - let mut current_stage: Option = Some(true); + let mut previous_stage: Option = Some(true); let mut num_learnt = 0; + let mut current_core: usize = 999_999; + let mut core_was_rebuilt: Option = None; + let stage_size: usize = 32; + #[cfg(feature = "rephase")] + let mut sls_core = cdb.derefer(cdb::property::Tusize::NumClause); - state.stm.initialize( - (asg.derefer(assign::property::Tusize::NumUnassertedVar) as f64).sqrt() as usize, - ); + state.stm.initialize(stage_size); while 0 < asg.derefer(assign::property::Tusize::NumUnassignedVar) || asg.remains() { if !asg.remains() { let lit = asg.select_decision_literal(); asg.assign_by_decision(lit); } - if let Err(cc) = asg.propagate(cdb) { - if asg.decision_level() == asg.root_level() { - return Err(SolverError::RootLevelConflict(cc)); + let Err(cc) = asg.propagate(cdb) else { continue; }; + if asg.decision_level() == asg.root_level() { + return Err(SolverError::RootLevelConflict(cc)); + } + asg.update_activity_tick(); + #[cfg(feature = "clause_rewarding")] + cdb.update_activity_tick(); + if 1 < handle_conflict(asg, cdb, state, &cc)? { + num_learnt += 1; + } + if state.stm.stage_ended(num_learnt) { + if let Some(p) = state.elapsed() { + if 1.0 <= p { + return Err(SolverError::TimeOut); + } + } else { + return Err(SolverError::UndescribedError); } - asg.update_activity_tick(); - #[cfg(feature = "clause_rewarding")] - cdb.update_activity_tick(); - if 1 < handle_conflict(asg, cdb, state, &cc)? { - num_learnt += 1; + RESTART!(asg, cdb, state); + asg.select_rephasing_target(); + asg.clear_asserted_literals(cdb)?; + + #[cfg(feature = "trace_equivalency")] + cdb.check_consistency(asg, "before simplify"); + + dump_stage(asg, cdb, state, previous_stage); + let next_stage: Option = state.stm.prepare_new_stage(num_learnt); + let scale = state.stm.current_scale(); + let max_scale = state.stm.max_scale(); + if cfg!(feature = "reward_annealing") { + let base = state.stm.current_stage() - state.stm.cycle_starting_stage(); + let decay_index: f64 = (20 + 2 * base) as f64; + asg.update_activity_decay((decay_index - 1.0) / decay_index); } - if state.stm.stage_ended(num_learnt) { - if let Some(p) = state.elapsed() { - if 1.0 <= p { - return Err(SolverError::TimeOut); + if let Some(new_segment) = next_stage { + // a beginning of a new cycle + { + state.exploration_rate_ema.update(1.0); + if cfg!(feature = "two_mode_reduction") { + cdb.reduce( + asg, + ReductionType::LBDonALL( + state.config.cls_rdc_lbd, + state.config.cls_rdc_rm2, + ), + ); } - } else { - return Err(SolverError::UndescribedError); } - RESTART!(asg, cdb, state); - cdb.reduce(asg, state.stm.num_reducible()); - #[cfg(feature = "trace_equivalency")] - cdb.check_consistency(asg, "before simplify"); - dump_stage(state, asg, current_stage); - let next_stage: Option = state.stm.prepare_new_stage( - (asg.derefer(assign::property::Tusize::NumUnassignedVar) as f64).sqrt() - as usize, - num_learnt, - ); - let scale = state.stm.current_scale(); - let max_scale = state.stm.max_scale(); - if let Some(new_segment) = next_stage { - asg.select_rephasing_target(); - if cfg!(feature = "clause_vivification") { - cdb.vivify(asg, state)?; - } - if new_segment { - 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)?; - asg.eliminated.append(elim.eliminated_lits()); - state[Stat::Simplify] += 1; - state[Stat::SubsumedClause] = elim.num_subsumed; + #[cfg(feature = "rephase")] + { + 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); + asg.reward_by_sls(&$assign); + if $improved(cls) { + asg.override_rephasing_target(&$assign); + } + sls_core = sls_core.min(cls.1); + }; } - if cfg!(feature = "dynamic_restart_threshold") { - state.restart.set_segment_parameters(max_scale); + 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 { + { + let base = state.stm.current_segment(); + let decay_index: f64 = (20 + 2 * base) as f64; + asg.update_activity_decay((decay_index - 1.0) / decay_index); + } + 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); + } + } + } else { + { + if cfg!(feature = "two_mode_reduction") { + cdb.reduce( + asg, + ReductionType::RASonADD( + state.stm.num_reducible(state.config.cls_rdc_rm1), + ), + ); + } } - asg.clear_asserted_literals(cdb)?; - state.progress(asg, cdb); - asg.handle(SolverEvent::Stage(scale)); - state.restart.set_stage_parameters(scale); - current_stage = next_stage; - } else if state.restart.restart( - cdb.refer(cdb::property::TEma::LBD), - cdb.refer(cdb::property::TEma::Entanglement), - ) { - RESTART!(asg, cdb, state); } - if let Some(na) = asg.best_assigned() { - state.flush(""); - state.flush(format!("unreachable core: {}", na)); + { + if !cfg!(feature = "two_mode_reduction") { + cdb.reduce( + asg, + ReductionType::RASonADD(state.stm.num_reducible(state.config.cls_rdc_rm1)), + ); + } + } + state.progress(asg, cdb); + asg.handle(SolverEvent::Stage(scale)); + state.restart.set_stage_parameters(scale); + previous_stage = next_stage; + } else if state.restart.restart( + cdb.refer(cdb::property::TEma::LBD), + cdb.refer(cdb::property::TEma::Entanglement), + ) { + 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.log( @@ -329,25 +428,27 @@ 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: &mut ClauseDB, state: &mut State, shift: Option) { let active = true; // state.rst.enable; let cycle = state.stm.current_cycle(); - let scale = state.stm.current_scale(); + let span = state.stm.current_span(); let stage = state.stm.current_stage(); let segment = state.stm.current_segment(); 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 current_stage { + match shift { None => Some((None, None, stage)), 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!("{span:>7}, fuel:{fuel:>9.2}, cpr:{cpr:>8.2}, vdr:{vdr:>3.2}, cdt:{cdt:>5.2}"), ); } diff --git a/src/solver/stage.rs b/src/solver/stage.rs index 429c5670c..a48e50a7d 100644 --- a/src/solver/stage.rs +++ b/src/solver/stage.rs @@ -11,9 +11,13 @@ pub struct StageManager { segment: usize, unit_size: usize, luby_iter: LubySeries, + max_scale_of_segment: usize, scale: usize, end_of_stage: usize, next_is_new_segment: bool, + cycle_starting_stage: usize, + segment_starting_stage: usize, + segment_starting_cycle: usize, } impl Instantiate for StageManager { @@ -21,9 +25,10 @@ impl Instantiate for StageManager { let unit_size = (cnf.num_of_variables as f64).sqrt() as usize; StageManager { unit_size, + max_scale_of_segment: 1, scale: 1, end_of_stage: unit_size, - next_is_new_segment: true, + next_is_new_segment: false, ..StageManager::default() } } @@ -38,51 +43,65 @@ impl StageManager { segment: 0, unit_size, luby_iter: LubySeries::default(), + max_scale_of_segment: 1, scale: 1, end_of_stage: unit_size, - next_is_new_segment: true, + next_is_new_segment: false, + cycle_starting_stage: 0, + segment_starting_stage: 0, + segment_starting_cycle: 0, } } pub fn initialize(&mut self, unit_size: usize) { self.cycle = 0; self.unit_size = unit_size; self.scale = 1; + self.max_scale_of_segment = 1; self.end_of_stage = unit_size; + self.next_is_new_segment = true; + } + pub fn reset(&mut self) { + self.cycle = 0; + self.scale = 1; + self.max_scale_of_segment = 1; + self.end_of_stage = self.unit_size; + self.next_is_new_segment = true; } /// 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 { - // self.scale *= 2; - // self.stage += 1; - // let span = self.current_span(); - // self.end_of_stage = now + span; - // None - self.unit_size = rescale; + pub fn prepare_new_stage(&mut self, now: usize) -> Option { let mut new_cycle = false; - let old_max = self.luby_iter.max_value(); - let old_scale = self.scale; + let mut new_segment = false; self.scale = self.luby_iter.next_unchecked(); + self.stage += 1; if self.scale == 1 { self.cycle += 1; + self.cycle_starting_stage = self.stage; new_cycle = true; if self.next_is_new_segment { self.segment += 1; + self.max_scale_of_segment *= 2; self.next_is_new_segment = false; + self.segment_starting_stage = self.stage; + self.segment_starting_cycle = self.cycle; + new_segment = true; } - } else if old_max < self.scale { + } + if self.max_scale_of_segment == self.scale { self.next_is_new_segment = true; } - self.stage += 1; let span = self.current_span(); self.end_of_stage = now + span; - new_cycle.then(|| old_scale == self.luby_iter.max_value()) + new_cycle.then_some(new_segment) } pub fn stage_ended(&self, now: usize) -> bool { - self.end_of_stage < now + self.end_of_stage == now } /// returns the number of conflicts in the current stage + /// Note: we need not to make a strong correlation between this value and + /// scale defined by Luby series. So this is fine. pub fn current_span(&self) -> usize { self.cycle * self.unit_size } @@ -102,10 +121,11 @@ impl StageManager { } /// returns a recommending number of redicible learnt clauses, based on /// the length of span. - pub fn num_reducible(&self) -> usize { - const REDUCTION_FACTOR: f64 = 2.0; + pub fn num_reducible(&self, reducing_factor: f64) -> usize { let span = self.current_span(); - let keep = (REDUCTION_FACTOR * (self.unit_size as f64).powf(0.75)) as usize; + // let scale = (self.current_scale() as f64).powf(0.6); + // let keep = scale * self.unit_size as f64; + let keep = (span as f64).powf(1.0 - reducing_factor) as usize; span.saturating_sub(keep) } /// returns the maximum factor so far. @@ -113,6 +133,15 @@ impl StageManager { /// This means it is the value found at the last segment. /// So the current value should be the next value, which is the double. pub fn max_scale(&self) -> usize { - 2 * self.luby_iter.max_value() + self.max_scale_of_segment + } + pub fn cycle_starting_stage(&self) -> usize { + self.cycle_starting_stage + } + pub fn segment_starting_cycle(&self) -> usize { + self.segment_starting_cycle + } + pub fn segment_starting_stage(&self) -> usize { + self.segment_starting_stage } } diff --git a/src/state.rs b/src/state.rs index 3d979c16c..2e130bbab 100644 --- a/src/state.rs +++ b/src/state.rs @@ -27,6 +27,7 @@ pub trait StateIF { fn progress(&mut self, asg: &A, cdb: &C) where A: PropertyDereference + + PropertyDereference + PropertyReference, C: PropertyDereference + PropertyDereference @@ -51,6 +52,8 @@ pub enum Stat { Simplify, /// the number of subsumed clause by processor SubsumedClause, + /// for SLS + SLS, /// don't use this dummy (sentinel at the tail). EndOfStatIndex, } @@ -105,13 +108,19 @@ pub struct State { pub b_lvl: Ema, /// EMA of conflicting levels pub c_lvl: Ema, + /// EMA of c_lbd - b_lbd, or Exploration vs. Eploitation + pub e_mode: Ema2, + pub e_mode_threshold: f64, + pub exploration_rate_ema: Ema, #[cfg(feature = "support_user_assumption")] /// 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 +131,8 @@ pub struct State { pub progress_cnt: usize, /// keep the previous statistics values pub record: ProgressRecord, + /// progress of SLS + pub sls_index: usize, /// start clock for timeout handling pub start: Instant, /// upper limit for timeout handling @@ -143,15 +154,22 @@ impl Default for State { b_lvl: Ema::new(5_000), c_lvl: Ema::new(5_000), + e_mode: Ema2::new(40).with_slow(4_000).with_value(10.0), + e_mode_threshold: 1.20, + exploration_rate_ema: Ema::new(1000), #[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(), @@ -246,6 +264,27 @@ macro_rules! im { } } }; + ($format: expr, $state: expr, $key: expr, $val: expr, $threshold: expr) => { + match ($val, $key) { + (v, LogUsizeId::End) => format!($format, v), + (v, k) => { + let ptr = &mut $state.record[k]; + if $state.config.no_color { + *ptr = v; + format!($format, *ptr) + } else if v < $threshold { + *ptr = v; + format!("\x1B[031m{}\x1B[000m", format!($format, *ptr)) + } else if $threshold < v { + *ptr = v; + format!("\x1B[036m{}\x1B[000m", format!($format, *ptr)) + } else { + *ptr = v; + format!($format, *ptr) + } + } + } + }; } macro_rules! i { @@ -289,6 +328,27 @@ macro_rules! fm { } } }; + ($format: expr, $state: expr, $key: expr, $val: expr, $threshold: expr) => { + match ($val, $key) { + (v, LogF64Id::End) => format!($format, v), + (v, k) => { + let ptr = &mut $state.record[k]; + if $state.config.no_color { + *ptr = v; + format!($format, *ptr) + } else if v < $threshold { + *ptr = v; + format!("\x1B[031m{}\x1B[000m", format!($format, *ptr)) + } else if $threshold < v { + *ptr = v; + format!("\x1B[036m{}\x1B[000m", format!($format, *ptr)) + } else { + *ptr = v; + format!($format, *ptr) + } + } + } + }; } #[allow(unused_macros)] @@ -325,7 +385,7 @@ impl StateIF for State { } if 0 == self.progress_cnt { self.progress_cnt = 1; - println!("{}", self); + println!("{self}"); //## PROGRESS REPORT ROWS for _i in 0..PROGRESS_REPORT_ROWS - 1 { @@ -368,6 +428,7 @@ impl StateIF for State { fn progress(&mut self, asg: &A, cdb: &C) where A: PropertyDereference + + PropertyDereference + PropertyReference, C: PropertyDereference + PropertyDereference @@ -391,7 +452,7 @@ impl StateIF for State { let asg_num_conflict = asg.derefer(assign::property::Tusize::NumConflict); let asg_num_decision = asg.derefer(assign::property::Tusize::NumDecision); let asg_num_propagation = asg.derefer(assign::property::Tusize::NumPropagation); - + // let asg_cwss: f64 = asg.derefer(assign::property::Tf64::CurrentWorkingSetSize); let asg_dpc_ema = asg.refer(assign::property::TEma::DecisionPerConflict); let asg_ppc_ema = asg.refer(assign::property::TEma::PropagationPerConflict); let asg_cpr_ema = asg.refer(assign::property::TEma::ConflictPerRestart); @@ -414,21 +475,21 @@ impl StateIF for State { self.progress_cnt += 1; // print!("\x1B[9A\x1B[1G"); print!("\x1B["); - print!("{}", PROGRESS_REPORT_ROWS); + print!("{PROGRESS_REPORT_ROWS}"); print!("A\x1B[1G"); if self.config.show_journal { while let Some(m) = self.log_messages.pop() { if self.config.no_color { - println!("{}", m); + println!("{m}"); } else { - println!("\x1B[2K\x1B[000m\x1B[034m{}\x1B[000m", m); + println!("\x1B[2K\x1B[000m\x1B[034m{m}\x1B[000m"); } } } else { self.log_messages.clear(); } - println!("\x1B[2K{}", self); + println!("\x1B[2K{self}"); println!( "\x1B[2K #conflict:{}, #decision:{}, #propagate:{}", i!("{:>11}", self, LogUsizeId::NumConflict, asg_num_conflict), @@ -512,18 +573,19 @@ impl StateIF for State { ), ); println!( - "\x1B[2K misc|vivC:{}, subC:{}, core:{}, /ppc:{}", + "\x1B[2K misc|vivC:{}, xplr:{}, core:{}, /ppc:{}", im!( "{:>9}", self, LogUsizeId::VivifiedClause, self[Stat::VivifiedClause] ), - im!( - "{:>9}", + fm!( + "{:>9.4}", self, - LogUsizeId::SubsumedClause, - self[Stat::SubsumedClause] + LogF64Id::ExExTrend, + // self.e_mode.trend(), + self.exploration_rate_ema.get() // , self.e_mode_threshold ), im!( "{:>9}", @@ -621,23 +683,16 @@ impl fmt::Display for State { let mut fname = match &self.target.pathname { CNFIndicator::Void => "(no cnf)".to_string(), CNFIndicator::File(f) => f.to_string(), - CNFIndicator::LitVec(n) => format!("(embedded {} element vector)", n), + CNFIndicator::LitVec(n) => format!("(embedded {n} element vector)"), }; if width <= fname.len() { fname.truncate(58 - vclen); } let fnlen = fname.len(); if width < vclen + fnlen + 1 { - write!(f, "{:9.2}", fname, tm, w = width) + write!(f, "{fname:9.2}") } else { - write!( - f, - "{}{:>w$} |time:{:>9.2}", - fname, - &vc, - tm, - w = width - fnlen, - ) + write!(f, "{fname}{:>w$} |time:{tm:>9.2}", &vc, w = width - fnlen,) } } } @@ -835,6 +890,11 @@ pub enum LogUsizeId { VivifiedVar, Vivify, + // + //## Stochastic Local Search + // + SLS, + // the sentinel End, } @@ -851,11 +911,13 @@ pub enum LogF64Id { TrendLBD, BLevel, CLevel, + ExExTrend, DecisionPerConflict, ConflictPerRestart, PropagationPerConflict, LiteralBlockEntanglement, RestartEnergy, + End, } diff --git a/src/types.rs b/src/types.rs index 8d35c36e8..550268450 100644 --- a/src/types.rs +++ b/src/types.rs @@ -64,13 +64,10 @@ pub trait ActivityIF { #[cfg(debug)] todo!() } + /// update reward decay. + fn update_activity_decay(&mut self, _decay: f64); /// update internal counter. fn update_activity_tick(&mut self); - /// update reward decay. - fn update_activity_decay(&mut self, _index: Option) { - #[cfg(debug)] - todo!() - } } /// API for object instantiation based on `Configuration` and `CNFDescription`. @@ -373,20 +370,27 @@ impl RefClause { pub enum SolverError { // StateUNSAT = 0, // StateSAT, + // A given CNF contains empty clauses or derives them during reading + EmptyClause, + // A clause contains a literal out of the range defined in its header. + // '0' is an example. + InvalidLiteral, + // Exceptions caused by file operations IOError, + // UNSAT with some internal context Inconsistent, OutOfMemory, - OutOfRange, + // UNSAT with some internal context RootLevelConflict(ConflictContext), - EmptyClause, TimeOut, SolverBug, + // For now, this is used for catching errors relating to clock UndescribedError, } impl fmt::Display for SolverError { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{:?}", self) + write!(f, "{self:?}") } } @@ -414,8 +418,8 @@ impl fmt::Display for CNFIndicator { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { CNFIndicator::Void => write!(f, "No CNF specified)"), - CNFIndicator::File(file) => write!(f, "CNF file({})", file), - CNFIndicator::LitVec(n) => write!(f, "A vec({} clauses)", n), + CNFIndicator::File(file) => write!(f, "CNF file({file})"), + CNFIndicator::LitVec(n) => write!(f, "A vec({n} clauses)"), } } } @@ -455,7 +459,7 @@ impl fmt::Display for CNFDescription { num_of_clauses: nc, pathname: path, } = &self; - write!(f, "CNF({}, {}, {})", nv, nc, path) + write!(f, "CNF({nv}, {nc}, {path})") } } @@ -521,7 +525,7 @@ impl TryFrom<&Path> for CNFReader { continue; } Err(e) => { - println!("{}", e); + println!("{e}"); return Err(SolverError::IOError); } } @@ -621,9 +625,9 @@ impl Logger { use std::io::Write; if let Some(f) = &mut self.dest { f.write_all(&mes.into_bytes()) - .unwrap_or_else(|_| panic!("fail to dump {:?}", f)); + .unwrap_or_else(|_| panic!("fail to dump {f:?}")); } else { - println!("{}", mes); + println!("{mes}"); } } }