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

担当 田中哲朗

スライド

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

リンク

• z3(github)
• z3 Documentation
• Z3 API in Python

サンプルプログラム

• 線形制約

  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人の賢者問題の求解

他の問題

1+5+6=12と2+3+7=12は，同じ数(12)を，全く異なる3つずつの整数の和として表す式の組合せです．左辺に登場する整数 1,5,6,2,3,7には重複がありません．
右辺の数を42にして，同様な式いくつかの組合せ

a + b + c = 42
d + c + f = 42
g + h + i = 42
...

この問題はz3を使って「エレガント」ではなく力任せで解ける．

• seminar_9_elegant_1.html ( seminar_9_elegant_1.py seminar_9_elegant_1.ipynb )

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

• pyenv
• Anaconda-5.0.1
• z3

仮想環境の作成

mv ~/.pyenv ~/.pyenv.old

git clone https://github.com/yyuu/pyenv.git ~/.pyenv
echo 'export PYENV_ROOT="$HOME/.pyenv"' >> ~/.bashrc
echo 'export PATH="$PYENV_ROOT/bin:$PATH"' >> ~/.bashrc
echo 'eval "$(pyenv init -)"' >> ~/.bashrc
source ~/.bashrc
pyenv install -l | grep ana #最新のパッケージを検索
pyenv install anaconda3-5.0.1
pyenv rehash
pyenv global anaconda3-5.0.1
echo 'export PATH="$PYENV_ROOT/versions/anaconda3-5.0.1/bin/:$PATH"' >> ~/.bashrc
source ~/.bashrc
conda update conda

. ~/.bashrc

z3のインストール

mkdir ~/work
cd ~/work
git clone https://github.com/Z3Prover/z3.git

cd ~/work/z3
python scripts/mk_make.py --python --prefix=/home/「自分のユーザ名」/.pyenv/versions/anaconda3-5.0.1

cd ~/work/z3/build
make

make install

z3の利用

python

Python 3.6.3 |Anaconda, Inc.| (default, Oct  6 2017, 12:04:38) 
[GCC 4.2.1 Compatible Clang 4.0.1 (tags/RELEASE_401/final)] 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