## 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`.
## 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
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 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
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
```
#### 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<i32>> = 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
```rust
use splr::*;
use std::env::args;
fn main() {
let cnf = args().nth(1).expect("takes an arg");
let assigns: Vec<i32> = 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::<Vec<i32>>();
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<i32>`'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::<Vec<&i32>>();
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
| `#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] <cnf-file>
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 <c-cls-lim> Soft limit of #clauses (6MC/GB) 0
--crl <cls-rdc-lbd> Clause reduction LBD threshold 5
--cr1 <cls-rdc-rm1> Clause reduction ratio for mode1 0.20
--cr2 <cls-rdc-rm2> Clause reduction ratio for mode2 0.05
--ecl <elm-cls-lim> Max #lit for clause subsume 64
--evl <elm-grw-lim> Grow limit of #cls in var elim. 0
--evo <elm-var-occ> Max #cls for var elimination 20000
-o, --dir <io-outdir> Output directory .
-p, --proof <io-pfile> DRAT Cert. filename proof.drat
-r, --result <io-rfile> Result filename/stdout
-t, --timeout <timeout> CPU time limit in sec. 5000
--vdr <vrw-dcy-rat> Var reward decay rate 0.96
ARGS:
<cnf-file> 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.
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-2022, Narazaki Shuji