splr 0.1.4 - Docs.rs

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, EVSIDS 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.

Install

Just clone me, and cargo install.

Two executables will be installed:

splr -- SAT solver
dmcr -- A model checker to verify an assignment set which are generated by splr.

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.68
 #conflict:      33526, #decision:        38700, #propagate:        1521424
  Assignment|#rem:      235, #fix:        1, #elm:       14, prg%:   6.0000
 Clause Kind|Remv:    11807, LBD2:       75, Binc:        1, Perm:     1079
     Restart|#BLK:      403, #RST:        0, eASG:   1.4764, eLBD:   1.0034
    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.4 for tests/sample.cnf
c
c sample.cnf                                 , #var:      250, #cls:     1065
c  #conflict:      33526, #decision:        38700, #propagate:        1521424
c   Assignment|#rem:      235, #fix:        1, #elm:       14, prg%:   6.0000
c  Clause Kind|Remv:    11807, LBD2:       75, Binc:        1, Perm:     1079
c      Restart|#BLK:      403, #RST:        0, eASG:   1.4764, eLBD:   1.0034
c    Conflicts|aLBD:     8.20, bjmp:      NaN, cnfl:      NaN |blkR:   1.4000
c    Clause DB|#rdc:        5, #sce:        2, #exe:        0 |frcK:   0.8200
c     Strategy|mode:        initial, time:     0.66
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.

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.

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/.

2019, Shuji Narazaki