c++ - 建议具有良好 C++ 接口(interface)的高效 SAT 求解器(或 : is Z3 good for me)?

Question

对于我要开始的项目，我需要使用 SAT 求解器。我以前使用过其中一些，但主要用于实验，而这里项目的主要限制是良好的性能。我正在尝试寻找替代方案，并试图了解每个替代方案如何根据我的具体要求进行定位。特别是:

1. 我需要提取令人满意的赋值，而不仅仅是检查可满足性，求解器应该允许我重复求解相同的公式以寻找不同的可能令人满意的赋值，最终迭代所有这些赋值，在一个高效的方式(例如，我不必添加一个子句并重新开始)。

2. 该项目应该仍在积极维护并且具有相当的生产质量，而不是自发布以来放弃的一些获奖研究项目(参见 picosat)。

3. 此外，由于我使用的是 C++，求解器应该提供一个高效且(可能)编写良好的 C++ 接口(interface)。

我考虑的第一个候选者是 Z3，但我对文档感到困惑，无法理解上面的第 1 点是否得到支持，以及考虑到我只需要 SAT 而不是 SMT，它是否可能有点矫枉过正。 C++ 接口(interface)似乎也很容易使用，但我无法忍受我必须用纯字符串命名变量的事实(这与我周围的算法配对非常糟糕。这不是可以避免的吗？)。

那么你能给我一些关于使用哪个 SAT 求解器的建议，或者对 Z3 的疑问给出一些启示吗？

Answer 1

如果您愿意投入一些工作来修复不同平台的构建(或者根本不需要它们)，MiniSat's interface is rather nice.请注意，它不再真正维护了。

还有Glucose , 它共享 MiniSat 的接口(interface)并且维护相对积极。它在 SAT 比赛中的表现也比 MiniSat 好很多。

在选择一个或另一个之前，您需要了解虽然 Glucose 在 SAT 比赛中通常胜过 MiniSat，但您的用例可能不是解决 SAT 比赛。例如，我们的项目通常会生成可满足的公式，其中的任务是找到(通常)许多 SAT 作业之一，而 MiniSat 通常在这些作业中优于 Glucose。 OTOH 如果您的项目主要生成无法满足的公式或只有一个解决方案的公式，Glucose 可能会做得更好，因为它针对快速查找 UNSAT 证明进行了优化，而不是查找 SAT 作业。

我有过嵌入经验的另一个求解器是 CryptoMiniSat .它有一个合理的 C++ 接口(interface)，并且得到了非常积极的维护。当我遇到问题或错误时，通常会在一周内修复。但是，它很少提供稳定版本，因此如果您使用它，您最终可能会依赖特定的哈希而不是正确的版本。

还有一点需要注意:Glucose 提供了一个并行求解器，但有一个相当有趣的许可证。 CMSat 在 MIT 许可下提供并行求解器。 MiniSat 的许可证非常宽松，但根本没有并行选项。