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:

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

_Warning: Version 0.6.0 isn't the best version. It changed most modules like var reward mechanism, restart policy and in-processor timing.

Benchmark result(2021-01-16)

Install

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

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.

plain $ splr tests/uf250-02.cnf [ 512] Lcycle: 1, core: 135, #ion: 6, /cpr: 256.00 [ 1792] Lcycle: 2, core: 132, #ion: 3, /cpr: 358.40 [ 6144] Lcycle: 3, core: 114, #ion: 1, /cpr: 512.00 uf250-02.cnf 250,1065 |time: 0.12 #conflict: 6286, #decision: 7133, #propagate: 267271 Assignment|#rem: 244, #ass: 0, #elm: 6, prg%: 2.4000 Clause|Remv: 5737, LBD2: 26, Binc: 0, Perm: 1061 Stabilize|#BLK: 19, #RST: 13, #ion: 1, Lspn: 1 EMA|tLBD: 18.3107, tASG: 4.4215, core: 0, /dpc: 1.13 Conflict|eLBD: 13.25, cnfl: 11.62, bjmp: 10.88, /ppc: 42.52 misc|elim: 1, cviv: 0, #vbv: 0, /cpr: 483.54 Result|file: ./.ans_uf250-02.cnf s SATISFIABLE: tests/uf250-02.cnf

plain $ cat .ans_uf250-02.cnf c This file was generated by splr-0.6.0 for tests/uf250-02.cnf c c CNF file(uf250-02.cnf), #var: 250, #cls: 1065 c #conflict: 6286, #decision: 7133, #propagate: 267271, c Assignment|#rem: 244, #fix: 0, #elm: 6, prg%: 2.4000, c Clause|Remv: 5737, LBD2: 26, Binc: 0, Perm: 1061, c Restart|#BLK: 19, #RST: 13, #ion: 1, Lcyc: 3, c EMA|tLBD: 18.3107, tASG: 4.4215, core: 0, /dpc: 1.13, c Conflict|eLBD: 13.25, cnfl: 11.62, bjmp: 10.88, /ppc: 42.52, c misc|elim: 1, cviv: 0, #vbv: 0, /cpr: 483.54, c Strategy|mode: generic, time: 0.12, c s SATISFIABLE v -1 -2 -3 4 5 6 7 -8 9 10 11 12 -13 14 -15 16 -17 -18 19 -20 ... -250 0

plain $ dmcr tests/uf250-02.cnf A valid assignment set for tests/uf250-02.cnf is found in .ans_uf250-02.cnf

If you want to certificate unsatisfiability, use splr --certificate and recommend to use Grid.

  1. Run splr with certificate option.

plain $ splr -c tests/unsat.cnf unsat.cnf 83,570 |time: 0.00 #conflict: 0, #decision: 0, #propagate: 0 Assignment|#rem: 19, #ass: 64, #elm: 0, prg%: 77.1084 Clause|Remv: 0, LBD2: 0, Binc: 126, Perm: 135 Restart|#BLK: 0, #RST: 0, #ion: 0, Lspn: 1 EMA|tLBD: NaN, tASG: NaN, core: 83, /dpc: NaN Conflict|eLBD: 0.00, cnfl: 0.00, bjmp: 0.00, /ppc: NaN misc|elim: 1, cviv: 0, #vbv: 0, /cpr: NaN Result|file: ./.ans_unsat.cnf Certificate|file: proof.out s UNSATISFIABLE: tests/unsat.cnf

  1. Trim comments from the output

plain $ egrep -v '^[cs]' < proof.out > proof.drat

  1. Convert the drat file to a grat file.

```plain $ gratgen tests/unsat.cnf proof.drat -o proof.grat c sizeof(cdbt) = 4 c sizeof(cdbt*) = 8 c Using RAT run heuristics c Parsing formula ... 0ms c Parsing proof (ASCII format) ... 1ms c Forward pass ... 0ms c Starting Backward pass c Single threaded mode c Waiting for aux-threads ...done c Lemmas processed by threads: 0 mdev: nan c Finished Backward pass: 0ms c Writing combined proof ... 0ms s VERIFIED c Timing statistics (ms) c Parsing: 1 c Checking: 0 c * bwd: 0 c Writing: 0 c Overall: 2 c * vrf: 2

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

c Size statistics (bytes) c Number of clauses: 1110 c Clause DB size: 27612 c Item list: 23840 c Pivots store: 8192 ```

  1. Verify it with gratchk

