rsat

SAT 求解器。

目前，已实现基于 probSAT 的随机局部搜索和基于 MiniSAT 的 CDCL 求解器。更多算法将很快可用。

该项目仍在开发中。API 可能会在第一个稳定版本 v1.0.0 之前更改。

许可协议

MIT

lib.rs:

rsat 是一个 SAT 求解器。

使用 CDCL 求解器的示例

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