[−][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 by SATISFIABLE or UNSATISFIABLE.
It ends a line of assignments separated by a space and 0 as EOL, if the problem is satisfiable. Otherwise it contains only 0.
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