Splr is a modern SAT solver in Rust, based on Glucose 4.1. It adopts, or adopted, various research results on modern SAT solvers:
- CDCL, watch literals, LBD and so on from Glucose, Minisat and the ancestors
- Luby series based restart control
- Glucose-like dynamic blocking/forcing restarts
- pre/in-processor to simplify the given CNF
- branching variable selection based on Learning Rate Based Branching with Reason Side Rewarding or EVSIDS
- CaDiCaL-like extended phase saving
- restart stabilization inspired by CadiCaL
- clause vivification
- trail saving
Many thanks to SAT researchers.
Please check ChangeLog about recent updates.
Though Splr comes with ABSOLUTELY NO WARRANTY, I'd like to show some results.
- SAT Competition 2021, Benchmarks main track -- splr-0.17.0 solved with a 300 sec timeout (this is one of the best of splr):
- 49 satisfiable problems: all the solutions were correct.
- 34 unsatisfiable problems: all certifications were verified with Grat toolchain or drat-trim.
Just run cargo install splr after installing the latest cargo.
Two executables will be installed:
splr-- the solverdmcr-- a very simple model checker to verify a satisfiable assignment set generated bysplr.
Alternatively, Nix users can use nix build.
If you want to build a library for no_std environment,
or if you want to compile with feature no_IO,
you have to run cargo build --lib --features no_IO.
They are incompatible with cargo install.
- [2024-02-03] Feature
platform_wasmwas added.
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.
$ splr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
unif-k3-r4.25-v360-c1530-S1293537826-039.cnf 360,1530 |time: 732.01
#conflict: 9663289, #decision: 23326959, #propagate: 546184944
Assignment|#rem: 351, #fix: 0, #elm: 9, prg%: 2.5000
Clause|Remv: 69224, LBD2: 2857, BinC: 1, Perm: 1522
Conflict|entg: 7.0499, cLvl: 12.2451, bLvl: 11.1030, /cpr: 30.74
Learning|avrg: 10.4375, trnd: 1.0069, #RST: 566140, /dpc: 1.18
misc|vivC: 7370, subC: 0, core: 122, /ppc: 61.53
Result|file: ./ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
s SATISFIABLE: cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
$ cat ans_unif-k3-r4.25-v360-c1530-S1293537826-039.cnf
c This file was generated by splr-0.15.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: 9663289, #decision: 23326959, #propagate: 546184944,
c Assignment|#rem: 351, #fix: 0, #elm: 9, prg%: 2.5000,
c Clause|Remv: 69224, LBD2: 2857, BinC: 1, Perm: 1522,
c Conflict|entg: 7.0499, cLvl: 12.2451, bLvl: 11.1030, /cpr: 30.74,
c Learing|avrg: 10.4375, trnd: 1.0069, #RST: 566140, /dpc: 1.18,
c misc|vivC: 7370, subC: 0, core: 122, /ppc: 61.53,
c Strategy|mode: generic, time: 732.03,
c
c config::VarRewardDecayRate 0.960
c assign::NumConflict 9663289
c assign::NumDecision 23326959
c assign::NumPropagation 546184944
c assign::NumRephase 734
c assign::NumRestart 566141
c assign::NumVar 360
c assign::NumAssertedVar 0
c assign::NumEliminatedVar 9
c assign::NumReconflict 653
c assign::NumRepropagation 12460396
c assign::NumUnassertedVar 351
c assign::NumUnassignedVar 351
c assign::NumUnreachableVar 0
c assign::RootLevel 0
c assign::AssignRate 0.000
c assign::DecisionPerConflict 1.179
c assign::PropagationPerConflict 61.527
c assign::ConflictPerRestart 122.388
c assign::ConflictPerBaseRestart 122.388
c assign::BestPhaseDivergenceRate 0.000
c clause::NumBiClause 1
c clause::NumBiClauseCompletion 0
c clause::NumBiLearnt 1
c clause::NumClause 70746
c clause::NumLBD2 2857
c clause::NumLearnt 69224
c clause::NumReduction 1461
c clause::NumReRegistration 0
c clause::Timestamp 0
c clause::LiteralBlockDistance 10.438
c clause::LiteralBlockEntanglement 7.050
c state::Vivification 735
c state::VivifiedClause 7370
c state::VivifiedVar 0
c state::NumCycle 734
c state::NumStage 1461
c state::IntervalScale 1
c state::IntervalScaleMax 1024
c state::BackjumpLevel 11.103
c state::ConflictLevel 12.245
c
s SATISFIABLE
v 1 -2 3 4 5 6 -7 -8 9 -10 -11 -12 13 -14 ... -360 0
$ 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.
Firstly run splr with the certificate option -c.
$ splr -c cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
unif-k3-r4.25-v360-c1530-S1028159446-096.cnf 360,1530 |time: 204.09
#conflict: 4018458, #decision: 9511129, #propagate: 221662222
Assignment|#rem: 345, #fix: 7, #elm: 8, prg%: 4.1667
Clause|Remv: 11290, LBD2: 2018, BinC: 137, Perm: 1517
Conflict|entg: 4.5352, cLvl: 8.0716, bLvl: 6.9145, /cpr: 112.08
Learning|avrg: 1.5625, trnd: 0.2219, #RST: 237295, /dpc: 1.07
misc|vivC: 4085, subC: 0, core: 345, /ppc: 52.55
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
A: Verify with drat-trim
$ drat-trim cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat
c parsing input formula with 360 variables and 1530 clauses
c finished parsing
c detected empty clause; start verification via backward checking
c 1530 of 1530 clauses in core
c 2036187 of 4029964 lemmas in core using 68451907 resolution steps
c 0 RAT lemmas in core; 908116 redundant literals in core lemmas
s VERIFIED
c verification time: 105.841 seconds
Firstly you have to convert the generated DRAT file to a GRAT file.
$ gratgen cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf proof.drat -o proof.grat
c sizeof(cdb_t) = 4
c sizeof(cdb_t*) = 8
c Using RAT run heuristics
c Parsing formula ... 1ms
c Parsing proof (ASCII format) ... 32251ms
c Forward pass ... 2073ms
c Starting Backward pass
c Single threaded mode
0% 10 20 30 40 50 60 70 80 90 100%
|----|----|----|----|----|----|----|----|----|----|
***************************************************
c Waiting for aux-threads ...done
c Lemmas processed by threads: 2032698 mdev: 0
c Finished Backward pass: 65356ms
c Writing combined proof ... 19088ms
s VERIFIED
c Timing statistics (ms)
c Parsing: 32253
c Checking: 67465
c * bwd: 65356
c Writing: 19088
c Overall: 118808
c * vrf: 99720
c Lemma statistics
c RUP lemmas: 2032698
c RAT lemmas: 0
c RAT run heuristics: 0
c Total lemmas: 2032698
c Size statistics (bytes)
c Number of clauses: 4031493
c Clause DB size: 309680252
c Item list: 128778112
c Pivots store: 16777216
Then verify it with gratchk.
$ 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
Since 0.4.0, you can use Splr in your programs. (Here I suppose that you uses Rust 2021.)
use splr::*;
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(Certificate::UNSAT) => println!("s UNSATISFIABLE"),
Err(e) => panic!("s UNKNOWN; {}", e),
}
}The following example requires 'incremental_solver' feature. You need the following dependeny:
splr = { version = "^0.17", features = ["incremental_solver"] }Under this configuration, module splr provides some more functions:
splr::Solver::reset(&mut self)splr::Solver::add_var(&mut self)// increments the last variable numbersplr::Solver::add_clause(&mut self, vec: AsRef<[i32]>) -> Result<&mut Solver, SolverError>
You have to call reset before calling add_var, add_clause, and solve again.
By this, splr forgets everything about the previous formula, especially non-equivalent transformations by pre/inter-processors like clause subsumbtion.
So technically splr is not an incremental solver.
'add_clause' will emit an error if vec is invalid.
use splr::*;
use std::env::args;
fn main() {
let cnf = args().nth(1).expect("takes an arg");
let assigns: Vec<i32> = Vec::new();
println!("#solutions: {}", run(&cnf, &assigns));
}
#[cfg(feature = "incremental_solver")]
fn run(cnf: &str, assigns: &[i32]) -> usize {
let mut solver = Solver::try_from(cnf).expect("panic at loading a CNF");
for n in assigns.iter() {
solver.add_assignment(*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::<Vec<i32>>();
match solver.add_clause(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:
#[cfg(feature = "incremental_solver")]
for (i, v) in Solver::try_from(cnf).expect("panic").iter().enumerate() {
println!("{}-th answer: {:?}", i, v);
}sample code from my sudoku solver
let mut solver = Solver::try_from((config, rules.as_ref())).expect("panic");
for a in setting.iter() {
solver.add_assignment(*a).expect("panic");
}
for ans in solver.iter().take(1) {
let mut picked = ans.iter().filter(|l| 0 < **l).collect::<Vec<&i32>>();
for _i in 1..=range {
for _j in 1..=range {
let (_i, _j, d, _b) = Cell::decode(*picked.remove(0));
print!("{:>2} ", d);
}
println!();
}
println!();
}
}| 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 |
entg |
the current average of 'Literal Block entanglement' |
cLvl |
the EMA of decision levels at which conflicts occur |
bLvl |
the EMA of decision levels to which backjumps go |
/cpr |
the EMA of conflicts per restart |
avrg |
the EMA, Exponential Moving Average, of LBD of learnt clauses |
trnd |
the current trend of the LBD's EMA |
#RST |
the number of restarts |
/dpc |
the EMA of decisions 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 |
/ppc |
the EMA of propagations per conflict |
time |
the elapsed CPU time in seconds |
A modern CDCL SAT solver in Rust
Activated features: best phase tracking, stage-based clause elimination, stage-based clause vivification, stage-based dynamic restart threshold, Learning-Rate Based rewarding, reason-side rewarding, stage-based re-phasing, two-mode reduction, trail saving, unsafe access
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
-j, --journal Shows log about restart stages
-l, --log Uses Glucose-like progress report
-V, --version Prints version information
OPTIONS:
--cl <c-cls-lim> Soft limit of #clauses (6MC/GB) 0
--crl <cls-rdc-lbd> Clause reduction LBD threshold 5
--cr1 <cls-rdc-rm1> Clause reduction ratio for mode1 0.20
--cr2 <cls-rdc-rm2> Clause reduction ratio for mode2 0.05
--ecl <elm-cls-lim> Max #lit for clause subsume 64
--evl <elm-grw-lim> Grow limit of #cls in var elim. 0
--evo <elm-var-occ> Max #cls for var elimination 20000
-o, --dir <io-outdir> Output directory .
-p, --proof <io-pfile> DRAT Cert. filename proof.drat
-r, --result <io-rfile> Result filename/stdout
-t, --timeout <timeout> CPU time limit in sec. 5000
--vdr <vrw-dcy-rat> Var reward decay rate 0.96
ARGS:
<cnf-file> DIMACS CNF file
Splr-0.17.0 adopts the following features by default:
- Learning-rate based (LRB) var rewarding and clause rewarding[4]
- Reason-side var rewarding[4]
chronological backtrack[5]disabled since 0.12 due to incorrect UNSAT certificates.- clause vivification[6]
- Luby series based on the number of conflicts defines 'stages/cycles/segments', which are used as trigger of
- restart
- clause reduction
- in-processor (clause elimination, subsumption and vivification)
- re-configuration of var phases and var activities
- re-configuration of trail saving extended with reason refinement based on clause quality[3].
(Splr-0.15.0 and upper try to discard various dynamic and heuristic-based control schemes used in the previous versions.)
The following figure explains the flow used in the latest Splr.
I use the following terms here:
- a stage -- a span in which solver uses the same restart parameters
- a cycle -- a group of continuos spans of which the corresponding Luby values make a non-decreasing sequence
- a segment -- a group of continuos cycles which are separated by new maximum Luby values' occurrences
-
[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 LNCS, vol.7513, pp.118–126, 2012.
-
[3] R. Hickey and F. Bacchus, "Trail Saving on Backtrack", SAT 2020, LNCS, vol. 12178, pp.46-61, 2020.
-
[4] J. H. Liang, V. Ganesh, P. Poupart, and K. Czarnecki, "Learning Rate Based Branching Heuristic for SAT Solvers," in LNCS, vol.9710, pp.123–140, 2016.
-
[5] A. Nadel and V. Ryvchin, "Chronological Backtracking," in Theory and Applications of Satisfiability Testing - SAT 2018, June 2018, pp.111–121, 2018.
-
[6] C. Piette, Y. Hamadi, and L. Saïs, "Vivifying propositional clausal formulae," Front. Artif. Intell. Appl., vol.178, pp.525–529, 2008.
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-2024, Narazaki Shuji