splr 0.4.0

A modern SAT Solver for Propositional Logic in Rust

Splr is a pure Rustic modern 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 and CaDiCaL-like stabilization
• pre/in-process simplification based on clause subsumption and variable elimination
• compile-time selection of a variant of Learning Rate Based Branching with Reason Side Rewarding and EVSIDS
• chronological backtrack aka chronoBT
• Glucose-like heuristics adaptation
• CaDiCaL-like extended phase 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.4.0

• SAT Race 2019, Benchmarks, splr-0.4.0(e0461bd) solved with a 300 sec (soft) timeout:
  • 43 satisfiable problems: all the solutions were correct.
  • 4 unsatisfiable problems: all were verified with Grad.

Version 0.3.1

• SAT Race 2019, Benchmarks, splr-0.3.1 solved with a 200 sec (soft) 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

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

Install

Just run cargo install splr after installing the latest cargo. 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:     1.27
 #conflict:      38892, #decision:        47095, #propagate:          85990 
  Assignment|#rem:      243, #fix:        1, #elm:        6, prg%:   2.8000 
      Clause|Remv:    19886, LBD2:      114, Binc:        0, Perm:     1056 
   Stabilize|#BLK:      257, #RST:      512, tASG:   1.3309, tLBD:   0.9605 
    Conflict|eLBD:     9.27, cnfl:    12.84, bjmp:    11.83, rpc%:   1.3165 
        misc|#rdc:        7, #smp:        1, 2smp:    36681, vdcy:   0.9800 
    Strategy|mode: Initial search phase before a main strategy
      Result|file: ./.ans_sample.cnf
s SATISFIABLE: tests/sample.cnf

$ cat .ans_sample.cnf
c An assignment set generated by splr-0.4.0 for tests/sample.cnf
c 
c CNF file(sample.cnf), #var:      250, #cls:     1065
c  #conflict:      38892, #decision:        47095, #propagate:          85990 
c   Assignment|#rem:      243, #fix:        1, #elm:        6, prg%:   2.8000 
c       Clause|Remv:    19886, LBD2:      114, Binc:        0, Perm:     1056 
c      Restart|#BLK:      257, #RST:      512, eASG:   1.3309, eLBD:   0.9605 
c     Conflict|eLBD:     9.27, cnfl:    12.84, bjmp:    11.83, rpc%:   1.3190 
c         misc|#rdc:        7, #smp:        1, 2smp:    36681, vdcy:   0.9800 
c     Strategy|mode:        Initial, time:     1.27
c 
s SATISFIABLE
v 1 2 3 4 -5 6 7 -8 -9 10 11 -12 -13 -14 15 16 -17 18 ... 0

$ dmcr tests/sample.cnf
A valid assignment set for tests/sample.cnf is found in .ans_sample.cnf.

Since 0.4.0, you can use Splr in your programs.

use splr::*;
use std::convert::TryFrom;

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(Cetrificate::UNSAT) => println!("s UNSATISFIABLE"),
        Err(e) => panic!("s UNKNOWN; {}", e),
    }
}

Mnemonics used in the progress message

Command line options

Please check help message.

• The 'switch' in help message below is either '1' or '0' to or not to use a module.
• Splr can't handle compressed CNF files so far.

$ splr --help
splr 0.4.0
Narazaki Shuji <shujinarazaki@protonmail.com>
A modern CDCL SAT solver in Rust

USAGE:
    splr [FLAGS] [OPTIONS] <cnf-file>

FLAGS:
    -h, --help        Prints help information
    -C, --no-color    Disable coloring
    -q, --quiet       Disable any progress message
    -c, --certify     Writes a DRAT UNSAT certification file
    -l, --log         Uses Glucose-like progress report
    -V, --version     Prints version information

OPTIONS:
        --ADP <adaptive>          Strategy adaptation switch [default: 1]
        --cbt <cbt-thr>           Level threshold to use chronoBT [default: 100]
        --cl <clause-limit>       Soft limit of #clauses (6MC/GB) [default: 0]
        --stat <dump-int>         Interval for dumping stat data [default: 0]
        --PRO <elim>              Pre/in-processor switch [default: 1]
        --ecl <elim-cls-lim>      Max #lit for clause subsume [default: 100]
        --evl <elim-grw-lim>      Grow limit of #cls in var elim [default: 0]
        --et <elim-trigger>       #cls to start simplification [default: 40000]
        --evo <elim-var-occ>      Max #cls for var elimination [default: 10000]
    -o, --dir <output-dir>        Output directory [default: .]
    -p, --proof <proof-file>      Cert. file in DRAT format [default: proof.out]
        --RDC <reduce>            Clause reduction switch [default: 1]
        --RPH <rephase>           Rephase switch [default: 1]
    -r, --result <result-file>    Result filename/stdout [default: ]
        --RSR <rsr>               Reason-Side Rewarding switch [default: 1]
        --ral <rst-asg-len>       Length for assignment average [default: 3500]
        --rab <rst-asg-thr>       Blocking restart threshold [default: 1.40]
        --rll <rst-lbd-len>       Length of LBD fast EMA [default: 50]
        --rls <rst-lbd-slw>       Length of LBD slow EMA [default: 10000]
        --rlt <rst-lbd-thr>       Forcing restart threshold [default: 0.70]
        --rss <rst-stb-scl>       Stabilizer scaling [default: 2.0]
        --rs <rst-step>           #conflicts between restarts [default: 50]
        --STB <stabilize>         Stabilization switch [default: 1]
    -t, --timeout <timeout>       CPU time limit in sec [default: 5000.0]
        --vri <vrw-dcy-beg>       Initial var reward decay [default: 0.75]
        --vrm <vrw-dcy-end>       Maximum var reward decay [default: 0.98]

ARGS:
    <cnf-file>    CNF file in DIMACS format

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