	Rob Kremer
	Example Solution: And Tree/ Towers of Hanoi CPSC 433: Artifical Intelligence	Computer Science

Model

Note that we are modeling the problem as a tower to move to another spindle with only ONE spindle having any disks on it. It may be in the overall picture, there are disks on other spindles, but those are always ignored and treated like the base. Thus, a problem is always to move n spindles to the spindle.

A: (S,T)
S: Atree
Atree: (pr, sol:{yes,?}, b₁:Atree, ... ,b_n:Atree), n>=0
Tower: seq Nat | ∀ x,y ∈ Tower • ((x=y) → (ord x = ord y)) /\ ((ord x < ord y) → (y > x)) // A Tower is a sequence of numbers (disks) with no duplicates with only smaller on larger disks
pr: {(T₁:Tower, T₂:Tower, T₃:Tower, d:{1,2,3}) | ∃ i, j | i≠j /\ j≠n . T_i≠<<>> /\ T_n=<<>> /\ T_j=<<>> } // A problem is a 3 spindles with a tower on one and the other spindles are empty, together with a target spindle (which is empty). Note that it could be that i=n, which means the problem is solved.

Div: pr+
Div = ((T₁, T₂, T₃, n), ((T'₁, T'₂, T'₃, n'), (T"₁, T"₂, T"₃, n"), (T'''₁, T'''₂, T'₃, n''')) where
    ∃ i, j | i≠j /\ j≠n /\ i≠n /\ T_i≠<<>> /\ T_n=<<>> /\ T_j=<<>> .
   T'_i = tail T_i /\ T'_j = <<>> /\ T'_n == <<>> /\ n' = j
   T"_i = << head T_i >> /\ T"_j = <<>> /\ T"_n == <<>> /\ n" = n
   T'''_i = <<>> /\ T'''_j = tail T_i /\ T'''_n == <<>> /\ n''' = n
// T_i is the stack, T_n is the target. Move all but the bottom disk to T_j; move the bottom disk to T_n; then move T_j to T_n.

T: S x S,
T= {(s₁, s₂) | s₁ ∈ S /\ s₂ ∈ S . Erw (s₁, s₂) \/ Erw* (s₂, s₁)}
Erw((pr, ?), (pr, yes)) \/ // mark solved
Erw((pr, ?), (pr, ?, (pr₁, ?), ..., (pr_n, ?))) \/ // divide the problem into children
Erw((pr, ?, b₁, ..., b_n), (pr, ?, b₁', ..., b_n')), ∃₁ j | j ≤ n • ∀ i | i ≠ j • Erw(b_j, b_j'), /\ b_i = b_i' // choose a child to work on
Erw*((pr, ?, , b₁, ... , b_n), (pr, ?, , b₁', ... , b_n')), ∀ i • Erw*(b_i, b_i') \/ b_i' = b_i' // backtrack //This is not needed for this problem
Erw_markSolved((T₁, T₂, T₃, n)) = T_n ≠ <<>>
Erw_divide= (pr, ?) → (pr, ?, Div(pr))
Erw_choose= <random>
Erw* = <never backtrack >

Process

P: (A, Env, K)
Env: (none)
K: S x Env → S
K(s,env) = apply Erw until we can mark the root as solved.

Search Instance (Example)

Ins = (s₀, G)
s₀= (<<3 2 1>>, <<>>, <<>>)
G: s → {yes,no}
G = {s → x | s ∈ s_goal /\ x=yes \/ x=no}

s_goal ⊆ s \/ no more expansions possible
s_goal= {(<<>>, <<>>, <<3 2 1>>)}

Example Diagram

                                                                                                         (<<3 2 1>>, <<>>, <<>>, 3)
                                                                                                    /                            |                       \
                                                             (<<2 1>>, <<>>, <<>>, 2) (<<3>>, <<>>, <<>>, 3) (<<>>, <<2 1>>, <<>>, 3)
                                        /                               |                \                               yes                         /                      |                                    \
(<<1>>, <<>>, <<>>, 3) (<<2>>, <<>>, <<>>, 2) (<<>>, <<>>, <<1>>, 2)    (<<>>, <<1>>, <<>>, 1) (<<>>, <<2>>, <<>>, 3) (<<1>>, <<>>, <<>>, 3)
              yes                                       yes                                         yes                                yes                                       yes                                         yes

CPSC 433: Arficial Intelligence

Last updated 2013-09-01 15:45

Rob Kremer