PythonでSMTソルバ (z3py) 入門

はじめに

SMTソルバ^[1]とは、数式や真理値を用いて定式化された問題を解くツールです。例えば「$x + y < 5$ を満たす自然数$(x, y)$ をすべて求めなさい。」のような問題を解くことができます。
SMTソルバには様々な種類がありますが、本記事では z3^[2] を利用して簡単な問題を解いてみます。

準備

pip で z3py をインストールします。^[3]

pip install z3-solver

チュートリアル

簡単な例

問題

$x + y < 5$ を満たす自然数$(x, y)$ をすべて求めなさい。

解答

$(x,y) = (1,1),(1,2),(1,3),(2,1),(2,2),(3,1)$
具体的には、次のコードを用いて求めます。

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]

やや複雑な例

問題

$n$ を自然数とするとき、$\dfrac{n+110}{13}$ と $\dfrac{240-n}{7}$ の値がともに自然数となる $n$ の値をすべて求めなさい。(大阪府公立高等学校 2017改)

解答

$n = 72, 163$
具体的には、次のコードを用いて求めます。

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適性検査の推論などのパズル的な問題をはじめ、より複雑な問題にも応用が可能です。時間を見つけて挑戦してみようと思います。
なお、本記事の執筆にあたり 電気通信大学の講義サイト を参考にしました。日本語で詳細な情報がまとめられています。

脚注

1. SMTは、Satisfiability Modulo Theories (背景理論付き充足可能性問題) の略です。

2. Microsoft Research が開発したSMTソルバ。性能が良く、Pythonからも利用可能な z3py というバインディングが付属しています。

3. Dockerを用いたPython環境で、インストールに失敗する場合はこちらも参照ください。