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
変数の作成
ブール変数を作る
一つ作成
1 x = Bool("x")
複数同時作成
1 x, y = Bools(["x", "y"])
配列で同時作成
1 xs = [Bool("x%d" % i) for i in range (128)]
整数変数を作る
一つ作成
1 x = Int("x")
複数同時作成
1 x, y = Ints(["x", "y"])
配列で同時作成
1 xs = [Int("x%d" % i) for i in range (128)]
制約の設定
条件の追加
AND
OR
イコール
不等式
解を得る方法
ブール変数の解を得る
