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 after installing the latest cargo. Two executables will be installed:

Alternatively, Nix users can use nix build.

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/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf unif-k3-r4.25-v360-c1530-S1293537826-039.cnf 360,1530 |time: 309.35 #conflict: 4156094, #decision: 5251386, #propagate: 225262345 Assignment|#rem: 350, #ass: 1, #elm: 9, prg%: 2.7778 Clause|Remv: 89387, LBD2: 1163, Binc: 28, Perm: 1538 Restart|#BLK: 0, #RST: 30968, trgr: 1, peak: 128 LBD|avrg: 10.5611, trnd: 0.9841, depG: 2.9608, /dpc: 1.36 Conflict|tASG: 0.9761, cLvl: 12.85, bLvl: 11.68, /ppc: 50.32 misc|elim: 7, #sub: 0, core: 0, /cpr: 123.60 Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf s SATISFIABLE: tests/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf

plain $ cat ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf c This file was generated by splr-0.7.0 for tests/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: 4156094, #decision: 5251386, #propagate: 225262345, c Assignment|#rem: 350, #fix: 1, #elm: 9, prg%: 2.7778, c Clause|Remv: 89387, LBD2: 1163, Binc: 28, Perm: 1538, c Restart|#BLK: 0, #RST: 30968, trgr: 1, peak: 128, c LBD|avrg: 10.5611, trnd: 0.9841, depG: 2.9608, /dpc: 1.36, c Conflict|tASG: 0.9761, cLvl: 12.85, bLvl: 11.68, /ppc: 50.32, c misc|elim: 7, #sub: 0, core: 0, /cpr: 123.60, c Strategy|mode: generic, time: 309.35, c s SATISFIABLE v 1 -2 3 4 5 6 -7 -8 9 -10 -11 -12 13 -14 -15 16 17 18 -19 20 ... -359 -360 0

plain $ dmcr tests/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf A valid assignment set for tests/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 splr --certificate and recommend to use Grid.

  1. Run splr with certificate option.

plain $ splr -c tests/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf unif-k3-r4.25-v360-c1530-S1028159446-096.cnf 360,1530 |time: 77.92 #conflict: 1531986, #decision: 1922419, #propagate: 80871699 Assignment|#rem: 279, #ass: 73, #elm: 8, prg%: 22.5000 Clause|Remv: 120822, LBD2: 752, Binc: 185, Perm: 1657 Restart|#BLK: 0, #RST: 12160, trgr: 1, peak: 1 LBD|avrg: 4.0368, trnd: 0.5933, depG: 1.9282, /dpc: 1.14 Conflict|tASG: 0.9954, cLvl: 7.47, bLvl: 6.34, /ppc: 53.05 misc|elim: 4, #sub: 23, core: 171, /cpr: 160.59 Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1028159446-096.cnf Certificate|file: proof.out s UNSATISFIABLE: tests/unif-k3-r4.25-v360-c1530-S1028159446-096.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/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat -o proof.grat c sizeof(cdbt) = 4 c sizeof(cdbt*) = 8 c Using RAT run heuristics c Parsing formula ... 1ms c Parsing proof (ASCII format) ... 12075ms c Forward pass ... 2763ms c Starting Backward pass c Single threaded mode c Waiting for aux-threads ...done c Lemmas processed by threads: 1381423 mdev: 0 c Finished Backward pass: 50489ms c Writing combined proof ... 14515ms s VERIFIED c Timing statistics (ms) c Parsing: 12077 c Checking: 53273 c * bwd: 50489 c Writing: 14515 c Overall: 79878 c * vrf: 65363

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

c Size statistics (bytes) c Number of clauses: 1535302 c Clause DB size: 105203416 c Item list: 47143024 c Pivots store: 8388608 ```

  1. Verify it with gratchk

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

```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 | | trgr | the number of the restart trigger before executing restart | | peak | the largest trigger so far | | avrg | the EMA, Exponential Moving Average, of LBD of learnt clauses | | depG | the EMA of LBD of the clauses used in conflict analysis | | /dpc | the EMA of decisions per conflict | | tASG | the current trend of the number of assigned vars after restart | | cLvl | the EMA of decision levels at which conflicts occur | | bLvl | the EMA of decision levels to which backjumps go | | /ppc | the EMA of propagations per conflict | | elim | the number of invocations of clause/var elimination | | #sub | the number of the clauses subsumed by caluse elimination processor | | core | the number of unreachable vars | | /cpr | the EMA of conflicts per restart | | mode | Selected strategy's id | | time | the elapsed CPU time in seconds |

