Crate splr[−][src]
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::Ema; |
pub use types::Ema2; |
pub use types::EmaIF; |
pub use types::PropertyDereference; |
pub use types::PropertyReference; |
pub use types::SolverError; |
Modules
assign | Crate |
cdb | |
config | Crate |
processor | Crate |
solver | Crate |
state | Crate |
types | Crate |
Constants
VERSION | Splr version number. |
Traits
SatSolverIF | API for SAT solver creation and modification. |
SolveIF | API to |
ValidateIF | API for SAT validator like |