rustsat - Rust 的全面 SAT 库

rustsat 是一个用于在 Rust 中处理布尔可满足性问题的一组接口和工具。本库旨在为可满足性问题解决领域的软件开发提供常用元素的实现。该库的焦点是提供尽可能方便的使用方式，同时不牺牲性能。

示例

let mut instance: SatInstance = SatInstance::new();
let l1 = instance.new_lit();
let l2 = instance.new_lit();
instance.add_binary(l1, l2);
instance.add_binary(!l1, l2);
instance.add_unit(l1);
let mut solver = rustsat_minisat::core::Minisat::default();
solver.add_cnf(instance.as_cnf().0).unwrap();
let res = solver.solve().unwrap();
assert_eq!(res, SolverResult::Sat);
let sol = solver.full_solution().unwrap();
assert_eq!(sol[l1.var()], TernaryVal::True);
assert_eq!(sol[l2.var()], TernaryVal::True);

crate

RustSAT 项目分为多个 crate，它们都包含在 这个仓库 中。以下是该项目包含的 crate：

安装

要将RustSAT库作为项目依赖项使用，只需运行以下命令：cargo add rustsat。要在项目中使用SAT求解器接口，请运行以下命令：cargo add rustsat-<satsolver>。通常，可以通过crate功能选择SAT求解器的版本，有关详细信息，请参阅相应SAT求解器crate的文档。