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.

```plain $ 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. ```

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