Crate kissat[−][src]
Expand description
A simple wrapper for the Kissat SAT solver.
Kissat is a state of the art SAT solver by Armin Biere and others. It is written in C rather than C++, unlike CaDiCaL (upon which it is based) and older solvers such as minisat and glucose. This makes it particularly nice to embed in Rust.
This crate builds the entire source code of Kissat, and provides a safe interface over it.
extern crate kissat;
fn main() {
let mut solver = kissat::Solver::new();
let a = solver.var();
let b = solver.var();
solver.add2(a, !b);
solver.add1(b);
match solver.sat() {
Some(solution) => println!("SAT: {:?} {:?}", solution.get(a), solution.get(b)),
None => println!("UNSAT"),
}
}