splr 0.1.1

A pure rustic CDCL SAT solver based on Glucose
Documentation

Splr -- SAT Solver for Propositional Logic in Rust

Features

  • Splr is a pure Rustic SAT solver, based on Glucose 4.1.
  • It adopts many ideas in modern SAT solvers like:
    • Glucose-like dynamic blocking/forcing restarts based on EMAs
    • heuristics adaptation
    • pre/in-process simplification based on clause subsumption and variable elimination

Install

Just clone me, and cargo install.

Two executables will be installed:

  • splr -- SAT solver
  • dmcr -- A model checker to verify assignments which are generated by splr.

Usage

Splr is a standalone program, taking an CNF file. The result will be saved to a file.

$ splr tests/sample.cnf
sample.cnf                         250,1065 |time:     0.39, Mode:  Initial
 #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
   Conflicts|aLBD:     7.92, bjmp:     8.64, cnfl:    10.79 |blkR:   1.4000
   Clause DB|#rdc:        5, #sce:        2, #exe:        1 |frcK:   0.6500
SATISFIABLE: sample.cnf. The answer was dumped to .ans_sample.cnf.

$ cat .ans_sample.cnf
c An assignment generated by splr-0.1.1 for tests/sample.cnf
c
c sample.cnf                         , v:     250, c:    1065, time:     0.39
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:        1 |frcK:   0.6500
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 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:

2019, Shuji Narazaki