fixedpoint.jp




2016/08/13

「歩と銀を逆にするゲーム」を最短手数で解くには

将棋の駒を使ったパズルに「歩と銀を逆にするゲーム」というものがあります。次の動画で紹介されています: https://www.youtube.com/watch?v=vUoOiphQhR8

図1:図1図2: 図2

簡単に言うと、図1のように3x3のマスに歩、銀、金からなる8枚の駒を置いて始め、この限られた9マス内で将棋のルールに従った駒の動きで図2のような配置に持っていく、というゲームです。

例えば、34手での解答は次のようになります: 図3

このゲームの解で最小手数はいくつになるでしょうか。プログラムで初期状態から可能な状態遷移を網羅したゲーム木を生成すると、図4(svg/png)が得られます。

図4における矢印は、1つ駒を動かして得られる状態遷移を表します。ただし、グレーで白抜きの△からなる矢印による遷移は、最短でない経路であることを示します。ブルーで◇からなる矢印による遷移は(これも最短でない経路を表しますが)、駒を動かすと同時に盤面を左右反転させると(鏡像として)得られることを示します。

図4によって、このゲームの解としては32手が最短手数であることが分かります。また以下のようなことも分かります:

#permalink

2016/08/02

"Einstein's five houses"パズルをCoqで解く

Einstein's five houses riddle、またはZebra puzzleとも呼ばれる有名なパズルがあります。今回はこの解答をCoqで形式的に証明しました。

以下がこの問題を定義と公理にしたものです。興味のある方はここから解答の証明を考えてみてください。

five_houses_problem.v
Section five_houses.

(* Definitions and axioms *)

Inductive owner : Type :=
| a : owner
| b : owner
| c : owner
| d : owner
| e : owner.

Inductive nationality : Type :=
| dane : nationality
| brit : nationality
| swede : nationality
| norwegian : nationality
| german : nationality.

Parameter citizen : owner -> nationality.

Inductive color : Type :=
| yellow : color
| red : color
| white : color
| green : color
| blue : color.

Parameter house : owner -> color.

Inductive animal : Type :=
| horse : animal
| cat : animal
| bird : animal
| fish : animal
| dog : animal.

Parameter pet : owner -> animal.

Inductive beverage : Type :=
| water : beverage
| tea : beverage
| milk : beverage
| coffee : beverage
| root_beer : beverage.

Parameter drink : owner -> beverage.

Inductive cigar : Type :=
| pall_mall : cigar
| prince : cigar
| blue_master : cigar
| dunhill : cigar
| blends : cigar.

Parameter smoke : owner -> cigar.

Definition left_of (X1 X2 : owner) : Prop :=
  match X1, X2 with
    | a, b => True
    | b, c => True
    | c, d => True
    | d, e => True
    | _, _ => False
  end.

Definition next_to (X1 X2 : owner) : Prop :=
  left_of X1 X2 \/ left_of X2 X1.

Axiom citizen_is_surjective:
  forall N : nationality, exists X : owner, citizen X = N.

Axiom house_is_surjective:
  forall C : color, exists X : owner, house X = C.

Axiom pet_is_surjective:
  forall A : animal, exists X : owner, pet X = A.

Axiom drink_is_surjective:
  forall B : beverage, exists X : owner, drink X = B.

Axiom smoke_is_surjective:
  forall C : cigar, exists X : owner, smoke X = C.

Axiom clue1: (* The Brit lives in the house with red walls. *)
  forall X : owner,  house X = red -> citizen X = brit.

Axiom clue2: (* The Swede has a dog. *)
  forall X : owner, citizen X = swede -> pet X = dog.

Axiom clue3: (* The Dane drinks tea. *)
  forall X : owner, citizen X = dane -> drink X = tea.

Axiom clue4: (* The house with green walls is directly to the left of the house with white walls. *)
  forall X1 X2 : owner,
    house X1 = green -> (left_of X1 X2 <-> house X2 = white).

Axiom clue5: (* The owner of the house with green walls drinks coffee. *)
  forall X : owner, house X = green -> drink X = coffee.

Axiom clue6: (* The person who smokes Pall Mall cigars owns a bird. *)
  forall X : owner, smoke X = pall_mall -> pet X = bird.

Axiom clue7: (* The owner of the house with yellow walls smokes Dunhill. *)
  forall X : owner, house X = yellow -> smoke X = dunhill.

Axiom clue8: (* The man living in the center house drinks milk. *)
  drink c = milk.

Axiom clue9: (* The Norwegian lives in the first house. *)
  citizen a = norwegian.

Axiom clue10: (* The man who smokes blends lives next to the cat owner. *)
  forall X1 X2 : owner,
    smoke X1 = blends -> pet X2 = cat -> next_to X1 X2.

Axiom clue11: (* The horse’s owner lives next to the man who smokes Dunhill. *)
  forall X1 X2: owner,
    pet X1 = horse -> smoke X2 = dunhill -> next_to X1 X2.

Axiom clue12: (* The man who smokes Blue Master drinks root beer. *)
  forall X : owner, drink X = root_beer -> smoke X = blue_master.

Axiom clue13: (* The German smokes Prince. *)
  forall X : owner, citizen X = german -> smoke X = prince.

Axiom clue14: (* The Norwegian lives next to the house with blue walls. *)
  forall X1 X2 : owner,
    citizen X1 = norwegian -> house X2 = blue -> next_to X1 X2.

Axiom clue15: (* The man who smokes Blends lives next to the man who drinks water. *)
  forall X1 X2 : owner,
    smoke X1 = blends -> drink X2 = water -> next_to X1 X2.

Coq 8.4pl4で確認した解答の証明はこちら:

five_houses.v

このように証明することで、上から順に補題を追っていけば、15の手掛りをどの段階で使ってパズルを解けばいいかが説明できるようになります。総当りで解いた場合にはそうはいきません。また、この形の定義と公理なら直観主義論理で証明できるということが分かります。ただし、citizen_is_surjectiveなど各関数の全射性を公理とする代わりに、単射性を公理として仮定した場合は(等しい有限基数を持つ集合間の関数なので同値ですが)この限りではなさそうです。

参考

#permalink

Archives

2016: Jul / Mar / Feb / Jan

2015: Dec / Oct / Sep / Jul / May / Mar / Feb

2014: Dec / Nov / Oct / Aug / Apr / Mar / Feb / Jan

2013: Dec / Nov / Oct / Sep / Aug / Jun / May / Apr / Mar

2012: Nov / Oct / Sep / Jul / Jun / May / Mar / Feb / Jan

2011: Dec / Nov / Oct / Sep / Jul / Jun / Apr / Mar / Feb / Jan

2010: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2009: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2008: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2007: Dec / Nov / Oct / Sep / Aug / Jul / Jun / May / Apr / Mar / Feb / Jan

2006: Dec / Nov / Oct / Sep


© 2006-2016 fixedpoint.jp