splr 0.6.1

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:

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

• all the certifications of UUF250 were correct and verified with Grad.
• SAT Race 2019, Benchmarks -- splr-0.6.0 RC() solved with a 300 sec (soft) timeout:
  • 45 (20201226), 42 (eab832c), and 38 (0.6.0) satisfiable problems: all the solutions were correct.
  • 6 (20201226), 4 (eab832c), and 4 (0.6.0) unsatisfiable problems: all the certifications were verified with Grad.

Install

Just run cargo install splr --features cli 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.

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 tests/uf250-02.cnf 
[       512] Lcycle:     1, core:      135, #ion:         6, /cpr:   256.00
[      1792] Lcycle:     2, core:      132, #ion:         3, /cpr:   358.40
[      6144] Lcycle:     3, core:      114, #ion:         1, /cpr:   512.00
uf250-02.cnf                                       250,1065 |time:     0.12
 #conflict:       6286, #decision:         7133, #propagate:         267271
  Assignment|#rem:      244, #ass:        0, #elm:        6, prg%:   2.4000
      Clause|Remv:     5737, LBD2:       26, Binc:        0, Perm:     1061
   Stabilize|#BLK:       19, #RST:       13, #ion:        1, Lspn:        1
         EMA|tLBD:  18.3107, tASG:   4.4215, core:        0, /dpc:     1.13
    Conflict|eLBD:    13.25, cnfl:    11.62, bjmp:    10.88, /ppc:    42.52
        misc|elim:        1, cviv:        0, #vbv:        0, /cpr:   483.54
      Result|file: ./.ans_uf250-02.cnf
s SATISFIABLE: tests/uf250-02.cnf

$ cat .ans_uf250-02.cnf
c This file was generated by splr-0.6.0 for tests/uf250-02.cnf
c 
c CNF file(uf250-02.cnf), #var:      250, #cls:     1065
c  #conflict:       6286, #decision:         7133, #propagate:         267271,
c   Assignment|#rem:      244, #fix:        0, #elm:        6, prg%:   2.4000,
c       Clause|Remv:     5737, LBD2:       26, Binc:        0, Perm:     1061,
c      Restart|#BLK:       19, #RST:       13, #ion:        1, Lcyc:        3,
c          EMA|tLBD:  18.3107, tASG:   4.4215, core:        0, /dpc:     1.13,
c     Conflict|eLBD:    13.25, cnfl:    11.62, bjmp:    10.88, /ppc:    42.52,
c         misc|elim:        1, cviv:        0, #vbv:        0, /cpr:   483.54,
c     Strategy|mode:  generic, time:     0.12,
c 
s SATISFIABLE
v -1 -2 -3 4 5 6 7 -8 9 10 11 12 -13 14 -15 16 -17 -18 19 -20 ... -250 0

$ dmcr tests/uf250-02.cnf
A valid assignment set for tests/uf250-02.cnf is found in .ans_uf250-02.cnf

If you want to certificate unsatisfiability, use splr --certificate and recommend to use Grid.

1. Run splr with certificate option.

$ splr -c tests/unsat.cnf
unsat.cnf                                            83,570 |time:     0.00
 #conflict:          0, #decision:            0, #propagate:              0
  Assignment|#rem:       19, #ass:       64, #elm:        0, prg%:  77.1084
      Clause|Remv:        0, LBD2:        0, Binc:      126, Perm:      135
     Restart|#BLK:        0, #RST:        0, #ion:        0, Lspn:        1
         EMA|tLBD:      NaN, tASG:      NaN, core:       83, /dpc:      NaN
    Conflict|eLBD:     0.00, cnfl:     0.00, bjmp:     0.00, /ppc:      NaN
        misc|elim:        1, cviv:        0, #vbv:        0, /cpr:      NaN
      Result|file: ./.ans_unsat.cnf
 Certificate|file: proof.out
s UNSATISFIABLE: tests/unsat.cnf

