|
⇤ ← 2015-04-27 21:41:08時点のリビジョン1
サイズ: 616
コメント:
|
サイズ: 1401
コメント:
|
| 削除された箇所はこのように表示されます。 | 追加された箇所はこのように表示されます。 |
| 行 6: | 行 6: |
| z3pyはZ3のPythonバインディングであり，Z3に付属している． |
|
| 行 8: | 行 10: |
| [[https://github.com/Z3Prover/z3|Z3のGithubページ]]からgit cloneしてビルド・インストールする． z3pyは `/usr/lib/python2.7/dist-packages` 以下に同時にインストールされる． Python3用はないの？ |
|
| 行 9: | 行 15: |
| {{{#!highlight python # モジュールをimport from z3 import * # 変数を作成．引数は人間が見てわかりやすい名前． x, y = Bools(["x", "y"]) # ソルバのインスタンスを生成して s = Solver() # 制約を追加 s.add(x == True) s.add(x != y) # 解を探索，モデルを取得 s.check() m = s.model() # 解を取得 solution_x = is_true(m[x]) solution_y = is_true(m[y]) print solution_x, solution_y }}} |
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
イコール
不等式
解を得る方法
ブール変数の解を得る
