Splr -- SAT Solver for Propositional Logic in Rust
Features
- Splr is a pure Rustic SAT solver, based on Glucose 4.1.
- It adopts many ideas in modern SAT solvers like:
- Glucose-like dynamic blocking/forcing restarts based on EMAs
- heuristics adaptation
- pre/in-process simplification based on clause subsumption and variable elimination
Install
Just clone me, and cargo install
.
Two executables will be installed:
splr
-- SAT solverdmcr
-- A model checker to verify assignments which are generated bysplr
.
Usage
Splr is a standalone program, taking an CNF file. The result will be saved to a file.
$ splr tests/sample.cnf
sample.cnf 250,1065 |time: 0.35, Mode: Initial
#conflict: 19242, #decision: 22518, #propagate: 866681
Assignment|#rem: 243, #fix: 1, #elm: 6, prg%: 2.8000
Clause Kind|Remv: 11255, LBD2: 61, Binc: 0, Perm: 1056
Restart|#BLK: 276, #RST: 0, eASG: 0.4211, eLBD: 1.0312
Conflicts|aLBD: 9.37, bjmp: 9.21, cnfl: 11.66 |blkR: 1.4000
Clause DB|#rdc: 4, #sce: 2, #exe: 1 |frcK: 0.6100
SATISFIABLE: sample.cnf. The answer was dumped to .ans_sample.cnf.
$ cat .ans_sample.cnf
c An assignment generated by splr-0.1.0 for SATISFIABLE tests/sample.cnf
c
c sample.cnf , v: 250, c: 1065, time: 0.35
c #conflict: 19242, #decision: 22518, #propagate: 866681
c Assignment|#rem: 243, #fix: 1, #elm: 6, prg%: 2.8000
c Clause Kind|Remv: 11255, LBD2: 61, Binc: 0, Perm: 1056
c Restart|#BLK: 276, #RST: 0, eASG: 0.4211, eLBD: 1.0312
c Conflicts|aLBD: 9.37, bjmp: 9.21, cnfl: 11.66 |blkR: 1.4000
c Clause DB|#rdc: 4, #sce: 2, #exe: 1 |frcK: 0.6100
c
1 2 3 4 -5 6 7 -8 -9 10 -11 -12 -13 -14 15 16 -17 18 -19 -20 -21 -22 ... 0
$ dmcr tests/sample.cnf
Valid assignment for tests/sample.cnf found in .ans_sample.cnf.
Correctness
While Splr comes with ABSOLUTELY NO WARRANTY, Splr version 0.1.0 (splr-0.1.0) was verified with the following problems:
- The first 100 satisfiable 3-SAT problems from SATLIB, 250 variables 3-SAT: all the solutions are correct.
- SAT Competition 2017, Main track: with a 2000 sec timeout, splr-0.1.0 solved:
- 72 satisfiable problems: all the solutions are correct.
- 51 unsatisfiable problems: Lingeling or Glucose completely returns the same result.
2019, Shuji Narazaki