広域システム概論I「パズルをソルバーで解く」

担当田中哲朗

このページは2016/11/23(水)2限の広域システム概論Iで田中が担当した「パズルをソルバーで解く」のサポートページです．

スライド

solver.pdf 講義で使ったスライド(受講者以外への配布は不可)です．東京大学内部だけからアクセス可能．ユーザ名(iss1) パスワード(XX-YYY) (XX, YYY は講義のあった教室 (XX号館YYY教室) の数字に置き換えて下さい)

リンク

サンプルプログラム

線形制約

from z3 import *
x, y = Reals("x y")
p1 = (x + y <= 2)
p2 = (2 * x + y <= 3)
p3 = (x + y >= 3)
solve(x >= 0, y >= 0, p3, Or(p1, p2), Or(Not(p1), Not(p2)))

LinearSample ( LinearSample.py, LinearSample.ipynb )
非線形問題 ( nonlinear.py, nonlinear.ipynb )
覆面算 ( verbal_arithmetic.py, verbal_arithmetic.ipynb )
n-queens(ブール変数) ( nqueen_bool.py, .nqueen_boolipynb )
n-queens(整数変数) ( nqueen_int.py, nqueen_int.ipynb )
n-queens(row番号) ( nqueen_int_row.py, nqueen_int_row.ipynb )

Tutorialのnqueens 問題

from z3 import *
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)  for i in range(8) for j in range(i) ]
solve(val_c + col_c + diag_c)

z3を用いた3人の賢者問題の求解

数学セミナー「エレガントな解答をもとむ」で出題者の用意した解答の間違いの発見 z3を用いた3人の賢者問題の求解

z3を教育用計算機システム(ECCS)のMac環境で使う

ECCSのMac環境にはz3は入っていません．個人のホームディレクトリにz3を入れる方法を書きます．以下では，Anaconda 2.4.0のpython3環境に導入することを試みます．コマンドラインだけであれば，sshサーバで使う(およびインストール作業をおこなう)こともできます．

仮想環境の作成

/Applications/Anaconda3/bin/conda create -n my_root --clone=/usr/local/opt/pyenv/versions/anaconda3-2.4.0

を実行してください．数分間待つと，~/.conda/envs/my_root 以下に/usr/local/opt/pyenv/versions/anaconda3-2.4.0のコピーが作られます(z3までインストールすると ~/.conda 以下で200MBほどの容量のディスクが使われます)．

仮想環境の有効化

source /usr/local/opt/pyenv/versions/anaconda3-2.4.0/bin/activate my_root

を実行します．

z3のインストール

Anaconda用のz3はasmeurer / packages / z3で公開されています．

/Applications/Anaconda3/bin/conda install -c asmeurer z3=4.4.0

で ~/.conda 以下にインストールされます．

z3の利用

source /usr/local/opt/pyenv/versions/anaconda3-2.4.0/bin/activate my_root

を実行したターミナルで，

python

として起動すると，z3が使える環境でpython3が立ち上がります．

Python 3.5.2 |Anaconda 2.4.0 (x86_64)| (default, Jul  2 2016, 17:52:12) 
[GCC 4.2.1 Compatible Apple LLVM 4.2 (clang-425.0.28)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> x, y = Ints("x y")
>>> solve(x > 0, y > 0, x + y < 3, x + 2 * y < 5)
[y = 1, x = 1]

同じターミナルで，

jupyter-notebook

を実行すると，ブラウザ上でz3が使える状態で python3 を操作できます．

python2での利用

Z3 API in Pythonがpython2用に書かれているなどの理由でpython2で使いたい人がいるかもしれません．その場合は，以下のようにして，my_root2という名前でpython2の仮想環境を作って，z3をインストールすることもできます．

/Applications/Anaconda/bin/conda create -n my_root2 --clone=/usr/local/opt/pyenv/versions/anaconda-2.4.0
source /usr/local/opt/pyenv/versions/anaconda-2.4.0/bin/activate my_root2
/Applications/Anaconda/bin/conda install -c asmeurer z3=4.4.0