z3を使ってパズルを解く¶

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

覆面算を解く¶

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

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

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

from z3 import *

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

solverを作る．

solver = Solver()

これで，ソルバが作られる．

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

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

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

for var in allvars:
    solver.add(0 <= var, var <= 9)

solver

[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の中に重複要素がないことを書く．

solver.add(Distinct(allvars))

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

solver.add(s != 0)
solver.add(m != 0)

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

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を返すことで確認できる．

solver.check()

sat

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

solver.model()

[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にこの解ではないという制約を入れて解かせてみると良い．

solver.add(Or(r != 8, s != 9, e != 5, d != 7, n != 6, o != 0, m != 1, y != 2))
solver.check()

unsat