5

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

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

  2. 该项目应该仍然得到积极维护和相当的生产质量，而不是自出版以来放弃的一些赢得竞争的研究项目（见picosat）。

  3. 此外，由于我使用的是 C++，所以求解器应该提供一个高效且（可能）良好的书面 C++ 接口。

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

那么你能给我一些关于使用哪个 SAT 求解器的建议，或者通过对 Z3 的疑问来阐明一些观点吗？

4

1 回答 1

1

如果您愿意为不同平台修复构建（或根本不需要它们），MiniSat 的界面相当不错。请注意，它不再真正被维护了。

还有Glucose，它共享 MiniSat 的界面并且维护得比较积极。它在 SAT 比赛中的表现也比 MiniSat 好很多。

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

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

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

于 2017-10-13T09:45:27.973 回答