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.