有没有类似于WBO的Python SAT求解器？

Question

有没有一个 Python 模块/程序可以解决 SAT 问题？可能是加权布尔问题。 （具体而言，类似于 wbo 的东西）

如果没有，也许有绑定或 API 可以使用其中一个求解器。

我认为在我现在拥有的时间内自己编写一个是不可能的。

- WeGi

Answer 1

为了解决SAT问题，我建议使用MiniSat (http://minisat.se)、Glucose (https://www.lri.fr/~simon/?page=glucose)或Picosat (http://fmv.jku.at/picosat)等工具，还有其他类似的工具可供选择。在伪布尔优化方面，我知道MiniSat+ (http://minisat.se/MiniSat+.html)和Gurobi (http://www.gurobi.com)可以使用。我认为它们都是免费的，除了Gurobi提供试用和学术许可证。

它们都提供命令行接口，输入输出文件可以轻松地在Python中生成和读取。此外，Gurobi还具有完整的Python shell。

- anumi

---

另外，由于您使用Python，建议查看PuLP（http://pythonhosted.org/PuLP），这是一个用Python编写的线性规划模型。 - anumi

Answer 2

Picosat有与Python相关的绑定（pycosat）。

- Fractalic

---

开始非常简单，网上有示例（例如数独）。非常自然的子句（正整数或负整数）。我没有看到优化功能（加权软约束），但它就在那里，在pip install pycosat之后可用。 - Tomasz Gandor