ちょっと前に「Answer Set Programming」というのが使えそうだと思ったのだが、記述表現がよくわからなく停滞していたが、同じようなことをが「Z3Py」を使うとPythonで書けるということで、例題を通じて理解を深めようと思う。

SMTソルバー Z3Pyとは

Z3は、Microsoft Researchで開発された高性能の定理証明器（theorem prover）です。

SMT は背景理論付き充足可能性問題（Satisfiability Modulo Theories）の略語です。命題論理よりも表現能の高い論理体系で記述さた背景理論を、SAT技法で効果的に取り扱うことを目的とした技術だそうです。（条件を書くと、それが解けるか解けないかを判定してくれるもの、と理解していますorz）

例題

コイン問題（制約充足問題）
コイン問題２
 部分和問題
 魔法陣
 グラフ彩色問題
 数独
 ビンパッキング問題
 ナップサック問題
 クイーン問題
 制約最適化問題
 ハノイの塔
 巡回セールスマン問題
 ブロックワールド問題

参考

Z3: Theorem Prover
Coprisによる制約プログラミング入門

Ganesha 2021/07/25

コイン問題（制約充足問題）

問題

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 2021/08/04

コイン問題２

問題

以下のユーロ硬貨を持っているとする(総和は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 2021/08/04

部分和問題

問題

集合 {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()の詳細