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
• heuristics adaptation
• pre/in-process simplification based on clause subsumption and variable elimination
• a variant of Learning Rate Based Branching with Reason Side Rewarding,

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.

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

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

2020, Narazaki Shuji