## A modern SAT Solver for Propositional Logic in Rust Splr is a modern SAT solver in [Rust](https://www.rust-lang.org), based on [Glucose 4.1](https://www.labri.fr/perso/lsimon/glucose/). It adopts, or adopted, various research results on modern SAT solvers: - _CDCL_, _watch literals_, _LBD_ and so on from Glucose, [Minisat](http://minisat.se) and the ancestors - Luby series based restart control - Glucose-like _dynamic blocking/forcing restarts_ - pre/in-processor to simplify the given CNF - branching variable selection based on _Learning Rate Based Branching_ with _Reason Side Rewarding_ or EVSIDS - [CaDiCaL](https://github.com/arminbiere/cadical)-like extended phase saving - _restart stabilization_ inspired by CadiCaL - _clause vivification_ - _trail saving_ *Many thanks to SAT researchers.* Please check [ChangeLog](ChangeLog.md) about recent updates. ## Correctness Though Splr comes with **ABSOLUTELY NO WARRANTY**, I'd like to show some results. #### Version 0.17.0 - [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 Just run `cargo install splr` after installing the latest [cargo](https://www.rust-lang.org/tools/install). Two executables will be installed: - `splr` -- the solver - `dmcr` -- a very simple model checker to verify a *satisfiable* assignment set generated by `splr`. Alternatively, Nix users can use `nix build`. ### About `no_std` environment and feature `no_IO` If you want to build a library for `no_std` environment, or if you want to compile with feature `no_IO`, you have to run `cargo build --lib --features no_IO`. They are incompatible with `cargo install`. - [2024-02-03] Feature `platform_wasm` was added. ## Usage Splr is a standalone program, taking a CNF file. The result will be saved to a file, which format is defined by [SAT competition 2011 rules](http://www.satcompetition.org/2011/rules.pdf). ```plain $ splr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf unif-k3-r4.25-v360-c1530-S1293537826-039.cnf 360,1530 |time: 732.01 #conflict: 9663289, #decision: 23326959, #propagate: 546184944 Assignment|#rem: 351, #fix: 0, #elm: 9, prg%: 2.5000 Clause|Remv: 69224, LBD2: 2857, BinC: 1, Perm: 1522 Conflict|entg: 7.0499, cLvl: 12.2451, bLvl: 11.1030, /cpr: 30.74 Learning|avrg: 10.4375, trnd: 1.0069, #RST: 566140, /dpc: 1.18 misc|vivC: 7370, subC: 0, core: 122, /ppc: 61.53 Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf s SATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf ``` ```plain $ cat ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf c This file was generated by splr-0.15.0 for cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf c c unif-k3-r4.25-v360-c1530-S1293537826-039.cnf, #var: 360, #cls: 1530 c #conflict: 9663289, #decision: 23326959, #propagate: 546184944, c Assignment|#rem: 351, #fix: 0, #elm: 9, prg%: 2.5000, c Clause|Remv: 69224, LBD2: 2857, BinC: 1, Perm: 1522, c Conflict|entg: 7.0499, cLvl: 12.2451, bLvl: 11.1030, /cpr: 30.74, c Learing|avrg: 10.4375, trnd: 1.0069, #RST: 566140, /dpc: 1.18, c misc|vivC: 7370, subC: 0, core: 122, /ppc: 61.53, c Strategy|mode: generic, time: 732.03, c c config::VarRewardDecayRate 0.960 c assign::NumConflict 9663289 c assign::NumDecision 23326959 c assign::NumPropagation 546184944 c assign::NumRephase 734 c assign::NumRestart 566141 c assign::NumVar 360 c assign::NumAssertedVar 0 c assign::NumEliminatedVar 9 c assign::NumReconflict 653 c assign::NumRepropagation 12460396 c assign::NumUnassertedVar 351 c assign::NumUnassignedVar 351 c assign::NumUnreachableVar 0 c assign::RootLevel 0 c assign::AssignRate 0.000 c assign::DecisionPerConflict 1.179 c assign::PropagationPerConflict 61.527 c assign::ConflictPerRestart 122.388 c assign::ConflictPerBaseRestart 122.388 c assign::BestPhaseDivergenceRate 0.000 c clause::NumBiClause 1 c clause::NumBiClauseCompletion 0 c clause::NumBiLearnt 1 c clause::NumClause 70746 c clause::NumLBD2 2857 c clause::NumLearnt 69224 c clause::NumReduction 1461 c clause::NumReRegistration 0 c clause::Timestamp 0 c clause::LiteralBlockDistance 10.438 c clause::LiteralBlockEntanglement 7.050 c state::Vivification 735 c state::VivifiedClause 7370 c state::VivifiedVar 0 c state::NumCycle 734 c state::NumStage 1461 c state::IntervalScale 1 c state::IntervalScaleMax 1024 c state::BackjumpLevel 11.103 c state::ConflictLevel 12.245 c s SATISFIABLE v 1 -2 3 4 5 6 -7 -8 9 -10 -11 -12 13 -14 ... -360 0 ``` ```plain $ dmcr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf A valid assignment set for cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf is found in ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf ``` If you want to certificate unsatisfiability, use `--certify` or `-c` and use proof checker like [Grid](https://www21.in.tum.de/~lammich/grat/). Firstly run splr with the certificate option `-c`. ```plain $ splr -c cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf unif-k3-r4.25-v360-c1530-S1028159446-096.cnf 360,1530 |time: 204.09 #conflict: 4018458, #decision: 9511129, #propagate: 221662222 Assignment|#rem: 345, #fix: 7, #elm: 8, prg%: 4.1667 Clause|Remv: 11290, LBD2: 2018, BinC: 137, Perm: 1517 Conflict|entg: 4.5352, cLvl: 8.0716, bLvl: 6.9145, /cpr: 112.08 Learning|avrg: 1.5625, trnd: 0.2219, #RST: 237295, /dpc: 1.07 misc|vivC: 4085, subC: 0, core: 345, /ppc: 52.55 Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1028159446-096.cnf Certificate|file: proof.drat s UNSATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf ``` #### 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 c parsing input formula with 360 variables and 1530 clauses c finished parsing c detected empty clause; start verification via backward checking c 1530 of 1530 clauses in core c 2036187 of 4029964 lemmas in core using 68451907 resolution steps c 0 RAT lemmas in core; 908116 redundant literals in core lemmas s VERIFIED c verification time: 105.841 seconds ``` #### B: Verify with gratchk Firstly you have to convert the generated DRAT file to a GRAT file. ```plain $ gratgen cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat -o proof.grat c sizeof(cdb_t) = 4 c sizeof(cdb_t*) = 8 c Using RAT run heuristics c Parsing formula ... 1ms c Parsing proof (ASCII format) ... 32251ms c Forward pass ... 2073ms c Starting Backward pass c Single threaded mode 0% 10 20 30 40 50 60 70 80 90 100% |----|----|----|----|----|----|----|----|----|----| *************************************************** c Waiting for aux-threads ...done c Lemmas processed by threads: 2032698 mdev: 0 c Finished Backward pass: 65356ms c Writing combined proof ... 19088ms s VERIFIED c Timing statistics (ms) c Parsing: 32253 c Checking: 67465 c * bwd: 65356 c Writing: 19088 c Overall: 118808 c * vrf: 99720 c Lemma statistics c RUP lemmas: 2032698 c RAT lemmas: 0 c RAT run heuristics: 0 c Total lemmas: 2032698 c Size statistics (bytes) c Number of clauses: 4031493 c Clause DB size: 309680252 c Item list: 128778112 c Pivots store: 16777216 ``` Then verify it with `gratchk`. ```plain $ gratchk unsat cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.grat c Reading cnf c Reading proof c Done c Verifying unsat s VERIFIED UNSAT ``` ### Calling Splr from Rust programs Since 0.4.0, you can use Splr in your programs. (Here I suppose that you uses Rust 2021.) ```rust use splr::*; fn main() { let v: Vec> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]; match Certificate::try_from(v) { Ok(Certificate::SAT(ans)) => println!("s SATISFIABLE: {:?}", ans), Ok(Certificate::UNSAT) => println!("s UNSATISFIABLE"), Err(e) => panic!("s UNKNOWN; {}", e), } } ``` ### All solutions SAT solver as an application of 'incremental_solver' feature The following example requires 'incremental_solver' feature. You need the following dependeny: ```toml splr = { version = "^0.17", features = ["incremental_solver"] } ``` Under this configuration, module `splr` provides some more functions: - `splr::Solver::reset(&mut self)` - `splr::Solver::add_var(&mut self)` // increments the last variable number - `splr::Solver::add_clause(&mut self, vec: AsRef<[i32]>) -> Result<&mut Solver, SolverError>` You have to call `reset` before calling `add_var`, `add_clause`, and `solve` again. By this, splr forgets everything about the previous formula, especially non-equivalent transformations by pre/inter-processors like clause subsumbtion. So technically splr is not an incremental solver. 'add_clause' will emit an error if `vec` is invalid. ```rust use splr::*; use std::env::args; fn main() { let cnf = args().nth(1).expect("takes an arg"); let assigns: Vec = Vec::new(); println!("#solutions: {}", run(&cnf, &assigns)); } #[cfg(feature = "incremental_solver")] fn run(cnf: &str, assigns: &[i32]) -> usize { let mut solver = Solver::try_from(cnf).expect("panic at loading a CNF"); for n in assigns.iter() { solver.add_assignment(*n).expect("panic at assertion"); } let mut count = 0; loop { match solver.solve() { Ok(Certificate::SAT(ans)) => { count += 1; println!("s SATISFIABLE({}): {:?}", count, ans); let ans = ans.iter().map(|i| -i).collect::>(); match solver.add_clause(ans) { Err(SolverError::Inconsistent) => { println!("c no answer due to level zero conflict"); break; } Err(e) => { println!("s UNKNOWN; {:?}", e); break; } Ok(_) => solver.reset(), } } Ok(Certificate::UNSAT) => { println!("s UNSATISFIABLE"); break; } Err(e) => { println!("s UNKNOWN; {}", e); break; } } } count } ``` Since 0.4.1, `Solver` has `iter()`. So you can iterate on satisfiable '`solution: Vec`'s as: ```rust #[cfg(feature = "incremental_solver")] for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() { println!("{}-th answer: {:?}", i, v); } ``` #### 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 | | ------------ | ----------------------------------------------------------------------------------------- | | `#var` | the number of variables used in the given CNF file | | `#cls` | the number of clauses used in the given CNF file | | `time` | elapsed CPU time in seconds (or wall-clock time if CPU time is not available) | | `#conflict` | the number of conflicts | | `#decision` | the number of decisions | | `#propagate` | the number of propagates (its unit is literal) | | `#rem` | the number of remaining variables | | `#fix` | the number of asserted variables (which has been assigned a value at decision level zero) | | `#elm` | the number of eliminated variables | | `prg%` | the percentage of `remaining variables / total variables` | | `Remv` | the current number of learnt clauses that are not bi-clauses | | `LBD2` | the accumulated number of learnt clauses which LBDs are 2 | | `BinC` | the current number of binary learnt clauses | | `Perm` | the current number of given clauses and binary learnt clauses | | `entg` | the current average of 'Literal Block entanglement' | | `cLvl` | the EMA of decision levels at which conflicts occur | | `bLvl` | the EMA of decision levels to which backjumps go | | `/cpr` | the EMA of conflicts per restart | | `avrg` | the EMA, Exponential Moving Average, of LBD of learnt clauses | | `trnd` | the current trend of the LBD's EMA | | `#RST` | the number of restarts | | `/dpc` | the EMA of decisions per conflict | | `vivC` | the number of the vivified clauses | | `subC` | the number of the clauses subsumed by clause elimination processor | | `core` | the number of unreachable vars | | `/ppc` | the EMA of propagations per conflict | | `time` | the elapsed CPU time in seconds | ## Command line options ```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, two-mode reduction, trail saving, unsafe access USAGE: splr [FLAGS] [OPTIONS] FLAGS: -h, --help Prints help information -C, --no-color Disable coloring -q, --quiet Disable any progress message -c, --certify Writes a DRAT UNSAT certification file -j, --journal Shows log about restart stages -l, --log Uses Glucose-like progress report -V, --version Prints version information OPTIONS: --cl Soft limit of #clauses (6MC/GB) 0 --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 ``` ## Solver description 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] - ~~chronological backtrack[5]~~ disabled since 0.12 due to incorrect UNSAT certificates. - clause vivification[6] - Luby series based on the number of conflicts defines 'stages/cycles/segments', which are used as trigger of - restart - clause reduction - in-processor (clause elimination, subsumption and vivification) - 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 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.17](https://user-images.githubusercontent.com/997855/215309646-1bfe3ea5-dcc3-42ee-9d76-99e1b07610c4.png) 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 #### Bibliography - [1] G. Audemard and L. Simon, "Predicting learnt clauses quality in modern SAT solvers," in _International Joint Conference on Artificial Intelligence 2009_, pp. 399–404, 2009. - [2] G. Audemard and L. Simon, "Refining restarts strategies for SAT and UNSAT," in _LNCS_, vol.7513, pp.118–126, 2012. - [3] R. Hickey and F. Bacchus, "Trail Saving on Backtrack", _SAT 2020_, _LNCS_, vol. 12178, pp.46-61, 2020. - [4] J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, "Learning Rate Based Branching Heuristic for SAT Solvers," in _LNCS_, vol.9710, pp.123–140, 2016. - [5] A. Nadel and V. Ryvchin, "Chronological Backtracking," in _Theory and Applications of Satisfiability Testing - SAT 2018_, June 2018, pp.111–121, 2018. - [6] C. Piette, Y. Hamadi, and L. Saïs, "Vivifying propositional clausal formulae," _Front. Artif. Intell. Appl._, vol.178, pp.525–529, 2008. ## License This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed with this file, You can obtain one at http://mozilla.org/MPL/2.0/. --- 2020-2024, Narazaki Shuji