z3を使ってパズルを解く

Microsoft Researchの開発したSMT(Satisfiability modulo theories)を使ってパズルを解くことを試みる. パズルを計算機を使って解くのはプログラムの例題として,

覆面算を解く

覆面算は数字を文字に置き換えて,対応を当てるパズルである.

s e n d
+ m o r e
m o n e y

まずは,z3というモジュールに含まれる定義を使うことを宣言する.

In [1]:
from z3 import * 

記述をシンプルにするためにこのようにしたが,名前空間 (name space) をシンプルにすることを意図するなら, import z3 とした上で,z3.Var('x') などと記述することができる.

準備

solverを作る.

In [2]:
solver = Solver()

これで,ソルバが作られる.

変数を作る

解くパズルは「変数」と「制約」で表現する. 「変数」としては,出てくるアルファベットを作る.

In [6]:
allvars = [s, e, n, d, m, o, r, y] = Ints('s e n d m o r y')

制約を書く

まずrowsの要素は0以上9以下である.それを書く

In [10]:
for var in allvars:
    solver.add(0 <= var, var <= 9)
In [11]:
solver
Out[11]:
[s >= 0,
 s <= 9,
 e >= 0,
 e <= 9,
 n >= 0,
 n <= 9,
 d >= 0,
 d <= 9,
 m >= 0,
 m <= 9,
 o >= 0,
 o <= 9,
 r >= 0,
 r <= 9,
 y >= 0,
 y <= 9]

次にallvarsの中に重複要素がないことを書く.

In [13]:
solver.add(Distinct(allvars))

最上位に来る文字(s, m)は0でないことを書く

In [14]:
solver.add(s != 0)
solver.add(m != 0)

等式が成り立っていることを書く

In [15]:
solver.add(s * 1000 + e * 100 + n * 10 + d + m * 1000 + o * 100 + r * 10 + e == 
           m * 10000 + o * 1000 + n * 100 + e * 10 + y)

これが解を持つかどうかは solver.check() がsatを返すことで確認できる.

In [16]:
solver.check()
Out[16]:
sat

この時に変数にどのような割り当てが行われて制約が満たされたかは,solver.model() で確認できる.

In [17]:
solver.model()
Out[17]:
[r = 8, s = 9, e = 5, d = 7, n = 6, o = 0, m = 1, y = 2]

一瞬のうちに,

9 5 6 7
+ 1 0 8 5
1 0 6 5 2

という答えが求まった.これが,唯一の解かどうかを判定するにはsolverにこの解ではないという制約を入れて解かせてみると良い.

In [18]:
solver.add(Or(r != 8, s != 9, e != 5, d != 7, n != 6, o != 0, m != 1, y != 2))
solver.check()
Out[18]:
unsat
この答えがunsatであることで,解のuniqueness が計算できた.
In [ ]: