Python是否有類似wbo的SAT求解器？

有沒有一個Python模塊/程序，解決SAT問題？可能是一個加權布爾值。（具體而言，如wbo）Python是否有類似wbo的SAT求解器？

或者，如果沒有，可能是綁定或API來使用其中一個解算器。

我不認爲我現在可以自己編寫一個程序。

2013-03-12 WeGi

爲了解決SAT問題，我建議使用MiniSat（http://minisat.se），葡萄糖（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外殼。

2013-03-21 18:37:26 anumi

此外綁定，因爲你使用Python的工作，看看紙漿（http://pythonhosted.org/PuLP），用Python編寫的LP建模。 – anumi 2013-03-26 07:40:35

Picosat有蟒蛇（pycosat）

2014-10-11 18:55:27 Hyperflame

開始時非常簡單，並且在網絡上有例子（例如數獨）。非常自然的條款（正面或負面整數）。我沒有看到優化功能（加權軟約束），但它正好在'pip install pycosat'後可用。 – 2018-02-26 22:03:46

回答