Command line options

```plain $ splr --help A modern CDCL SAT solver in Rust Activated features: clause elimination, clause reduction, Learning-Rate based rewarding, Luby stabilization, reason side rewarding

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 -j, --journal Shows sub-module logs -l, --log Uses Glucose-like progress report -V, --version Prints version information OPTIONS (red options depend on features in Cargo.toml): --cbt Dec. lvl to use chronoBT 100 --cdr Clause reward decay rate 0.95 --cl Soft limit of #clauses (6MC/GB) 0 --ii #cls to start in-processor 16384 -t, --timeout CPU time limit in sec. 5000 --ecl Max #lit for clause subsume 18 --evl Grow limit of #cls in var elim. 0 --evo Max #cls for var elimination 20000 -o, --dir Output directory . -p, --proof DRAT Cert. filename proof.out -r, --result Result filename/stdout
--ral Length of assign. fast EMA 24 --ras Length of assign. slow EMA 8192 --rat Blocking restart threshold 0.75 --rll Length of LBD fast EMA 24 --rls Length of LBD slow EMA 8192 --rlt Forcing restart threshold 1.10 --rs #conflicts between restarts 24 --srd Decay rate for staged var reward 0.50 --srv Extra reward for staged vars 1.00 --vdr Var reward decay rate 0.94 --vds Var reward decay change step 0.10 ARGS: DIMACS CNF file ```

Solver description

Splr-0.7.0 adopts the following feature by default:

Among them, the unique feature is LubyStabilization. Let me explain it.

To make special periods with very low restart rate, known as 'stabilization mode,' Splr changes the number of restart trigger to execute restart. Usually SAT solvers execute 'restart' when the average LBD of learnt clauses getting higher. Splr requires that the condition holds by N times, where N is a value in the Luby series, and is changed during problem-solving. And, to avoid rapid parameters changes, Splr also introduces stages that share the same N. The length of stage is also controlled by Luby series. Here are the relations of values.

|stage n|N = Luby(n)|cycle|max N|stage len|restart cond.| restart | |--------:|--------------:|----:|------:|--------:|------------:|:-------:| | 1 | 1 | 0 | 1 | 1 | 1 | 1 | | 2 | 1 | 1 | 1 | 2 | 2 | 2 | | 3 | 2 | 1 | 1 | 1 | 3-4 | 3-4 | | 4 | 1 | 2 | 2 | 4 | 5-6 | 5-8 | | 5 | 1 | 2 | 2 | 4 | 7-8 | 9-12 | | 6 | 2 | 2 | 2 | 2 | 9-10 | 13-14 | | 7 | 4 | 2 | 2 | 1 | 11-14 | 15 | | 8 | 1 | 3 | 4 | 8 | 15-18 | 16-23 | | 9 | 1 | 3 | 4 | 8 | 19-22 | 24-31 | | 10 | 2 | 3 | 4 | 4 | 23-26 | 32-35 | | 11 | 1 | 3 | 4 | 8 | 27-30 | 36-43 | | 12 | 1 | 3 | 4 | 8 | 31-34 | 44-51 | | 13 | 2 | 3 | 4 | 4 | 35-38 | 52-55 | | 14 | 4 | 3 | 4 | 2 | 39-42 | 56-57 | | 15 | 8 | 3 | 4 | 1 | 43-50 | 58 | | 16 | 1 | 4 | 8 | 16 | 51-58 | 59-74 | | 17 | 1 | 4 | 8 | 16 | 59-66 | 75-90 | | 18 | 2 | 4 | 8 | 8 | 67-74 | 91-98 | | 19 | 1 | 4 | 8 | 16 | 75-82 | 99-114 | | 20 | 1 | 4 | 8 | 16 | 83-90 | 115-130 |

You can see effects of LubyStabilization with the value of trgr for N, peak for max N and /cpr for 'conflict per restart'. Here's an example.

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-2021, Narazaki Shuji