[][src]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::*;

let config = Config::from("tests/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::*, std::convert::TryFrom};

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::Solver;
pub use types::SolverError;

Modules

assign

Crate assign implements Boolean Constraint Propagation and decision var selection.

cdb

Crate cdb provides Clause object and its manager ClauseDB.

config

Crate config provides solver's configuration and CLI.

processor

Crate processor implements a simplifier: clause subsumption and var elimination.

solver

Crate solver provides the top-level API as a SAT solver.

state

Crate state is a collection of internal data.

types

Crate types provides various building blocks, including some common traits.

Constants

VERSION

Splr version number.

Traits

SatSolverIF

API for SAT solver creation and modification.

SolveIF

API to solve SAT problems.

ValidateIF

API for SAT validator like inject_assignment, validate and so on.