A modern SAT Solver for Propositional Logic in Rust
----
Splr is a pure [Rust](https://www.rust-lang.org)ic modern SAT solver, based on [Glucose 4.1](https://www.labri.fr/perso/lsimon/glucose/).
It adopts various research results on SAT solvers:
- *CDCL*, *watch literals*, *LBD* and so on from Glucose, [Minisat](http://minisat.se) and the ancestors
- Glucose-like *dynamic blocking/forcing restarts* based on [EMAs](https://arxiv.org/abs/1506.08905) and [CaDiCaL](https://github.com/arminbiere/cadical)-like *stabilization*
- pre/in-process simplification based on clause subsumption and variable elimination
- compile-time selection of a variant of *Learning Rate Based Branching* with *Reason Side Rewarding* and EVSIDS
- *chronological backtrack* aka *chronoBT*
- Glucose-like heuristics adaptation
- CaDiCaL-like extended phase 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.4.0
* [SAT Race 2019](http://sat-race-2019.ciirc.cvut.cz), [Benchmarks](http://satcompetition.org/sr2019benchmarks.zip), splr-0.4.0(e0461bd) solved with a 300 sec (soft) timeout:
* 43 satisfiable problems: all the solutions were correct.
* 4 unsatisfiable problems: all were verified with [Grad](https://www21.in.tum.de/~lammich/grat/).
#### Version 0.3.1
* [SAT Race 2019](http://sat-race-2019.ciirc.cvut.cz), [Benchmarks](http://satcompetition.org/sr2019benchmarks.zip), splr-0.3.1 solved with a 200 sec (soft) timeout:
* 35 satisfiable problems: all the solutions were correct.
* 4 unsatisfiable problems:
* 3 were verified with Grad.
* Verifying gto_p60c238-sc2018.cnf was timed out due to the size of the drat file (1.3 GB).
#### Version 0.1.0
* The first 100 problems from
[SATLIB](https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html),
[250 variables uniform random satisfiable 3-SAT](https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/uf250-1065.tar.gz)
: all the solutions were correct.
* The first 100 problems from
[SATLIB](https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html),
[250 variables uniform random unsatisfiable 3-SAT](https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/uuf250-1065.tar.gz)
: all the solutions were correct and verified with [drat-trim](http://www.cs.utexas.edu/~marijn/drat-trim/).
* [SAT Competition 2017](https://baldur.iti.kit.edu/sat-competition-2017/index.php?cat=tracks),
[Main track](https://baldur.iti.kit.edu/sat-competition-2017/benchmarks/Main.zip)
: with a 2000 sec timeout, splr-0.1.0 solved:
* 72 satisfiable problems: all the solutions were correct.
* 51 unsatisfiable problems: [Lingeling](http://fmv.jku.at/lingeling/) or Glucose completely returns the same result. And,
* 37 certificates generated by splr-0.1.1 were verified with drat-trim.
* The remaining 14 certificates weren't able to be verified due to [timeout](https://gitlab.com/satisfiability01/splr/issues/74#note_142021555) by 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 model checker to verify an assignment set which was generated by `splr`.
## Usage
Splr is a standalone program, taking a CNF file. The result will be saved to a file.
```plain
$ splr tests/sample.cnf
Assignment|#rem: 243, #fix: 1, #elm: 6, prg%: 2.8000
Clause|Remv: 19886, LBD2: 114, Binc: 0, Perm: 1056
misc|#rdc: 7, #smp: 1, 2smp: 36681, vdcy: 0.9800
Strategy|mode: Initial search phase before a main strategy
Result|file: ./.ans_sample.cnf
s SATISFIABLE: tests/sample.cnf
$ cat .ans_sample.cnf
c An assignment set generated by splr-0.4.0 for tests/sample.cnf
c
c CNF file(sample.cnf), #var: 250, #cls: 1065
c #conflict: 38892, #decision: 47095, #propagate: 85990
c Restart|#BLK: 257, #RST: 512, eASG: 1.3309, eLBD: 0.9605
c Conflict|eLBD: 9.27, cnfl: 12.84, bjmp: 11.83, rpc%: 1.3190
c misc|#rdc: 7, #smp: 1, 2smp: 36681, vdcy: 0.9800
c Strategy|mode: Initial, time: 1.27
c
s SATISFIABLE
v 1 2 3 4 -5 6 7 -8 -9 10 11 -12 -13 -14 15 16 -17 18 ... 0
$ dmcr tests/sample.cnf
A valid assignment set for tests/sample.cnf is found in .ans_sample.cnf.
```
Since 0.4.0, you can use Splr in your programs.
```rust
use splr::*;
use std::convert::TryFrom;
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(Cetrificate::UNSAT) => println!("s UNSATISFIABLE"),
Err(e) => panic!("s UNKNOWN; {}", e),
}
}
```
### Mnemonics used in the progress message
| `v` | the number of variables used in the given CNF file |
| `c` | 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 solved 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 number of learnt clauses which are not biclauses |
| `LBD2` | the number of learnt clauses which LBDs are 2 |
| `Binc` | the number of binary learnt clauses |
| `Perm` | the number of given clauses and binary learnt clauses |
| `#BLK` | the number of blocking restart |
| `#RST` | the number of restart |
| `tASG` | the trend rate of the number of assigned variables |
| `tLBD` | the trend rate of learn clause's LBD |
| `eLBD` | the EMA, Exponential Moving Average, of learn clauses' LBDs |
| `cnfl` | the EMA of decision levels to which backjumps go |
| `bjmp` | the EMA of decision levels at which conflicts occur |
| `rpc%` | a percentage of restart per conflict |
| `#rdc` | the number of `clause reduction` invocations |
| `#smp` | the number of `clause and var simplification` invocations |
| `2smp` | the number of literals to invoke the simplifier again |
| `vdcy` | var activity decay rate |
| `mode` | Selected strategy's id |
| `time` | the elapsed CPU time in seconds |
## Command line options
Please check help message.
* The 'switch' in help message below is either '1' or '0' to or not to use a module.
* Splr can't handle compressed CNF files so far.
```plain
$ splr --help
splr 0.4.0
Narazaki Shuji <shujinarazaki@protonmail.com>
A modern CDCL SAT solver in Rust
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
-l, --log Uses Glucose-like progress report
-V, --version Prints version information
OPTIONS:
--ADP <adaptive> Strategy adaptation switch [default: 1]
--cbt <cbt-thr> Level threshold to use chronoBT [default: 100]
--cl <clause-limit> Soft limit of #clauses (6MC/GB) [default: 0]
--stat <dump-int> Interval for dumping stat data [default: 0]
--PRO <elim> Pre/in-processor switch [default: 1]
--ecl <elim-cls-lim> Max #lit for clause subsume [default: 100]
--evl <elim-grw-lim> Grow limit of #cls in var elim [default: 0]
--et <elim-trigger> #cls to start simplification [default: 40000]
--evo <elim-var-occ> Max #cls for var elimination [default: 10000]
-o, --dir <output-dir> Output directory [default: .]
-p, --proof <proof-file> Cert. file in DRAT format [default: proof.out]
--RDC <reduce> Clause reduction switch [default: 1]
--RPH <rephase> Rephase switch [default: 1]
-r, --result <result-file> Result filename/stdout [default: ]
--RSR <rsr> Reason-Side Rewarding switch [default: 1]
--ral <rst-asg-len> Length for assignment average [default: 3500]
--rab <rst-asg-thr> Blocking restart threshold [default: 1.40]
--rll <rst-lbd-len> Length of LBD fast EMA [default: 50]
--rls <rst-lbd-slw> Length of LBD slow EMA [default: 10000]
--rlt <rst-lbd-thr> Forcing restart threshold [default: 0.70]
--rss <rst-stb-scl> Stabilizer scaling [default: 2.0]
--rs <rst-step> #conflicts between restarts [default: 50]
--STB <stabilize> Stabilization switch [default: 1]
-t, --timeout <timeout> CPU time limit in sec [default: 5000.0]
--vri <vrw-dcy-beg> Initial var reward decay [default: 0.75]
--vrm <vrw-dcy-end> Maximum var reward decay [default: 0.98]
ARGS:
<cnf-file> CNF file in DIMACS format
```
## 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, Narazaki Shuji