z3py
Z3はMicrosoft Researchの開発した,SAT・SMTソルバである. ブール代数の充足問題に限らず,整数計画問題などにも適用が可能である.
z3pyはZ3のPythonバインディングであり,Z3に付属している.
目次
インストール
Z3のGithubページからgit cloneしてビルド・インストールする. z3pyは /usr/lib/python2.7/dist-packages 以下に同時にインストールされる. Python3用はないの?
基本的な流れ
1 # モジュールをimport
2 from z3 import *
3
4 # 変数を作成.引数は人間が見てわかりやすい名前.
5 x, y = Bools(["x", "y"])
6
7 # ソルバのインスタンスを生成して
8 s = Solver()
9
10 # 制約を追加
11 s.add(x == True)
12 s.add(x != y)
13
14 # 解を探索,モデルを取得
15 s.check()
16 m = s.model()
17
18 # 解を取得
19 solution_x = is_true(m[x])
20 solution_y = is_true(m[y])
21
22 print solution_x, solution_y
変数の作成
ブール変数を作る
整数変数を作る
制約の設定
条件の追加
AND
OR
イコール
不等式
解を得る方法
ブール変数の解を得る