Crate splr

A modern CDCL SAT solver in Rust

Splr is a pure Rustic SAT solver, based on Glucose 4.1. It adopts various research results on SAT solvers:

• CDCL, watch literals, and so on from Minisat and the ancestors
• Glucose-like dynamic blocking/forcing restarts based on EMAs
• heuristics adaptation
• pre/in-process simplification based on clause subsumption and variable elimination
• Chronological backtrack and non-chronological backjump
• Learning Rate Based Branching and Reason Side Rewarding
• Rephase
• Search stabilization
• clause vivification

Many thanks to SAT researchers.

Examples

Build a solver from a configuration based on a CNF file, then solve it.

use splr::*;
use std::path::Path;

let config = Config::from(Path::new("cnfs/sample.cnf"));
if let Ok(mut s) = Solver::build(&config) {
    if let Ok(ans) = s.solve() {
        println!("{:?}", ans);
    }
}

On-memory direct conversion from a vec to a solution

use splr::*;

let v: Vec<Vec<i32>> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]];
match Certificate::try_from(v).expect("panic!") {
    Certificate::UNSAT => 0,
    Certificate::SAT(vec) => vec.len(),
};

Incremental solver

Splr provides ‘incremental solver mode’ if you built it with feature ‘incremental_solver’. This document covers extra functions only if you built it with cargo doc --features incremental_solver.

Re-exports

• pub use config::Config;
• pub use solver::Certificate;
• pub use solver::SatSolverIF;
• pub use solver::SolveIF;
• pub use solver::Solver;
• pub use solver::ValidateIF;
• pub use types::PropertyDereference;
• pub use types::PropertyReference;
• pub use types::SolverError;
• pub use primitive::ema::*;
• pub use primitive::luby::*;

Modules

• assign
  Module assign implements Boolean Constraint Propagation and decision var selection.
• cdb
  Module cdb provides Clause object and its manager ClauseDB.
• cnf
  Module cnf provides basic operations on CNF files
• config
  Module config provides solver’s configuration and CLI.
• primitive
  Module primitive provides some fundamental data structures.
• processor
  Module processor implements a simplifier: clause subsumption and var elimination.
• solver
  Module solver provides the top-level API as a SAT solver.
• state
  Module state is a collection of internal data.
• types
  Module types provides various building blocks, including some common traits.

Constants

• VERSION
  Splr version number.