A modern SAT Solver for Propositional Logic in Rust

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

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

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

• SAT Competition 2021, Benchmarks main truck -- splr-0.12.0 RC (ed953b78) solved with a 500 sec timeout:
  • 42 satisfiable problems: all the solutions were correct.
  • 42 unsatisfiable problems: all the certifications were verified with Grad.

Version 0.11.0

• all the certifications of UUF250 were correct and verified with Grad.
• SAT Race 2019, Benchmarks -- splr-0.11.0 RC (84895b21) solved with a 300 sec timeout:
  • 43 satisfiable problems: all the solutions were correct.
  • 7 unsatisfiable problems: all the certifications were verified with Grad.

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.

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 unif-k3-r4.25-v360-c1530-S1293537826-039.cnf 360,1530 |time: 721.28 #conflict: 3527930, #decision: 6730814, #propagate: 186925863 Assignment|#rem: 351, #fix: 0, #elm: 9, prg%: 2.5000 Clause|Remv: 69093, LBD2: 773, BinC: 0, Perm: 1521 Restart|#BLK: 0, #RST: 14222, *scl: 1, sclM: 32 LBD|trnd: 0.8328, avrg: 10.2688, depG: 3.0410, /dpc: 1.19 Conflict|tASG: 0.9836, cLvl: 15.21, bLvl: 14.07, /ppc: 57.09 misc|vivC: 1351, subC: 0, core: 138, /cpr: 991.44 Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf s SATISFIABLE: cnfs/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.11.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: 3527930, #decision: 6730814, #propagate: 186925863, c Assignment|#rem: 351, #fix: 0, #elm: 9, prg%: 2.5000, c Clause|Remv: 69093, LBD2: 773, BinC: 0, Perm: 1521, c Restart|#BLK: 0, #RST: 14222, *scl: 1, sclM: 32, c LBD|avrg: 10.2688, trnd: 0.8328, depG: 3.0410, /dpc: 1.19, c Conflict|tASG: 0.9836, cLvl: 15.21, bLvl: 14.07, /ppc: 57.09, c misc|vivC: 104, subC: 0, core: 138, /cpr: 991.44, c Strategy|mode: generic, time: 721.29, c c config::ChronoBtThreshold 100 c config::ClauseRewardDecayRate 0.95 c config::InprocessorInterval 10000 c config::RestartAsgThreshold 0.6 c config::RestartLbdThreshold 1.6 c config::VarRewardDecayRate 0.96 c assign::NumConflict 3527930 c assign::NumDecision 6730814 c assign::NumPropagation 186925863 c assign::NumRephase 60 c assign::NumRestart 14223 c assign::NumVar 360 c assign::NumAssertedVar 0 c assign::NumEliminatedVar 9 c assign::NumUnassertedVar 351 c assign::NumUnassignedVar 351 c assign::NumUnreachableVar 0 c assign::RootLevel 0 c assign::DecisionPerConflict 1.190 c assign::PropagationPerConflict 57.089 c assign::ConflictPerRestart 1021.985 c assign::ConflictPerBaseRestart 1021.985 c assign::BestPhaseDivergenceRate 0.263 c clause::NumBiClause 0 c clause::NumBiClauseCompletion 0 c clause::NumBiLearnt 0 c clause::NumClause 70614 c clause::NumLBD2 773 c clause::NumLearnt 69093 c clause::NumReduction 102 c clause::NumReRegistration 0 c clause::Timestamp 3527930 c clause::DpAverageLBD 3.041 c processor::NumFullElimination 104 c processor::NumSubsumedClause 0 c restart::NumBlock 0 c restart::NumCycle 5 c restart::NumRestart 14223 c restart::NumStage 102 c restart::IntervalScale 1 c restart::IntervalScaleMax 32 c state::NumDecisionConflict 1771382 c state::NumProcessor 103 c state::Vivification 103 c state::VivifiedClause 1351 c state::VivifiedVar 0 c state::BackjumpLevel 14.071 c state::ConflictLevel 15.207 c s SATISFIABLE v 1 -2 3 4 5 6 -7 -8 9 -10 -11 -12 13 -14 ... -360 0

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

1. Run splr with the certificate option.

