PythonでSMTソルバ (z3py) 入門
はじめに
SMTソルバ[1]とは、数式や真理値を用いて定式化された問題を解くツールです。例えば「
SMTソルバには様々な種類がありますが、本記事では z3[2] を利用して簡単な問題を解いてみます。
準備
pip で z3py をインストールします。[3]
pip install z3-solver
チュートリアル
簡単な例
問題
解答
具体的には、次のコードを用いて求めます。
from z3 import *
# 変数定義
x = Int("x")
y = Int("y")
# 基本制約
s = Solver()
s.add(x > 0, y > 0)
s.add(x + y < 5)
# 解を探索
while(s.check() == sat):
# 解の表示
m = s.model()
print(m)
# 解を制約条件に追加
s.add(Not(And(x == m[x], y == m[y])))
結果は、次のように求まります。(表示順は異なる可能性があります)
[x = 1, y = 1]
[x = 1, y = 2]
[x = 1, y = 3]
[x = 2, y = 1]
[x = 2, y = 2]
[x = 3, y = 1]
やや複雑な例
問題
解答
具体的には、次のコードを用いて求めます。
from z3 import *
# 変数定義
n = Int("n")
x = Int("x")
y = Int("y")
# 基本制約
s = Solver()
s.add(n > 0, x > 0, y > 0)
s.add(13*x == (n+110))
s.add(7*y == (240-n))
# 解を探索
while(s.check() == sat):
# 解の表示
m = s.model()
print(m)
# 解を制約条件に追加
s.add(Not(n == m[n]))
結果は、次のように求まります。(表示順は異なる可能性があります)
[n = 72, x = 14, y = 24]
[n = 163, x = 21, y = 11]
まとめ
SMTソルバの一種であるz3を用いて整数問題を解いてみました。紹介した問題は、比較的簡単なコードで解けることも分かりました。
本記事の内容は、数独やSPI適性検査の推論などのパズル的な問題をはじめ、より複雑な問題にも応用が可能です。時間を見つけて挑戦してみようと思います。
なお、本記事の執筆にあたり 電気通信大学の講義サイト を参考にしました。日本語で詳細な情報がまとめられています。
-
SMTは、Satisfiability Modulo Theories (背景理論付き充足可能性問題) の略です。 ↩︎
-
Microsoft Research が開発したSMTソルバ。性能が良く、Pythonからも利用可能な z3py というバインディングが付属しています。 ↩︎
-
Dockerを用いたPython環境で、インストールに失敗する場合はこちらも参照ください。 ↩︎
Discussion