13 releases

0.1.12 Oct 18, 2020
0.1.11 Jun 5, 2020
0.1.10 May 25, 2020
0.1.7 Nov 22, 2019
0.1.4 Sep 29, 2019

#27 in #satisfiability

42 downloads per month
Used in 3 crates

MIT license

45KB
1K SLoC

rsat

SAT Solver.

Crates.io Crates.io Crates.io Docs

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);

Dependencies

~5MB
~88K SLoC