plain $ gratchk unsat tests/unsat.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.

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

All solutions SAT solver

```rust use splr::*; use std::{convert::TryFrom, env::args};

fn main() { let cnf = args().nth(1).expect("takes an arg"); let assigns: Vec = Vec::new(); println!("#solutions: {}", run(&cnf, &assigns)); }

[cfg(feature = "incremental_solver")]

fn run(cnf: &str, assigns: &[i32]) -> usize { let mut solver = Solver::tryfrom(cnf).expect("panic at loading a CNF"); for n in assigns.iter() { solver.addassignment(*n).expect("panic at assertion"); } let mut count = 0; loop { match solver.solve() { Ok(Certificate::SAT(ans)) => { count += 1; println!("s SATISFIABLE({}): {:?}", count, ans); let ans = ans.iter().map(|i| -i).collect::>(); match solver.addclause(ans) { Err(SolverError::Inconsistent) => { println!("c no answer due to level zero conflict"); break; } Err(e) => { println!("s UNKNOWN; {:?}", e); break; } Ok() => solver.reset(), } } Ok(Certificate::UNSAT) => { println!("s UNSATISFIABLE"); break; } Err(e) => { println!("s UNKNOWN; {}", e); break; } } } count } ```

Since 0.4.1, Solver has iter(). So you can iterate on satisfiable 'solution: Vec<i32>'s as:

```rust

[cfg(feature = "incremental_solver")]

for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() { println!("{}-th answer: {:?}", i, v); } ```

Mnemonics used in the progress message

| mnemonic | meaning | | ------------ | ----------------------------------------------------------------------------------------- | | #var | the number of variables used in the given CNF file | | #cls | 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 | | #ass | the number of asserted 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 | | Lspn | the current length of rephrase mode | | Lcyc | the number of Lucy-based rephrasing cycle | | tLBD | the trend rate of learn clause's LBD | | core | the least number of unassigned vars | | /dpc | decisions per conflict | | eLBD | the EMA, Exponential Moving Average, of learn clauses' LBDs | | cnfl | the EMA of decision levels at which conflicts occur | | bjmp | the EMA of decision levels to which backjumps go | | /ppc | propagations per conflict | | elim | the number of invocations of clause/var elimination | | cviv | the number of invocations of clause vivification | | #vbv | the number of vars which were asserted by clause vivification | | /cpr | conflicts per restart | | mode | Selected strategy's id | | time | the elapsed CPU time in seconds | | #ion | the number of vars with high activities but aren't involved in best phase |

Command line options

Please check the help message.

```plain $ splr --help splr 0.6.0 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 (green options depends on compile-time flags): OPTIONS (red options depend on features in Cargo.toml): --ADP Strategy adaptation switch 0 --ELI Eliminator switch 1 --LBY Use Luby series for restart 0 --RDC Clause reduction switch 1 --RPH Re-phase switch 1 --RSR Reason-Side Rewarding switch 1 --STB Stabilization switch 1 --STG Stage switch 1 --VIV Vivification switch 0 --cbt Dec. lvl to use chronoBT 100 --cl Soft limit of #clauses (6MC/GB) 0 --ii #cls to start in-processor 10000 -t, --timeout CPU time limit in sec. 5000 --ecl Max #lit for clause subsume 32 --evl Grow limit of #cls in var elim. 0 --evo Max #cls for var elimination 8192 -o, --dir Output directory . -p, --proof DRAT Cert. filename proof.out -r, --result Result filename/stdout
--ral Length of assign. fast EMA 32 --ras Length of assign. slow EMA 10000 --rat Blocking restart threshold 0.10 --rct Conflict Correlation threshold 0.00 --rll Length of LBD fast EMA 32 --rls Length of LBD slow EMA 8192 --rlt Forcing restart threshold 1.20 --rms Scaling for Max LBD of Dep. 0.00 --rmt Threshold for Max LBD of Dep. 0.00 --rss Stabilizer scaling 2.00 --rs #conflicts between restarts 24 --srd Decay rate for staged vare reward 0.50 --srv Extra reward for staged vars 1.00 --vit #clause to try to vivify 200 --vri Initial var reward decay 0.00 --vrm Maximum var reward decay 0.00 --vro Occ. compression rate in LR 0.00 ARGS: DIMACS CNF file ```

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