A fast (but please don't compare with Cadical) SAT Solver for Propositional Logic in Rust

Splr is a pure Rustic fast SAT solver, based on Glucose 4.1. It adopts various research results on SAT solvers:

• CDCL, watch literals, LBD and so on from Glucose, 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 aka chronoBT
• Glucose-like heuristics adaptation

Please check ChangeLog about recent updates.

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.24 #conflict: 12273, #decision: 13676, #propagate: 25950 Assignment|#rem: 243, #fix: 1, #elm: 6, prg%: 2.8000 Clause|Remv: 2337, LBD2: 46, Binc: 0, Perm: 1056 Restart|#BLK: 100, #RST: 0, tASG: 1.1967, tLBD: 1.0378 Conflict|eLBD: 11.92, cnfl: 18.87, bjmp: 17.84, rpc%: 0.0000 misc|#rdc: 9, #sce: 2, stag: 0, vdcy: 0.9292 Strategy|mode: Initial search phase before 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