SMT SolverであるZ3でお絵かきロジックソルバを書きました。練習です。

コードはこちら。

罠が何箇所かありました。まず、Z3 python bindingで多次元配列を作る方法がわからなかったので、１次元配列の添字を適当にスキップさせて二次元の図形用変数を作りました。これは自明。

解答を作ったあと、それを表示しようとしてハマりました。結果の配列をprintするとTrueやFalseが正しく出てくるのですが、それをアスキーアートに変えようとすると全てTrueになってしまいます。原因は以下のとおり。

>>> import z3
>>> q = z3.Bool('q')
>>> s = z3.Solver()
>>> s.add(z3.Not(q))
>>> s.check()
sat
>>> m = s.model()
>>> m
[q = False]
>>> m.eval(q)
False
>>> not m.eval(q)
False
>>> help(m.eval(q))
Help on instance of BoolRef in module z3:

class BoolRef(ExprRef)

つまりm.eval(q)の返り値はBoolRefであってBoolではなく、FalseなBoolRefはpythonの真偽値としてはTrueを持つのでした。

ちなみに効率ですが、10x10の人手で解けるパズルを解くのに8秒とかかかります。ちょっとつらい。2^100の探索よりは圧倒的に速いですが、そもそも人手で解くことが可能なパズルならばもっと高速で解けて欲しいところです。不適切なツールだったということでFA。

それからz3で一般に困りそうなところ。そういえば数年前のICFPCでも困りました。

  • シングルプロセス
  • 遅い時に高速化をどうすればいいかわからない。