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 短い
乗法標準形 - 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にっきとか使う話ではないだろうなぁ。