【发布时间】：2013-02-28 03:02:18
【问题描述】：
【问题讨论】：
标签： python computer-science solver
【发布时间】：2013-02-28 03:02:18
【问题描述】：
为了解决 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。
【讨论】：
-
另外，由于您使用的是 Python，请查看 PuLP (pythonhosted.org/PuLP)，这是一个用 Python 编写的 LP 建模器。
Picosat 具有 Python 绑定 (pycosat)
【讨论】：
-
上手超级简单，并且在网络上有示例（例如数独）。非常自然的子句（正整数或负整数）。我没有看到优化功能（加权软约束），但它就在那里，在
pip install pycosat之后可用。