PythonでSATを使いたい

調べた

http://minisat.se/MiniSat.html

$ port search minisat
minisat @2.2.0 (math, science)
    Minimalistic SAT solver
port search minisat  1.85s user 0.13s system 90% cpu 2.178 total

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

https://github.com/shtaxxx/pyminisat 短い

SAT ソルバで数独を解く方法 - まめめも

乗法標準形 - Wikipediaのおさらい。

今回 「(x and y and z)ではない、かつ(~x and ~y and ~z)ではない」がandで固まっている問題だから、ド・モルガンで(~x or ~y or ~z) かつ (x or y or z)に変形すればいいんだよな。で、このorの塊をタプルにしてつっこんでいけばいい、と。

solver = minisat.SatSolver()
vars = {}
for x in RANGE:
    for y in RANGE:
        vars[(x, y)] = minisat.SatVar()

for baika in baika_list:
    solver.append(tuple(vars[p] for p in baika))
    solver.append(tuple(-vars[p] for p in baika))

def to_xo(x):
    if x < 0: return 'x'
    if x > 0: return 'o'
    raise AssertionError

solver.solve(dump=False)
print "\n".join(" ".join(
        to_xo(solver[vars[(x, y)]]) for x in RANGE) for y in RANGE)

"""
x x o x x
o x x x x
x x x o x
x o x x x
x x x o o
"""

できたできた

o x o o x o x x o x o x x o x
x x o o x x x x x x o o x x o
o o x o x o o o x o o x o x x
o x o o o x o x o o o x x x x
x x x x x x o o o x o x o o o
x o x x o x o o x o o o x o x
x o o x x o o x x x x x x o o
o o x o x x o x o x x o x o o
o o x x x x x x o o x x o o x
x o x o o o x o o x o x x o x
o o o x o x o o o x x x x x x
x x x x o o o x o x o o o x o
x x o x o o x o o o x o x o o
o x x o o x x x x x x o o o x
x o x x o o o x x o x o o x o
python ex2.py  189.17s user 1.08s system 94% cpu 3:20.40 total

17路の結果が中々出ない。でもCNFを作成する所で詰まっているわけではないからSATソルバを使うためにCNFを作る - soutaroにっきとか使う話ではないだろうなぁ。

特集「最近のSAT技術の発展」