Kissat SAT 求解器

这是一个独立的 crate，包含 Kissat SAT 求解器的 C 源代码及其 Rust 绑定。C 文件在构建过程中进行编译和静态链接。

Kissat 变体在 2022 年 SAT 竞赛的比赛中占据了主导地位。作者 Armin Biere 如下描述 Kissat：

Kissat 是一个用 C 编写的“保持简单和干净的裸金属 SAT 求解器”。它是将 CaDiCaL 返回 C 语言的端口，具有改进的数据结构、更好的处理调度和优化的算法和实现。巧合的是，“kissat”在芬兰语中也意味着“猫”。

此 crate 基于“cadical”crate，尽可能与 API 兼容。这使得可以作为一种调试策略切换回 cadical::Solver（它具有文件 I/O 等额外功能）。请注意：这也意味着 API 将允许您在解决问题后尝试修改问题，但 Kissat 将终止。增量求解尚未实现。

文本是未包装的正负整数，与 DIMACS 格式完全相同。常见的 IPASIR 操作以安全的 Rust 接口呈现。

let mut sat: cat_solver::Solver::new();
sat.add_clause([1, 2]);
sat.add_clause([-1, 2]);
assert_eq!(sat.solve(), Some(true));
assert_eq!(sat.value(2), Some(true));