[−][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
sample.cnf                                         250,1065 |time:     0.31
 #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.6250
    Strategy|mode: in the initial search phase to determine a main strategy
SATISFIABLE: sample.cnf. The answer was dumped to .ans_sample.cnf.

$ cat .ans_sample.cnf
c An assignment set generated by splr-0.1.2 for tests/sample.cnf
c
c sample.cnf                                 , #var:      250, #cls:     1065
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.6250
c     Strategy|mode:        initial, time:     0.31
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
`#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
`blkR`	the coefficient for blocking restart, called 'R' in Glucose
`frcK`	the coefficient for forcing restart, called 'K' in Glucose

Command line options

Please check help message.

$ splr --help
Shuji Narazaki <shujinarazaki@protonmail.com>
SAT solver for Propositional Logic in Rust, version 0.1.2

USAGE:
    splr [FLAGS] [OPTIONS] <cnf_file>

FLAGS:
    -h, --help                    Prints help information
    -R, --no-adaptive_restart     Disables dynamic restart adaptation
    -S, --no-adaptive_strategy    Disables dynamic strategy adaptation
    -E, --no-elim                 Disables exhaustive simplification
    -T, --no-stagnation           Disables stagnation model
    -c, --certify                 Writes a DRAT UNSAT certification file
    -l, --log                     Uses Glucose format for progress report
    -V, --version                 Prints version information

OPTIONS:
        --cl <clause_limit>           soft limit of #clauses (24000000 is about 4GB) [default: 0]
        --eg <elim_grow_limit>        grow limit of #clauses by var elimination [default: 0]
        --el <elim_lit_limit>         #literals in a merged clause by var elimination [default: 64]
    -o, --output <output_filename>    output filename; use default rule if it's empty. [default: ]
    -p, --proof <proof_filename>      filename of DRAT UNSAT certification [default: proof.out]
        --ra <restart_asg_samples>    #samples for average assignment rate [default: 3500]
        --rb <restart_blocking>       threshold for blocking restart (R in Glucose) [default: 1.40]
        --rl <restart_lbd_samples>    #samples for average LBD of learnt clauses [default: 50]
        --rs <restart_step>           #conflicts between restarts [default: 50]
        --rt <restart_threshold>      threshold for forcing restart (K in Glucose) [default: 0.60]
        --to <timeout>                time limit in sec by WALL-CLOCK TIME. (zero for no limit). [default: 0]

ARGS:
    <cnf_file>    a CNF file to solve

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