建议一个高效的C++解决方案与良好的Z3接口(或:Z3对我有好处)？

Question

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

1. 我需要提取令人满意的赋值，而不仅仅是检查可满足性，求解者应该允许我反复求解相同的公式，寻找不同可能的满意任务，最终以有效的方式迭代所有这些任务(例如，不必添加一个子句并重新开始)。
2. 该项目仍应积极维护和公平的生产质量，而不是一些竞争获胜的研究项目放弃自出版(见picosat)。
3. 此外，由于我使用的是C++，解决程序应该提供一个高效且(可能)良好的C++接口。

我考虑的第一个候选人是Z3，但我对文档感到困惑，无法理解上面第1点是否被支持，如果考虑到我只需要SAT而不需要SMT，那么这可能是过分的。C++接口看起来也很容易使用，但是我不能忍受这样一个事实:我必须用普通字符串来命名变量(这与我周围的算法非常糟糕)。这不是可以避免的吗？)

那么，你能不能给我一些建议，用哪一个SAT解决方案，或者用一些关于Z3的疑问来说明问题？

Answer 1

如果您愿意将一些工作用于修复不同平台的构建(或者根本不需要它们)，MiniSat的界面相当不错。确实注意到它已经不再被维护了。

还有葡萄糖，它共享MiniSat的接口，并且相对主动地维护。它在SAT比赛中的表现也比MiniSat要好得多。

在选择其中一种或另一种之前，您需要理解的是，虽然葡萄糖通常在SAT竞赛中胜过MiniSat，但您的用例可能并不能解决SAT竞赛。例如，我们的项目通常会生成可满足的公式，其中的任务是找到(通常)许多SAT作业中的一个，而在那里，MiniSat的性能通常优于葡萄糖。OTOH如果你的项目产生无法满足的公式或公式与单一的解决方案，葡萄糖可能会做得更好，因为它是为快速找到UNSAT证明，而不是寻找SAT作业优化。

我有过嵌入经验的另一个解决者是CryptoMiniSat。它有一个合理的C++接口，并非常积极地维护。当我有问题或错误时，通常在一周内修复。然而，它很少提供稳定的版本，所以如果您正在使用它，您很可能会依赖特定的散列而不是适当的版本来生活。

还有一件事要注意:葡萄糖提供了一个并行的解决方案，但是有一个相当有趣的许可。CMSat提供麻省理工学院许可下的并行求解器。MiniSat有一个非常自由的许可，但根本就没有类似的选择。