Crate splr[−][src]
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::*; let config = Config::from("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::*, 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::Ema;
pub use types::Ema2;
pub use types::EmaIF;
pub use types::PropertyDereference;
pub use types::PropertyReference;
pub use types::SolverError;
Modules
Crate assign
implements Boolean Constraint Propagation and decision var selection.
Crate config
provides solver’s configuration and CLI.
Crate processor
implements a simplifier: clause subsumption and var elimination.
Crate solver
provides the top-level API as a SAT solver.
Crate state
is a collection of internal data.
Crate types
provides various building blocks, including some common traits.
Constants
Splr version number.
Traits
API for SAT solver creation and modification.
API to solve
SAT problems.
API for SAT validator like inject_assignment
, validate
and so on.