23 releases (10 breaking)

0.13.0 Oct 12, 2021
0.11.0 Aug 17, 2021
0.10.0 Jul 11, 2021
0.7.0 Mar 14, 2021
0.1.2 Mar 7, 2019

#17 in Math

Download history 16/week @ 2021-07-06 3/week @ 2021-07-13 26/week @ 2021-07-20 42/week @ 2021-07-27 21/week @ 2021-08-03 9/week @ 2021-08-10 45/week @ 2021-08-17 1/week @ 2021-08-24 1/week @ 2021-08-31 2/week @ 2021-09-07 2/week @ 2021-09-14 13/week @ 2021-09-21 29/week @ 2021-09-28 5/week @ 2021-10-05 45/week @ 2021-10-12 3/week @ 2021-10-19

67 downloads per month

MPL-2.0 license

470KB
11K SLoC

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

  • SAT Competition 2021, Benchmarks main truck -- splr-0.13.0 RC (8d45af74) solved with a 500 sec timeout:
    • 41 satisfiable problems: all the solutions were correct.
    • 44 unsatisfiable problems: ?? 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.

$ splr cnfs/unif-k3-r4.25-v360-c1530-S1293537826-039.cnf 
unif-k3-r4.25-v360-c1530-S1293537826-039.cnf       360,1530 |time:    36.59
 #conflict:     529230, #decision:      1056348, #propagate:       29414590
  Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000
      Clause|Remv:    40118, LBD2:      201, BinC:        0, Perm:     1521
     Restart|#BLK:        0, #RST:     4889, *scl:        2, sclM:       16
         LBD|trnd:   1.0550, avrg:  14.0262, depG:   2.9379, /dpc:     1.14
    Conflict|tASG:   0.9417, cLvl:    17.96, bLvl:    16.81, /ppc:    61.97
        misc|vivC:      181, subC:        0, core:      160, /cpr:   200.70
      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.13.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:     529230, #decision:      1056348, #propagate:       29414590,
c   Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000,
c       Clause|Remv:    40118, LBD2:      201, BinC:        0, Perm:     1521,
c      Restart|#BLK:        0, #RST:     4889, *scl:        2, sclM:       16,
c          LBD|avrg:  14.0262, trnd:   1.0550, depG:   2.9379, /dpc:     1.14,
c     Conflict|tASG:   0.9417, cLvl:    17.96, bLvl:    16.81, /ppc:    61.97,
c         misc|vivC:       42, subC:        0, core:      160, /cpr:   200.70,
c     Strategy|mode:  generic, time:    36.59,
c 
c   config::ChronoBtThreshold                      100.000
c   config::ClauseRewardDecayRate                    0.950
c   config::InprocessorInterval                  10000.000
c   config::RestartAsgThreshold                      0.600
c   config::RestartLbdThreshold                      1.600
c   config::VarRewardDecayRate                       0.960
c   assign::NumConflict                         529230
c   assign::NumDecision                        1056348
c   assign::NumPropagation                    29414590
c   assign::NumRephase                              31
c   assign::NumRestart                            4890
c   assign::NumVar                                 360
c   assign::NumAssertedVar                           0
c   assign::NumEliminatedVar                         9
c   assign::NumReconflict                           36
c   assign::NumRepropagation                    137945
c   assign::NumUnassertedVar                       351
c   assign::NumUnassignedVar                       351
c   assign::NumUnreachableVar                        0
c   assign::RootLevel                                0
c   assign::DecisionPerConflict                      1.137
c   assign::PropagationPerConflict                  61.971
c   assign::ConflictPerRestart                     218.774
c   assign::ConflictPerBaseRestart                 218.774
c   assign::BestPhaseDivergenceRate                  0.000
c   clause::NumBiClause                              0
c   clause::NumBiClauseCompletion                    0
c   clause::NumBiLearnt                              0
c   clause::NumClause                            41639
c   clause::NumLBD2                                201
c   clause::NumLearnt                            40118
c   clause::NumReduction                            40
c   clause::NumReRegistration                        0
c   clause::Timestamp                           529230
c   clause::DpAverageLBD                             2.938
c   processor::NumFullElimination                   42
c   processor::NumSubsumedClause                     0
c   restart::NumBlock                                0
c   restart::NumCycle                                4
c   restart::NumRestart                           4890
c   restart::NumStage                               40
c   restart::IntervalScale                           2
c   restart::IntervalScaleMax                       16
c   state::NumDecisionConflict                  263195
c   state::NumProcessor                             41
c   state::Vivification                             41
c   state::VivifiedClause                          181
c   state::VivifiedVar                               0
c   state::BackjumpLevel                            16.810
c   state::ConflictLevel                            17.962
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.

