竹内の「3人の賢者問題」の求解

このレポジトリには，[組合せゲーム・パズル 第11回 研究集会](http://www.alg.cei.uec.ac.jp/itohiro/Games/Game160307.html, 組合せゲーム・パズル プロジェクト 第11回 研究集会]での発表「SMTソルバを用いた「竹内の3人の賢者問題」の求解」関係のファイルを置きます．

---

スライド (three_wise_men.pdf)

(東京都立六郷工科高校教員の高池 建彦様の指摘を受けて2019/11/1 に 修正しています)

---

プログラムの説明と実行

python version 3用のプログラムです． [Z3](https://github.com/Z3Prover/z3, Z3)のpython bindingをインストールする必要があります．

---

0.py

• 1 – n の相異なるカードをA, B, Cに配れる最小のnを求めるプログラムです．
• 当然ながらn = 3 が解答になります．

---

1.py

• ニッコリが1回続く最小のnを求めるプログラムです．
• n = 5が解答になります．

---

2.py

• ニッコリが2回続く最小のnを求めるプログラムです．
• n = 9が解答になります．

---

3.py

• n = 20 に対してニッコリが最大何回続くかを求めるプログラムです．
• 3回続きます． (東京都立六郷工科高校教員の高池 建彦様の指摘を受けて2019/11/1 に 修正しています)

---

4.py

• n = 20 に対してニッコリが最大回数続いた後，自分の勝ちを宣言できるカードの組合せを求めます．
• 40通りになります． (東京都立六郷工科高校教員の高池 建彦様の指摘を受けて2019/11/1 に 修正しています)

---

関連リンク

• 竹内郁雄さん作成のプログラム https://www.dropbox.com/s/qfnddaybtwqv5l5/three-wizards.pdf?dl=0
• z3 (https://github.com/Z3Prover/z3)

---

おまけ

組合せゲーム・パズル 第11回 研究集会で田中の前に発表した九州大学山中さん の発表「『数の六角パズル』を頭だけ使って解こう」の追試をするz3プログラム (hex.py) と出力 (hex.out) も置きます．