rsat

SAT Solver.

Currently, a stochastic local search based on probSAT and a CDCL solver based on MiniSAT has been implemented. More algorithms will be available soon.

This projetct is still in development. The APIs can change before the first stable release v1.0.0.

License

MIT

lib.rs:

rsat is a SAT Solver.

An example using the CDCL solver

use rsat::cdcl::{Solver, SolverOptions};
use solhop_types::{Var, Solution};

let options = SolverOptions::default();
let mut solver = Solver::new(options);
let vars: Vec<Var> = solver.new_vars(3);
solver.add_clause(vec![vars[0].pos_lit()]);
solver.add_clause(vec![vars[1].neg_lit()]);
solver.add_clause(vec![vars[0].neg_lit(), vars[1].pos_lit(), vars[2].pos_lit()]);

assert_eq!(solver.solve(vec![]), Solution::Sat(vec![true, false, true]));

assert_eq!(solver.solve(vec![vars[2].neg_lit()]), Solution::Unsat);

assert_eq!(solver.solve(vec![]), Solution::Sat(vec![true, false, true]));

solver.add_clause(vec![vars[2].neg_lit()]);
assert_eq!(solver.solve(vec![]), Solution::Unsat);