splr 0.3.1 - 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 and so on from Minisat and the ancestors
Glucose-like dynamic blocking/forcing restarts based on EMAs
pre/in-process simplification based on clause subsumption and variable elimination
a variant of Learning Rate Based Branching with Reason Side Rewarding
chronological backtrack
heuristics adaptation

Many thanks to SAT researchers.

Install

Just clone me, and cargo install, with rustc version 1.41 or upper. Two executables will be installed:

splr -- the solver
dmcr -- A model checker to verify an assignment set which was 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.37
 #conflict:      17792, #decision:        20650, #propagate:          38443
  Assignment|#rem:      243, #fix:        1, #elm:        6, prg%:   2.8000
      Clause|Remv:    11307, LBD2:       52, Binc:        0, Perm:     1056
     Restart|#BLK:      213, #RST:        0, tASG:   1.3606, tLBD:   1.0145
    Strategy|mode: in the initial search phase to determine a main strategy
      Result|file: ./.ans_sample.cnf
SATISFIABLE: tests/sample.cnf

$ cat .ans_sample.cnf
c An assignment set generated by splr-0.3.0 for tests/sample.cnf
c
c sample.cnf                                 , #var:      250, #cls:     1065
c  #conflict:      17792, #decision:        20650, #propagate:          38443
c   Assignment|#rem:      243, #fix:        1, #elm:        6, prg%:   2.8000
c       Clause|Remv:    11307, LBD2:       52, Binc:        0, Perm:     1056
c      Restart|#BLK:      213, #RST:        0, eASG:   1.3606, eLBD:   1.0145
c     Conflict|eLBD:    11.00, cnfl:    15.80, bjmp:    14.65, rpc%:   0.0000
c         misc|#rdc:        3, #sce:        2, stag:        0, vdcy:      0.0
c     Strategy|mode:        initial, time:     0.36
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
A valid assignment set for tests/sample.cnf is found in .ans_sample.cnf.

Correctness

Though Splr comes with ABSOLUTELY NO WARRANTY, I'd like to show some results.

Version 0.3.1

Splr version 0.3.1 (splr-0.3.1) was checked with the following problems:

SAT Race 2019, Benchmarks, splr-0.3.1 solved with a 200 sec timeout:
- 35 satisfiable problems: all the solutions were correct.
- 4 unsatisfiable problems:
  - 3 were verified with grad.
  - Verifying gto_p60c238-sc2018.cnf was timed out due to the size of the drat file (1.3 GB).

Version 0.1.0

Splr version 0.1.0 (splr-0.1.0) was checked with the following problems:

The first 100 problems from SATLIB, 250 variables uniform random satisfiable 3-SAT : all the solutions were correct.
The first 100 problems from SATLIB, 250 variables uniform random unsatisfiable 3-SAT : all the solutions were 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 were 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/.

2020, Narazaki Shuji