[−][src]Crate rsat
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);
Modules
cdcl | CDCL solver module. |
sls | Stochastic local search solver module. |