SMTソルバー Z3Py
Ganeshaちょっと前に「Answer Set Programming」というのが使えそうだと思ったのだが、記述表現がよくわからなく停滞していたが、同じようなことをが「Z3Py」を使うとPythonで書けるということで、例題を通じて理解を深めようと思う。
SMTソルバー Z3Pyとは
Z3は、Microsoft Researchで開発された高性能の定理証明器（theorem prover）です。 SMT は背景理論付き充足可能性問題（Satisfiability Modulo Theories）の略語です。命題論理よりも表現能の高い論理体系で記述さた背景理論を、SAT技法で効果的に取り扱うことを目的とした技術だそうです。（条件を書くと、それが解けるか解けないかを判定してくれるもの、と理解していますorz）
例題
コイン問題（制約充足問題）
コイン問題２
部分和問題
魔法陣
グラフ彩色問題
数独
ビンパッキング問題
ナップサック問題
クイーン問題
制約最適化問題
ハノイの塔
巡回セールスマン問題
ブロックワールド問題
参考
Ganeshaコイン問題（制約充足問題）
問題
1円硬貨，5円硬貨，10円硬貨を合計で15枚，それぞれを1枚以上持っている．
金額の合計は90円である． それぞれの硬貨を何枚持っているか?
回答
from z3 import *
coin__1yen = Int("coin__1yen")
coin__5yen = Int("coin__5yen")
coin_10yen = Int("coin_10yen")
s = Solver()
s.add(coin__1yen >= 1)
s.add(coin__5yen >= 1)
s.add(coin_10yen >= 1)
s.add((coin__1yen + coin__5yen + coin_10yen) == 15)
s.add((coin__1yen + 5 * coin__5yen + 10 * coin_10yen) == 90)
print(s.check())
if s.check() == sat:
print(s.model())
出力
sat
[coin__5yen = 3, coin_10yen = 7, coin__1yen = 5]
解説
【基本的な順序】
Int()等で変数を定義し、s=Solver()にs.add()で条件・制約を定義する。
s.check()で解があるかを確認する。（たぶん、ここで演算をしている）
解がある場合、「sat」が返ってき、解がない場合は「unsat」が返ってくる。
「sat」が返ってきた場合、s.model()で条件を満たす解の1つが取得できる。
（一つしか出てこないため、条件を満たす解が見つかった時点で探索を終了すると思われる）
Ganeshaコイン問題２
問題
以下のユーロ硬貨を持っているとする(総和は148セントになる)。
20セント硬貨 4枚
10セント硬貨 4枚
5セント硬貨 4枚
2セント硬貨 4枚
合計がちょうど93セントになる組合せはあるだろうか?
各3枚の場合はどうか？
回答
from z3 import *
coin__2cent = Int("coin__2cent")
coin__5cent = Int("coin__5cent")
coin_10cent = Int("coin_10cent")
coin_20cent = Int("coin_20cent")
s = Solver()
s.add(And(0 <= coin__2cent, coin__2cent <= 4))
s.add(And(0 <= coin__5cent, coin__5cent <= 4))
s.add(And(0 <= coin_10cent, coin_10cent <= 4))
s.add(And(0 <= coin_20cent, coin_20cent <= 4))
s.add(2*coin__2cent + 5*coin__5cent + 10*coin_10cent + 20*coin_20cent == 93)
print(s.check())
if s.check() == sat:
print(s.model())
s = Solver()
s.add(And(0 <= coin__2cent, coin__2cent <= 3))
s.add(And(0 <= coin__5cent, coin__5cent <= 3))
s.add(And(0 <= coin_10cent, coin_10cent <= 3))
s.add(And(0 <= coin_20cent, coin_20cent <= 3))
s.add(2*coin__2cent + 5*coin__5cent + 10*coin_10cent + 20*coin_20cent == 93)
print(s.check())
if s.check() == sat:
print(s.model())
出力
sat
[coin__2cent = 4,
coin__5cent = 1,
coin_10cent = 0,
coin_20cent = 4]
unsat
4枚の場合は解があるが、3枚の場合は解がないことが分かる。
解説
And()は、And条件を生成します。
そもそも、条件の追加（.add()）はAnd条件として追加されているので、
s.add(0 <= coin_20cent, coin_20cent <= 4)も同じ。（今回の例では、必要なかったということ）
And()の詳細
or()もある。
Or()の詳細
Ganesha部分和問題
問題
集合 {2,3,5,8,13,21,34} の部分集合で， 和が50になるものはあるか?
回答
from z3 import *
X = [2, 3, 5, 8, 13, 21, 34]
a = [Bool("a%s" % i) for i in range(len(X))]
s = Solver()
s.add(Sum([X[i]*a[i] for i in range(len(X))]) == 50)
print(s.check())
if s.check() == sat:
m = s.model()
subset = []
for i in range(len(X)):
if m[a[i]] == True:
subset.append(X[i])
print(subset)
出力
sat
[3, 5, 8, 13, 21]
解説
Bool("a")で、ブーリアン型の変数を定義できる。
Sum()で、入力したものの総和を計算します。（配列でなくてもOK）
例）Sum([a, b, c]) → a + b + c
Sum()の詳細