[−][src]Crate splr
a SAT Solver for Propositional Logic in Rust
Splr is a pure Rustic SAT solver, based on Glucose 4.1. It adopts various research results on SAT solvers:
- CDCL, watch literals, VSIDS and so on from Minisat and the ancestors
- Glucose-like dynamic blocking/forcing restarts based on EMAs
- heuristics adaptation
- pre/in-process simplification based on clause subsumption and variable elimination
Many thanks to SAT researchers.
Usage
Splr is a standalone program, taking a CNF file. The result will be saved to a file.
$ splr tests/sample.cnf
$ splr tests/sample.cnf
sample.cnf 250,1065 |time: 0.38
#conflict: 22372, #decision: 25940, #propagate: 1005304
Assignment|#rem: 235, #fix: 1, #elm: 14, prg%: 6.0000
Clause Kind|Remv: 8414, LBD2: 60, Binc: 0, Perm: 1078
Restart|#BLK: 312, #RST: 0, eASG: 0.4327, eLBD: 0.8989
Conflict|aLBD: 7.92, bjmp: 8.64, cnfl: 10.79 |#stg: 0
Clause DB|#rdc: 5, #sce: 2 |blkR: 1.4000, frcK: 0.7800
Strategy|mode: in the initial search phase to determine a main strategy
SATISFIABLE: tests/sample.cnf. The result was saved to ./.ans_sample.cnf.
$ cat .ans_sample.cnf
c An assignment set generated by splr-0.1.3 for tests/sample.cnf
c
c sample.cnf , #var: 250, #cls: 1065
c #conflict: 22372, #decision: 25940, #propagate: 1005304
c Assignment|#rem: 235, #fix: 1, #elm: 14, prg%: 6.0000
c Clause Kind|Remv: 8414, LBD2: 60, Binc: 0, Perm: 1078
c Restart|#BLK: 312, #RST: 0, eASG: 0.4327, eLBD: 0.8989
c Conflicts|aLBD: 7.92, bjmp: 8.64, cnfl: 10.79 |blkR: 1.4000
c Clause DB|#rdc: 5, #sce: 2, #exe: 0 |frcK: 0.7800
c Strategy|mode: initial, time: 0.38
c
s SATISFIABLE
1 2 3 4 -5 6 7 -8 -9 10 -11 -12 -13 -14 15 16 -17 18 -19 -20 -21 -22 23 ... 0
$ dmcr tests/sample.cnf
Valid assignment set for tests/sample.cnf found in .ans_sample.cnf.
The answer file uses the following format.
- It contains a single line starting with
s
and followed bySATISFIABLE
orUNSATISFIABLE
. - It ends a line of assignments separated by a space and
0
as EOL, if the problem is satisfiable. Otherwise it contains only0
. - Lines starting with
c
are comments, used for dumping statistics
Mnemonics in progress message
mnemonic | meaning |
---|---|
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 |
eASG | a moving rate of the number of assigned variables |
eLBD | a moving rate of earn clause's LBD |
aLBD | the EMA, Exponential Moving Average, of learn clauses' LBDs |
bjmp | the EMA of decision levels at which conflicts occur |
cnfl | the EMA of decision levels to which backjumps go |
blkR | the coefficient for blocking restart, called 'R' in Glucose |
#rdc | the number of reduce invocations |
#sce | the number of satisfied clause eliminations done by simplify |
#exe | the number of exhaustive simplifications, that try both of clause subsumption and variable elimination |
frcK | the coefficient for forcing restart, called 'K' in Glucose |
mode | Selected strategy's id |
frcK | the elapsed CPU time in seconds |
Command line options
Please check help message.
$ splr --help
splr 0.1.3
Shuji Narazaki <shujinarazaki@protonmail.com>
SAT solver for Propositional Logic in Rust, version 0.1.3
USAGE:
splr [FLAGS] [OPTIONS] <cnf_filename>
FLAGS:
-h, --help Prints help information
-c, --certify Writes a DRAT UNSAT certification file
-l, --log Uses Glucose format for progress report
-V, --version Prints version information
-M, --with-learnt-minimization Enables learnt minimization
-R, --without-adaptive_restart Disables dynamic restart adaptation
-S, --without-adaptive_strategy Disables dynamic strategy adaptation
-D, --without-deep-search Disables deep search mode
-E, --without-elim Disables exhaustive simplification
OPTIONS:
--cl <clause_limit> soft limit of #clauses (24M is about 4GB) [default: 0]
--eg <elim_grow_limit> grow limit of #clauses by var elimination [default: 4]
--el <elim_lit_limit> #literals in a clause by var elimination [default: 64]
-o, --dir <output_dirname> output directory [default: .]
-p, --proof <proof_filename> filename for DRAT certification [default: proof.out]
--ra <restart_asg_len> length for assignment average [default: 3500]
--rb <restart_blocking> blocking restart threshold [default: 1.40]
--rl <restart_lbd_len> length for LBD average [default: 50]
--rs <restart_step> #conflicts between restarts [default: 50]
--rt <restart_threshold> forcing restart threshold [default: 0.70]
-r, --result <result_filename> result filename/stdout [default: ]
--to <timeout> CPU time limit in sec. (0 for no limit) [default: 0]
ARGS:
<cnf_filename> a DIMACS format CNF file
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 problems from SATLIB, 250 variables uniform random satisfiable 3-SAT : all the solutions are correct.
- The first 100 problems from SATLIB, 250 variables uniform random unsatisfiable 3-SAT : all the solutions are correct and verified with drat-trim.
- 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. 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 by drat-trim.
Modules
clause | Clause structure |
config | Parameters used for Solver initialization |
eliminator | Pre/In-processor for clause subsumption and variable elimination |
propagator | Assignment management |
restart | Solver restart implementation |
solver | The main structure |
state | Collection of various data and parameters for SAT solving process |
traits | Interfaces between submodules |
types | Plumping layer Basic types |
validator | validates a given assignment for a problem. |
var | Var structure |