splr 0.10.0

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 SAT solvers:

• CDCL, watch literals, LBD and so on from Glucose, Minisat and the ancestors
• Glucose-like dynamic blocking/forcing restarts based on EMAs
• pre/in-process simplification based on clause subsumption and variable elimination
• compile-time selection of a variant of Learning Rate Based Branching with Reason Side Rewarding and EVSIDS
• chronological backtrack aka chronoBT
• Glucose-like heuristics adaptation
• CaDiCaL-like extended phase saving
• a variant of CaDiCaL-like search stabilization
• clause vivification by {pre,in}-processor

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

Version 0.10.0 fixes some critical bugs.

• all the certifications of UUF250 were correct and verified with Grad.
• SAT Race 2019, Benchmarks -- splr-0.10.0 RC (5417d8bb) solved with a 200 sec timeout:
  • 30 satisfiable problems: all the solutions were correct.
  • 2 unsatisfiable problems: all the certifications were verified with Grad.

• The UNSAT certifications for aes_equiv_encry_3_rounds.debugged-sc2012.cnf, which was used in SAT Race 2019, were verified three times. Solving this problem by Splr took over 4 hours and the average drat file size was about 20 GB.

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

unif-k3-r4.25-v360-c1530-S1293537826-039.cnf       360,1530 |time:   138.82
 #conflict:    1367051, #decision:      1980153, #propagate:       73900974
  Assignment|#rem:      351, #ass:        0, #elm:        9, prg%:   2.5000
      Clause|Remv:   109225, LBD2:      367, Binc:        0, Perm:     1521
     Restart|#BLK:        0, #RST:     9747, trgr:        4, peak:       64
         LBD|avrg:   9.7604, trnd:   0.8732, depG:   2.9081, /dpc:     1.17
    Conflict|tASG:   1.0163, cLvl:    13.33, bLvl:    12.17, /ppc:    55.67
        misc|proc:       41, #sub:        0, core:        0, /cpr:   130.31
      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.10.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:    1367051, #decision:      1980153, #propagate:       73900974,
c   Assignment|#rem:      351, #fix:        0, #elm:        9, prg%:   2.5000,
c       Clause|Remv:   109225, LBD2:      367, Binc:        0, Perm:     1521,
c      Restart|#BLK:        0, #RST:     9747, trgr:        4, peak:       64,
c          LBD|avrg:   9.7604, trnd:   0.8732, depG:   2.9081, /dpc:     1.17,
c     Conflict|tASG:   1.0163, cLvl:    13.33, bLvl:    12.17, /ppc:    55.67,
c         misc|elim:       42, #sub:        0, core:        0, /cpr:   130.31,
c     Strategy|mode:  generic, time:   138.83,
c
c   config::ChronoBtThreshold                      100
c   config::ClauseRewardDecayRate                 0.95
c   config::InprocessorInterval                  10000
c   config::RestartAsgThreshold                   0.75
c   config::RestartLbdThreshold                    1.1
c   config::VarRewardDecayRate                    0.94
c   assign::NumConflict                        1367051
c   assign::NumDecision                        1980153
c   assign::NumPropagation                    73900974
c   assign::NumRephase                             136
c   assign::NumRestart                            9748
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.165
c   assign::PropagationPerConflict                  55.667
c   assign::ConflictPerRestart                     146.001
c   assign::BestPhaseDivergenceRate                  0.222
c   clause::NumBiClause                              0
c   clause::NumBiClauseCompletion                    0
c   clause::NumBiLearnt                              0
c   clause::NumClause                           110746
c   clause::NumLBD2                                367
c   clause::NumLearnt                           109225
c   clause::NumReduction                            40
c   clause::NumReRegistration                        0
c   clause::Timestamp                          1367051
c   clause::DpAverageLBD                             2.908
c   processor::NumFullElimination                   42
c   processor::NumSatElimination                     0
c   processor::NumSubsumedClause                     0
c   restart::NumBlock                                0
c   restart::NumCycle                                6
c   restart::NumRestart                           9748
c   restart::NumStage                              196
c   restart::TriggerLevel                            4
c   restart::TriggerLevelMax                        64
c   state::NumDecisionConflict                  686390
c   state::NumProcessor                             41
c   state::Vivification                             41
c   state::VivifiedClause                            1
c   state::VivifiedVar                               0
c   state::BackjumpLevel                            12.169
c   state::ConflictLevel                            13.334
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 splr --certificate and recommend to use Grid.

1. Run splr with 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:   217.38
 #conflict:    1999919, #decision:      2715863, #propagate:      101290756
  Assignment|#rem:      350, #ass:        2, #elm:        8, prg%:   2.7778
      Clause|Remv:   139189, LBD2:      592, Binc:      129, Perm:     1607
     Restart|#BLK:        0, #RST:    14891, trgr:        1, peak:      128
         LBD|avrg:   2.8599, trnd:   0.4103, depG:   2.2983, /dpc:     1.11
    Conflict|tASG:   1.0172, cLvl:     7.66, bLvl:     6.51, /ppc:    45.74
        misc|proc:       46, #sub:        0, core:      350, /cpr:   135.49
      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

2. 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) ... 16551ms
c Forward pass ... 5908ms
c Starting Backward pass
c Single threaded mode
c Waiting for aux-threads ...done
c Lemmas processed by threads: 1783765 mdev: 0
c Finished Backward pass: 93551ms
c Writing combined proof ... 17539ms
s VERIFIED
c Timing statistics (ms)
c Parsing:  16553
c Checking: 99485
c   * bwd:  93551
c Writing:  17539
c Overall:  133596
c   * vrf:  116057

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

c Size statistics (bytes)
c Number of clauses: 2008719
c Clause DB size:  146104372
c Item list:       62001536
c Pivots store:    8388608

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

Command line options

$ 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] <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          16384
  -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.out
  -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.75
      --rll <rst-lbd-len>   Length of LBD fast EMA                 24
      --rls <rst-lbd-slw>   Length of LBD slow EMA               8192
      --rlt <rst-lbd-thr>   Forcing restart threshold               1.10
      --rs  <rst-step>      #conflicts between restarts            24
      --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.10.0 adopts the following feature by default:

• Learning-rate based var rewarding and clause rewarding
• Reason-side var rewarding
• dynamic restart blocking based on the number of remaining vars
• dynamic restart based on average LBDs of learnt clauses
• clause elimination and subsumption as pre-processor and in-processor
• stabilization based on Luby series, or LubyStabilization
• chronological backtrack and non-chronological backtrack
• clause vivification
• re-phase the best phases

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.

• 'cycle' is a segment of stages, which is separated by highest Luby values.
• trigger_level N of stage n = Luby(n)
• length_of_stage n = (2 * max(Luby[1, n]) ) / n

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