具有良好C 接口的有效SAT求解器的建议(OR:Z3对我有益）

Suggestion of an efficient SAT solver with good C++ interface (or: is Z3 good for me)?

本文关键字：OR Z3 接口 有效 SAT      更新时间：2023-10-16

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

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

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

  3. 此外，由于我使用的是C ，因此求解器应提供有效的（可能是）良好的书面C 接口。

我考虑的第一个候选人是Z3，但是我对文档感到困惑，不明白是否支持上述点1。C 接口似乎也很容易使用，但是我无法忍受一个事实，我必须用普通字符串命名变量（与周围的算法非常糟糕。

那么，您能给我一些建议使用哪个sat求解器，或者对Z3的疑问？

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

也有葡萄糖，它共享了Minisat的界面，并相对维护。它在SAT比赛中的表现也比Minisat好得多。

在选择一个或另一个之前，您需要了解的是，尽管葡萄糖通常在SAT比赛中赢得Minisat，但您的用例可能无法解决SAT比赛。例如，我们的项目通常会产生令人满意的公式，其中任务是在其中找到一个（通常）的许多SAT作业，而迷你仪通常在此处优于葡萄糖。OTOH如果您的项目主要生成不满意的公式或使用单个解决方案的公式，则葡萄糖可能会更好，因为它已被优化，可快速找到Unsat证明，而不是找到SAT作业。

。

我曾经有一个嵌入经验的求解器是cryptominisat。它具有合理的C 接口，并且非常积极地维护。当我有问题或错误时，通常是在一周内修复的。但是，它很少提供稳定的发行版，因此，如果您使用它，您可能最终会依靠特定的哈希（Hash）而不是适当的版本。

还有一件事要注意：葡萄糖提供了平行的求解器，但具有相当有趣的许可。CMSAT根据MIT许可提供并行求解器。Minisat具有非常自由的许可证，但根本没有平行的选择。

相关文章：