A modern SAT Solver for Propositional Logic in Rust

Splr is a modern SAT solver in Rust, based on Glucose 4.1. It adopts, or adopted, various research results on modern SAT solvers:

CDCL, watch literals, LBD and so on from Glucose, Minisat and the ancestors
Luby series based restart control
Glucose-like dynamic blocking/forcing restarts
pre/in-processor to simplify the given CNF
branching variable selection based on Learning Rate Based Branching with Reason Side Rewarding or EVSIDS
CaDiCaL-like extended phase saving
restart stabilization inspired by CadiCaL
clause vivification
trail saving

Many thanks to SAT researchers.

Please check ChangeLog about recent updates.

Correctness

Though Splr comes with ABSOLUTELY NO WARRANTY, I'd like to show some results.

Version 0.17.0

SAT Competition 2021, Benchmarks main track -- splr-0.17.0 solved with a 300 sec timeout (this is one of the best of splr):
- 49 satisfiable problems: all the solutions were correct.
- 34 unsatisfiable problems: all certifications were verified with Grat toolchain or drat-trim.

Install

Just run cargo install splr after installing the latest cargo. Two executables will be installed:

splr -- the solver
dmcr -- a very simple model checker to verify a satisfiable assignment set generated by splr.

Alternatively, Nix users can use nix build.

About `no_std` environment and feature `no_IO`

If you want to build a library for no_std environment, or if you want to compile with feature no_IO, you have to run cargo build --lib --features no_IO. They are incompatible with cargo install.

[2024-02-03] Feature platform_wasm was added.

Usage

Splr is a standalone program, taking a CNF file. The result will be saved to a file, which format is defined by SAT competition 2011 rules.

$ splr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
unif-k3-r4.25-v360-c1530-S1293537826-039.cnf       360,1530 |time:   732.01
 #conflict:    9663289, #decision:     23326959, #propagate:      546184944
  Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000
      Clause|Remv:    69224, LBD2:     2857, BinC:        1, Perm:     1522
    Conflict|entg:   7.0499, cLvl:  12.2451, bLvl:  11.1030, /cpr:    30.74
    Learning|avrg:  10.4375, trnd:   1.0069, #RST:   566140, /dpc:     1.18
        misc|vivC:     7370, subC:        0, core:      122, /ppc:    61.53
      Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
s SATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf

$ cat ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
c This file was generated by splr-0.15.0 for cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
c
c unif-k3-r4.25-v360-c1530-S1293537826-039.cnf, #var:      360, #cls:     1530
c  #conflict:    9663289, #decision:     23326959, #propagate:      546184944,
c   Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000,
c       Clause|Remv:    69224, LBD2:     2857, BinC:        1, Perm:     1522,
c     Conflict|entg:   7.0499, cLvl:  12.2451, bLvl:  11.1030, /cpr:    30.74,
c      Learing|avrg:  10.4375, trnd:   1.0069, #RST:   566140, /dpc:     1.18,
c         misc|vivC:     7370, subC:        0, core:      122, /ppc:    61.53,
c     Strategy|mode:  generic, time:   732.03,
c
c   config::VarRewardDecayRate                       0.960
c   assign::NumConflict                        9663289
c   assign::NumDecision                       23326959
c   assign::NumPropagation                   546184944
c   assign::NumRephase                             734
c   assign::NumRestart                          566141
c   assign::NumVar                                 360
c   assign::NumAssertedVar                           0
c   assign::NumEliminatedVar                         9
c   assign::NumReconflict                          653
c   assign::NumRepropagation                  12460396
c   assign::NumUnassertedVar                       351
c   assign::NumUnassignedVar                       351
c   assign::NumUnreachableVar                        0
c   assign::RootLevel                                0
c   assign::AssignRate                               0.000
c   assign::DecisionPerConflict                      1.179
c   assign::PropagationPerConflict                  61.527
c   assign::ConflictPerRestart                     122.388
c   assign::ConflictPerBaseRestart                 122.388
c   assign::BestPhaseDivergenceRate                  0.000
c   clause::NumBiClause                              1
c   clause::NumBiClauseCompletion                    0
c   clause::NumBiLearnt                              1
c   clause::NumClause                            70746
c   clause::NumLBD2                               2857
c   clause::NumLearnt                            69224
c   clause::NumReduction                          1461
c   clause::NumReRegistration                        0
c   clause::Timestamp                                0
c   clause::LiteralBlockDistance                    10.438
c   clause::LiteralBlockEntanglement                 7.050
c   state::Vivification                            735
c   state::VivifiedClause                         7370
c   state::VivifiedVar                               0
c   state::NumCycle                                734
c   state::NumStage                               1461
c   state::IntervalScale                             1
c   state::IntervalScaleMax                       1024
c   state::BackjumpLevel                            11.103
c   state::ConflictLevel                            12.245
c
s SATISFIABLE
v 1 -2 3 4 5 6 -7 -8 9 -10 -11 -12 13 -14 ...  -360 0

