#SAT #logic #satisfiability #SAT-solver

bin+lib splr

A pure rustic CDCL SAT solver based on Glucose

10 releases

✓ Uses Rust 2018 edition

new 0.3.1 Feb 22, 2020
0.2.1 Dec 16, 2019
0.2.0 Nov 28, 2019
0.1.3 May 8, 2019
0.1.2 Mar 7, 2019

#17 in Science

Download history 9/week @ 2019-11-12 13/week @ 2019-11-19 36/week @ 2019-11-26 9/week @ 2019-12-03 84/week @ 2019-12-10 12/week @ 2019-12-17 8/week @ 2019-12-24 3/week @ 2019-12-31 18/week @ 2020-01-07 25/week @ 2020-01-14 3/week @ 2020-01-21 10/week @ 2020-02-04 15/week @ 2020-02-11 30/week @ 2020-02-18 11/week @ 2020-02-25

82 downloads per month

MPL-2.0 license

225KB
5.5K SLoC

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:

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

Dependencies

~1.7–2.2MB
~38K SLoC