建议一个有效的SAT求解器具有良好的C++接口(或者:Z3对我有用)？

Question

对于我正在开始的项目,我将需要使用SAT求解器.我之前使用过其中一些但主要用于实验,而这里项目的主要约束是良好的性能.我正在尝试寻找替代方案,并尝试了解每种方案如何根据我的具体要求定位.特别是:

1. 我需要提取令人满意的任务,不仅要检查是否满足,而且解算器应该允许我重复求解相同的公式,寻找不同的可能令人满意的任务,最终以有效的方式迭代所有这些,(例如,没有我)必须添加一个条款并重新开始).

2. 该项目应该仍然是积极维护和相当的生产质量,而不是自出版以来放弃的一些竞争获胜的研究项目(见picosat).

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

我考虑的第一个候选人是Z3,但我对文档感到困惑,如果上面的第1点得到支持则无法理解,如果我只需要SAT而不是SMT就可能有点过分.C++界面似乎也很容易使用,但我无法忍受这样一个事实:我必须使用普通字符串命名变量(这与我周围的算法配对非常糟糕.这是不是可以避免？).

那么你能否给我一些关于哪个SAT求解器使用的建议,或者对Z3的怀疑有所启发？

Answer 1

如果您愿意投入一些工作来修复不同平台的构建（或者根本不需要它们），MiniSat 的界面相当不错。请注意，它不再被真正维护。

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

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

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

还有一件事需要注意：Glucose 提供了一个并行求解器，但具有相当有趣的许可证。CMSat 在 MIT 许可下提供并行求解器。MiniSat 拥有非常自由的许可，但根本没有平行选项。