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.

```plain $ 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.

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

fn main() { let v: Vec> = 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

| mnemonic | meaning | | --------- |------- | | v | the number of variables used in the given CNF file | | c | the number of clauses used in the given CNF file | | time | elapsed CPU time in seconds (or wall-clock time if CPU time is not available) | | #conflict | the number of conflicts | | #decision | the number of decisions | | #propagate | the number of propagates (its unit is literal) | | #rem | the number of remaining variables | | #fix | the number of solved variables (which has been assigned a value at decision level zero) | | #elm | the number of eliminated variables | | prg% | the percentage of remaining variables / total variables | | Remv | the number of learnt clauses which are not biclauses | | LBD2 | the number of learnt clauses which LBDs are 2 | | Binc | the number of binary learnt clauses | | Perm | the number of given clauses and binary learnt clauses | | #BLK | the number of blocking restart | | #RST | the number of restart | | tASG | the trend rate of the number of assigned variables | | tLBD | the trend rate of learn clause's LBD | | eLBD | the EMA, Exponential Moving Average, of learn clauses' LBDs | | cnfl | the EMA of decision levels to which backjumps go | | bjmp | the EMA of decision levels at which conflicts occur | | rpc% | a percentage of restart per conflict | | #rdc | the number of clause reduction invocations | | #smp | the number of clause and var simplification invocations | | 2smp | the number of literals to invoke the simplifier again | | vdcy | var activity decay rate | | mode | Selected strategy's id | | time | the elapsed CPU time in seconds |

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.

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

USAGE: splr [FLAGS] [OPTIONS]

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 Strategy adaptation switch [default: 1] --cbt Level threshold to use chronoBT [default: 100] --cl Soft limit of #clauses (6MC/GB) [default: 0] --stat Interval for dumping stat data [default: 0] --PRO Pre/in-processor switch [default: 1] --ecl Max #lit for clause subsume [default: 100] --evl Grow limit of #cls in var elim [default: 0] --et #cls to start simplification [default: 40000] --evo Max #cls for var elimination [default: 10000] -o, --dir Output directory [default: .] -p, --proof Cert. file in DRAT format [default: proof.out] --RDC Clause reduction switch [default: 1] --RPH Rephase switch [default: 1] -r, --result Result filename/stdout [default: ] --RSR Reason-Side Rewarding switch [default: 1] --ral Length for assignment average [default: 3500] --rab Blocking restart threshold [default: 1.40] --rll Length of LBD fast EMA [default: 50] --rls Length of LBD slow EMA [default: 10000] --rlt Forcing restart threshold [default: 0.70] --rss Stabilizer scaling [default: 2.0] --rs #conflicts between restarts [default: 50] --STB Stabilization switch [default: 1] -t, --timeout CPU time limit in sec [default: 5000.0] --vri Initial var reward decay [default: 0.75] --vrm Maximum var reward decay [default: 0.98]

ARGS: 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