$ splr -c cnfs/unif-k3-r4.25-v360-c1530-S1028159446-096.cnf
unif-k3-r4.25-v360-c1530-S1028159446-096.cnf       360,1530 |time:   188.78
 #conflict:    1878094, #decision:      3632102, #propagate:       95497554
  Assignment|#rem:      346, #fix:        6, #elm:        8, prg%:   3.8889
      Clause|Remv:    22937, LBD2:      618, BinC:       97, Perm:     1500
     Restart|#BLK:        0, #RST:    11799, *scl:        8, sclM:       32
         LBD|trnd:   0.2960, avrg:   2.2538, depG:   2.4044, /dpc:     1.03
    Conflict|tASG:   1.0390, cLvl:     8.63, bLvl:     7.51, /ppc:    48.37
        misc|vivC:     1008, subC:        0, core:      346, /cpr:   178.13
      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 1588714 of 1889628 lemmas in core using 54190641 resolution steps
c 0 RAT lemmas in core; 808781 redundant literals in core lemmas
s VERIFIED
c verification time: 100.177 seconds

B: Verify with gratchk

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) ... 16602ms
c Forward pass ... 3092ms
c Starting Backward pass
c Single threaded mode
c Waiting for aux-threads ...done
c Lemmas processed by threads: 1587582 mdev: 0
c Finished Backward pass: 65581ms
c Writing combined proof ... 16102ms
s VERIFIED
c Timing statistics (ms)
c Parsing:  16604
c Checking: 68699
c   * bwd:  65581
c Writing:  16102
c Overall:  101411
c   * vrf:  85308

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

c Size statistics (bytes)
c Number of clauses: 1891157
c Clause DB size:  144045664
c Item list:       60101264
c Pivots store:    8388608

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

Calling Splr from Rust programs

Since 0.4.0, you can use Splr in your programs.

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

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),
    }
}

All solutions SAT solver

use splr::*;
use std::{convert::TryFrom, 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);
}

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

$ 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] <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 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 <c-cbt-thr>     Dec. lvl to use chronoBT              100
      --cdr <crw-dcy-rat>   Clause reward decay rate                0.95
      --cl <c-cls-lim>      Soft limit of #clauses (6MC/GB)         0
      --ii <c-ip-int>       #cls to start in-processor          10000
  -t, --timeout <timeout>   CPU time limit in sec.               5000
      --ecl <elm-cls-lim>   Max #lit for clause subsume            18
      --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                       
      --ral <rst-asg-len>   Length of assign. fast EMA             24
      --ras <rst-asg-slw>   Length of assign. slow EMA           8192
      --rat <rst-asg-thr>   Blocking restart threshold              0.60
      --rll <rst-lbd-len>   Length of LBD fast EMA                  8
      --rls <rst-lbd-slw>   Length of LBD slow EMA               8192
      --rlt <rst-lbd-thr>   Forcing restart threshold               1.60
      --rs  <rst-step>      #conflicts between restarts             2
      --srd <stg-rwd-dcy>   Decay rate for staged var reward        0.50
      --srv <stg-rwd-val>   Extra reward for staged vars            1.00
      --vdr <vrw-dcy-rat>   Var reward decay rate                   0.94
      --vds <vrw-dcy-stp>   Var reward decay change step            0.10
ARGS:
  <cnf-file>    DIMACS CNF file

Solver description

Splr-0.13.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]
  • 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
  • trail saving extended with reason refinement based on clause quality[3]

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

search algorithm in Splr 0.12

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

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

Dependencies