MiniSatのPythonラッパーを書いてみた

SAT(充足可能問題)を解く必要があったので，高速なSATソルバーのMiniSatをPythonから触るラッパーを書いてみた．

ダウンロード

githubにあげてあります．shtaxxx:pyminisat

使い方

SatSolver()がソルバーでSatVarが変数．
SatSolver.append()で節を追加していく．
最後にSatSolver.solve()を呼び出してSATを解く．

from minisat import *
solver = SatSolver()
a = SatVar()
b = SatVar()
solver.append((-a, -b))
solver.append((-a, b))
solver.append((a, -b))
#solver.append((a, b))
satisfy = solver.solve()

solver.view()
if satisfy:
    print(solver[a], solver[b], solver[c])

その他

APIはruby版のラッパーを参考にさせて頂きました．

追記 (2013年1月13日)

• Python3にも対応
• SatSolver.solve()がSATがSatisfiableかどうかを返すように変更
• SatSolver.view()を追加