$ dmcr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
A valid assignment set for cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf is found in ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf

If you want to certificate unsatisfiability, use --certify or -c and use proof checker like Grid.

Firstly run splr with the certificate option -c.

$ splr -c cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
unif-k3-r4.25-v360-c1530-S1028159446-096.cnf       360,1530 |time:   204.09
 #conflict:    4018458, #decision:      9511129, #propagate:      221662222
  Assignment|#rem:      345, #fix:        7, #elm:        8, prg%:   4.1667
      Clause|Remv:    11290, LBD2:     2018, BinC:      137, Perm:     1517
    Conflict|entg:   4.5352, cLvl:   8.0716, bLvl:   6.9145, /cpr:   112.08
    Learning|avrg:   1.5625, trnd:   0.2219, #RST:   237295, /dpc:     1.07
        misc|vivC:     4085, subC:        0, core:      345, /ppc:    52.55
      Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
 Certificate|file: proof.drat
s UNSATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf

A: Verify with drat-trim

$ drat-trim cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat
c parsing input formula with 360 variables and 1530 clauses
c finished parsing
c detected empty clause; start verification via backward checking
c 1530 of 1530 clauses in core
c 2036187 of 4029964 lemmas in core using 68451907 resolution steps
c 0 RAT lemmas in core; 908116 redundant literals in core lemmas
s VERIFIED
c verification time: 105.841 seconds

B: Verify with gratchk

Firstly you have to convert the generated DRAT file to a GRAT file.

$ gratgen cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat -o proof.grat
c sizeof(cdb_t) = 4
c sizeof(cdb_t*) = 8
c Using RAT run heuristics
c Parsing formula ... 1ms
c Parsing proof (ASCII format) ... 32251ms
c Forward pass ... 2073ms
c Starting Backward pass
c Single threaded mode

0%   10   20   30   40   50   60   70   80   90   100%
|----|----|----|----|----|----|----|----|----|----|
***************************************************
c Waiting for aux-threads ...done
c Lemmas processed by threads: 2032698 mdev: 0
c Finished Backward pass: 65356ms
c Writing combined proof ... 19088ms
s VERIFIED
c Timing statistics (ms)
c Parsing:  32253
c Checking: 67465
c   * bwd:  65356
c Writing:  19088
c Overall:  118808
c   * vrf:  99720

c Lemma statistics
c RUP lemmas:  2032698
c RAT lemmas:  0
c   RAT run heuristics:   0
c Total lemmas:  2032698

c Size statistics (bytes)
c Number of clauses: 4031493
c Clause DB size:  309680252
c Item list:       128778112
c Pivots store:    16777216

Then verify it with gratchk.

$ gratchk unsat cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.grat
c Reading cnf
c Reading proof
c Done
c Verifying unsat
s VERIFIED UNSAT

Calling Splr from Rust programs

Since 0.4.0, you can use Splr in your programs. (Here I suppose that you uses Rust 2021.)

use splr::*;

fn main() {
    let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]];
    match Certificate::try_from(v) {
        Ok(Certificate::SAT(ans)) => println!("s SATISFIABLE: {:?}", ans),
        Ok(Certificate::UNSAT) => println!("s UNSATISFIABLE"),
        Err(e) => panic!("s UNKNOWN; {}", e),
    }
}

Note: As of version 0.18.0, Splr no longer supports incremental mode, as it is not part of the development direction.

sample code from my sudoku solver

https://github.com/shnarazk/sudoku_sat/blob/4490b4358e5f3b72803a566323a6c8c196627f92/src/bin/sudoku400.rs#L36-L60

let

Splr

Install / Use

README

A modern SAT Solver for Propositional Logic in Rust

Correctness

Version 0.17.0

Install

About `no_std` environment and feature `no_IO`

Usage

A: Verify with drat-trim

B: Verify with gratchk

Calling Splr from Rust programs

sample code from my sudoku solver

Splr

Install / Use

README

A modern SAT Solver for Propositional Logic in Rust

Correctness

Version 0.17.0

Install

About no_std environment and feature no_IO

Usage

A: Verify with drat-trim

B: Verify with gratchk

Calling Splr from Rust programs

sample code from my sudoku solver

About `no_std` environment and feature `no_IO`