Crate splr

Expand description

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.