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

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

小テストに関する補足

(注) 小テストの問題2-2のz3のプログラムで，

solve(0 <= x0, x0 <= 1, 0 <= x1, x1 <= 1, p3, Or(p1, p2), Or(Not(p1), Not(p2)))

となっていたのですが，これは，

solve(0 <= x0, x0 <= 1, 0 <= x1, x1 <= 1, Not(p3), Or(p1, p2), Or(Not(p1), Not(p2)))

の誤りでした．

これに気がついて，穴埋めを

3 * x0 + 3 * x1 > 2

と書いた人も，

3 * x0 + 3 * x1<= 2

と書いた人もどちらも正解とします．

また，

3 * x0 + 3 * x1<= 2

と書いたプログラムを実行した結果の(1/6, 1/2)を問題2-1で解答した人も正解として扱います．

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

Google Colaboratoryを使って，クラウド実行環境でPythonプログラムを実行できます．

広域システム概論II: パズルをソルバーで解く
Googleアカウントへのログインを求められるので，通常のGoogleアカウント「XXX@gmail.com」でも，ECCSクラウドメールのアカウント「XXX@g.ecc.u-tokyo.ac.jp」のどちらでも良いので，ログインする．
Colaboratoryで開く」を選ぶ．
「PLAYGROUNDで開く」を選ぶ．
信頼できない作者によるNotebookを実行すると，セキュリティ上の危険があるため警告が出る．ktanaka@g.ecc.u-tokyo.ac.jp を信頼して実行する場合は，以下のように「このまま実行」を選ぶ．
Google Colaboratory で「ファイル」->「.ipynbをダウンロード」で保存したファイルは，手元の Jupyter NotebookからOpenして使うこともできる．

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

数学セミナー2017年9月号の「エレガントな解答をもとむ」でピーター・フランクルさんによる以下の問題が出された．

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を使って「エレガント」ではなく力任せで解ける．