2. Trim comments from the output

$ egrep -v '^[cs]' < proof.out > proof.drat

3. Convert the drat file to a grat file.

$ gratgen tests/unsat.cnf proof.drat -o proof.grat
c sizeof(cdb_t) = 4
c sizeof(cdb_t*) = 8
c Using RAT run heuristics
c Parsing formula ... 0ms
c Parsing proof (ASCII format) ... 1ms
c Forward pass ... 0ms
c Starting Backward pass
c Single threaded mode
c Waiting for aux-threads ...done
c Lemmas processed by threads: 0 mdev: nan
c Finished Backward pass: 0ms
c Writing combined proof ... 0ms
s VERIFIED
c Timing statistics (ms)
c Parsing:  1
c Checking: 0
c   * bwd:  0
c Writing:  0
c Overall:  2
c   * vrf:  2

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

c Size statistics (bytes)
c Number of clauses: 1110
c Clause DB size:  27612
c Item list:       23840
c Pivots store:    8192

4. Verify it with gratchk

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

Please check the help message.

• The 'switch' in help message below is either '1' or '0' to or not to use a module.
• Splr can't handle compressed CNF files so far.

$ splr --help
splr 0.6.0
A modern CDCL SAT solver in Rust

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
  -l, --log                Uses Glucose-like progress report
  -V, --version            Prints version information
OPTIONS (green options depends on compile-time flags):
OPTIONS (red options depend on features in Cargo.toml):
      --ADP <a-adaptive>   Strategy adaptation switch              0
      --ELI <a-elim>       Eliminator switch                       1
      --LBY <a-luby>       Use Luby series for restart             0
      --RDC <a-reduce>     Clause reduction switch                 1
      --RPH <a-rephase>    Re-phase switch                         1
      --RSR <a-rsr>        Reason-Side Rewarding switch            1
      --STB <a-stabilize>  Stabilization switch                    1
      --STG <a-stage>      Stage switch                            1
      --VIV <a-vivify>     Vivification switch                     0
      --cbt <c-cbt-thr>    Dec. lvl to use chronoBT              100
      --cl <c-cls-lim>     Soft limit of #clauses (6MC/GB)         0
      --ii <c-ip-int>      #cls to start in-processor          10000
  -t, --timeout <c-tout>   CPU time limit in sec.               5000
      --ecl <elm-cls-lim>  Max #lit for clause subsume            32
      --evl <elm-grw-lim>  Grow limit of #cls in var elim.         0
      --evo <elm-var-occ>  Max #cls for var elimination         8192
  -o, --dir <io-odir>      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             32
      --ras <rst-asg-slw>  Length of assign. slow EMA          10000
      --rat <rst-asg-thr>  Blocking restart threshold              0.10
      --rct <rst-ccc-thr>  Conflict Correlation threshold          0.00
      --rll <rst-lbd-len>  Length of LBD fast EMA                 32
      --rls <rst-lbd-slw>  Length of LBD slow EMA               8192
      --rlt <rst-lbd-thr>  Forcing restart threshold               1.20
      --rms <rst-mld-scl>  Scaling for Max LBD of Dep.             0.00
      --rmt <rst-mld-thr>  Threshold for Max LBD of Dep.           0.00
      --rss <rst-stb-scl>  Stabilizer scaling                      2.00
      --rs  <rst-step>     #conflicts between restarts            24
      --srd <stg-rwd-dcy>  Decay rate for staged vare reward       0.50
      --srv <stg-rwd-val>  Extra reward for staged vars            1.00
      --vit <viv-thr>      #clause to try to vivify              200
      --vri <vrw-dcy-beg>  Initial var reward decay                0.00
      --vrm <vrw-dcy-end>  Maximum var reward decay                0.00
      --vro <vrw-occ-cmp>  Occ. compression rate in LR             0.00
ARGS:
  <cnf-file>    DIMACS CNF file

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