plain $ splr -c cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf unif-k3-r4.25-v360-c1530-S1028159446-096.cnf 360,1530 |time: 354.12 #conflict: 2183312, #decision: 3933643, #propagate: 112056337 Assignment|#rem: 350, #fix: 2, #elm: 8, prg%: 2.7778 Clause|Remv: 68795, LBD2: 761, BinC: 532, Perm: 2013 Restart|#BLK: 0, #RST: 13680, *scl: 2, sclM: 32 LBD|trnd: 0.3261, avrg: 2.2739, depG: 2.1646, /dpc: 1.06 Conflict|tASG: 1.0175, cLvl: 7.98, bLvl: 6.84, /ppc: 51.88 misc|vivC: 1195, subC: 0, core: 350, /cpr: 201.37 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

1. Convert the generated DRAT file to a GRAT file.

```plain $ gratgen cnfs/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 ... 2ms c Parsing proof (ASCII format) ... 19986ms c Forward pass ... 4417ms c Starting Backward pass c Single threaded mode c Waiting for aux-threads ...done c Lemmas processed by threads: 1936846 mdev: 0 c Finished Backward pass: 99600ms c Writing combined proof ... 19980ms s VERIFIED c Timing statistics (ms) c Parsing: 19989 c Checking: 104047 c * bwd: 99600 c Writing: 19980 c Overall: 144024 c * vrf: 124044

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

c Size statistics (bytes) c Number of clauses: 2195700 c Clause DB size: 162762960 c Item list: 69104688 c Pivots store: 16777216 ```

1. Verify it with gratchk.

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

```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 | | #fix | 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 current number of learnt clauses that are not bi-clauses | | LBD2 | the accumulated number of learnt clauses which LBDs are 2 | | BinC | the current number of binary learnt clauses | | Perm | the current number of given clauses and binary learnt clauses | | #BLK | the number of blocking restarts | | #RST | the number of restarts | | *scl | the scaling factor for restart interval used in Luby stabilization | | sclM | the largest scaling factor so far | | avrg | the EMA, Exponential Moving Average, of LBD of learnt clauses | | trnd | the current trend of the LBD's EMA | | 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 | | vivC | the number of the vivified clauses | | subC | the number of the clauses subsumed by clause 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: best phase tracking, binary clause completion, clause elimination, clause vivification, Learning-Rate based rewarding, Luby stabilization, reason side rewarding, stage-based rephase

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 10000 -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.drat -r, --result Result filename/stdout
--ral Length of assign. fast EMA 24 --ras Length of assign. slow EMA 8192 --rat Blocking restart threshold 0.60 --rll Length of LBD fast EMA 8 --rls Length of LBD slow EMA 8192 --rlt Forcing restart threshold 1.60 --rs #conflicts between restarts 2 --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.12.0 adopts the following features by default:

• Learning-rate based (LRB) var rewarding and clause rewarding[3]
• Reason-side var rewarding[3]
• ~~chronological backtrack[4]~~ disabled in 0.12 due to incorrect UNSAT certificates.
• clause vivification[5]
• dynamic restart based on average LBDs of learnt clauses[1]
• dynamic restart blocking based on the number of remaining vars[2]
• clause elimination and subsumption as pre-processor and in-processor
• stabilization based on Luby series, or Luby Stabilization
• re-phase the best phases

As shown in the blow, Splr calls in-processor very frequently.

Luby stabilization is an original mechanism to make long periods without restarts, which are called stabilized modes. In this method, every clause reduction updates the restart interval, which usually has a constant value, as follows:

restart_interval = luby(n) * base_interval; where n represents the number of updates, and luby(n) is a function returning n-th value of Luby series. The longer the solver searches, the larger the average value is. So we can periodically explore the search space more deeply.

Here is an example.

Note: the mechanism explained here is different from that used in Splr-0.10.0.

Bibliography

• [1] G. Audemard and L. Simon, "Predicting learnt clauses quality in modern SAT solvers," in International Joint Conference on Artificial Intelligence 2009, pp. 399–404, 2009.

• [2] G. Audemard and L. Simon, "Refining restarts strategies for SAT and UNSAT," in Lecture Notes in Computer Science, vol.7513, pp.118–126, 2012.

• [3] J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, "Learning Rate Based Branching Heuristic for SAT Solvers," in Lecture Notes in Computer Science, vol.9710, pp.123–140, 2016.

• [4] A. Nadel and V. Ryvchin, "Chronological Backtracking," in Theory and Applications of Satisfiability Testing - SAT 2018, June 2018, pp.111–121, 2018.

• [5] C. Piette, Y. Hamadi, and L. Saïs, "Vivifying propositional clausal formulae," Front. Artif. Intell. Appl., vol.178, pp.525–529, 2008.

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