Pythonで論理式を簡単に解くSATソルバー/SMTソルバーZ3の基本的な使い方まとめ

こんにちは。

最近SAT/SMTソルバーなるものを知ったので、勉強がてら試しに使ってみることにしました。

今回はPythonで動くプログラムを使って、論理式を充足する解を求めてみようと思います。

SATソルバー・SMTソルバーとは

SATはSatisfiability problemという充足可能性問題のことで、

SMTはSatisfiability Modulo Theoriesの略だそうです。

こちらの資料(SAT/SMTソルバの仕組み)に詳しく書いてあります。

身近な言葉に言い換えると、以下の問題のことだと理解しました。

• SAT : 真偽値の論理式を満たす解が存在するか？を解く問題
• SMT : 真偽値だけでなく数式(算術演算)を含む式を満たす解が存在するか？を解く問題

(もし違ったらご指摘お願いします...)

PythonにZ3を導入する方法

pythonでは以下でパッケージがインストールできます。

pip install z3-solver

Z3の基本的な使い方

以下の流れで使用します。

1. Z3をimportする
2. 変数をセットする
3. ソルバーのインスタンスを作成する
4. ソルバーに制約条件を追加する
5. 解を探索する
6. モデルを取得 (解を取得する)

Z3をインポートする

from z3 import *

変数をセットする

真偽値の場合はBool()を、数値の場合はInt()を使います。

また、複数を一度にセットする場合はBools()やInts()のようにsをつけるとリストで返ってきます。

変数が大量にある場合は、Vectorをつけて「何個生成するか」を指定できる方法もあります。

p, q = Bools(["p", "q"]) # ブール変数
x = Int("x") # 整数変数

xs = BoolVector("x",12) # ブール変数を複数作成
xs = IntVector("x",12) # 整数変数を複数作成
# 作成された変数名: x__0, x__1, ..., x__12

xs = [Bool("x%d" % i) for i in range(12)]
# 作成された変数名: x0, x1, ..., x12

また、変数の型はz3.z3と特有のものであることがわかります。

# 型チェック
type(Bool("x")) # z3.z3.BoolRef
type(Int("x")) # z3.z3.ArithRef

ソルバーのインスタンスを作成する

s = Solver()

制約を追加する

命題というか変数が満たすべき条件式を書いていきます。

P1 = q == True
P2 = p != q # p ≠ q

s.add(P1,P2) 

addメソッドで、制約をソルバーに追加していきます。

追加された制約(つまり各変数の節)は、ANDで処理されます。

論理式はこんなものたちが使えます

And(P1,P2) # q = True ∧ p ≠ q
Or(P1,P2) # OR
Xor(P1,P2) # XOR
Not(P1) # ¬(q = True)
Implies(P1, P2) # q = True ⇒ p ≠ q

z3.z3特有の型なので、Pythonのandやorだとエラーになります。

解を探索する & モデルを取得する

r = s.check()

if r == sat:
  m = s.model()

.check()で式が充足可能か評価します。ソルバーの本体ですね。返り値がsatなら充足可能、unsatなら充足不可能です。

checkしたあと、充足可能なら.model()メソッドで解の組み合わせを取得できます。

解を取得する

ans_p = is_true(m[p])

model()の返り値はz3特有の形式となっているので、pythonの型に変換したくなったりします。

真偽値の場合はis_true()でbooleanに変換、数値の場合は.as_long()メソッドで数値に変換できます。

インスタンス作成から表示までを一括処理

solve()を使うことでSolver()インスタンス作成せずに一気に解の表示までできます。

軽く調べたいときに便利。

p, q = Bools("p q")

P1 = Not(p)
P2 = Or(p, q)

solve(P1,P2) # 結果: [p = False, q = True]

SATの例題 論理式

以下の論理式を充足する解を調べてみます。

変数$x$はTrue or Falseの真偽値です。

こちら(数独を一瞬で解く by SATソルバー)の例題と同じものです。

解は$x_1=1, x_2=0, x3=1$ですね。

例題を解いてみる

というわけで上の例題を解いてみます。

x1,x2,x3 = Bools("x1 x2 x3")

s = Solver()

P1 = Or(x1,Not(x2)) # x1 ∨ ¬x2
P2 = x3
P3 = Or(Not(x1),Not(x2)) # ¬x1 ∨ ¬x2

s.add(P1,P2,P3,P4) # [x1 ∨ ¬x2, x3, ¬x1 ∨ ¬x2]

c = s.check() # sat
if c == sat:
  m = s.model() # [x3 = True, x2 = False, x1 = False]

l = [x1,x2,x3]

for i in l:
  print(f"{i} = {is_true(m[i])}")

"""
結果
x1 = False
x2 = False
x3 = True
"""

...って、予想してた答えと違う！！

でもこの解でも式が成り立ちそうなので、複数の解があるようですね。

$x1$がTrueになるようにP4 = x1という節を追加してみました。

これでも全体が充足可能で、無事に予想していた答えになりました。

x1,x2,x3 = Bools("x1 x2 x3")

s = Solver()

P1 = Or(x1,Not(x2)) # x1 ∨ ¬x2
P2 = x3
P3 = Or(Not(x1),Not(x2)) # ¬x1 ∨ ¬x2
P4 = x1

solve(P1,P2,P3,P4)
"""
結果
[x3 = True, x2 = False, x1 = True]
"""

SMTの例題 不等式を含む数式

いい感じの問題が見つからなかったので自分で作ってみました。

以下の条件をすべて満たす整数$x,y$の値はいくつでしょうか？

• $x > 2$
• $0 < y < 3$
• $x+y <5$

これは簡単にわかりますが、$x=3, y=1$ですね。

SMTの例題を解いてみる

上の条件を書いていきます。

２つめの条件のような囲まれた不等式は1つの式にできないので、P2とP3のように２つの節に分けます。

x,y = Ints("x y")

P1 = x>2
P2 = 0<y
P3 = y<3
P4 = x+y<5

solve(P1,P2,P3,P4)
"""
結果
[y = 1, x = 3]
"""

というわけで無事に解けました。

参考

Z3Prover/z3: The Z3 Theorem Prover - GitHub

SAT/SMTソルバのしくみ Proof summit 2015

充足可能性問題について

電気通信大学MMA z3py