$35
Project 2: SATPlan and the Tower of Hanoi Solution
The Tower of Hanoi is a classic puzzle consisting of round disks stacked on pegs. One must move all disks to the nal peg, subject to the following constraints:
Only one disk can be moved at a time.
Each move consists of taking the upper disk from one of the stacks and placing it on top of another stack.
No disk may be placed on top of a smaller disk.
Answer the following questions:
(15 pts) Create PDDL domains (operators and facts) for the following Tower of Hanoi instances (it is possible that the PDDL operators will be the same):
Three pegs and two disks. Answer:
Operators:
Listing 1: Getting labels
1 ( d e f i n e ( domain h a n o i )
( : p r e d i c a t e s
3
( c l e a r ? x )
4
( s m a l l e r ? x ? y )
( on ? x ? y ) )
6
7
( : a c t i o n
move
disk
8
: p a r a m e t e r s
( ? d i s k
? from ? t o )
9
: p r e c o n d i t i o n
(and
( s m a l l e r
? d i s k
? t o )
10
( on
? d i s k
? from )
11
( c l e a r ? d i s k )
12
( c l e a r ? t o ) )
13
: e f f e c t
(and
( c l e a r ? from )
14
( on ? d i s k ? t o )
15
( not
( on
? d i s k
? from ) )
16
( not ( c l e a r
? t o ) ) ) ) )
Facts:
1
( d e f i n e ( problem
towers
of
hanoi
three
pegs two disks )
( : domain h a n o i )
3 ( : o b j e c t s d i s k 1 d i s k 2 peg1 peg2 peg3 )
( : i n i t
5
( on d i s k 1
d i s k 2 )
6
( on d i s k 2
peg1 )
7
( c l e a r d i s k 1 )
8
( c l e a r
peg2 )
9
( c l e a r
peg3 )
10
( s m a l l e r d i s k 1 d i s k 2 )
1 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
11
( s m a l l e r
d i s k 1
peg1 )
( s m a l l e r
d i s k 1
peg2 )
( s m a l l e r
d i s k 1
peg3 )
12
( s m a l l e r
d i s k 2
peg1 )
( s m a l l e r
d i s k 2
peg2 )
( s m a l l e r
d i s k 2
peg3 ) )
13
( : g o a l (and
( on
d i s k 2
peg3 )
14
( on d i s k 1
d i s k 2 ) ) ) )
(b) Three pegs and four disks. Answer: Operators:
1 ( d e f i n e ( domain h a n o i )
( : p r e d i c a t e s
3
( c l e a r ? x )
4
( s m a l l e r ? x ? y )
( on ? x ? y ) )
6
7
( : a c t i o n
move
disk
8
: p a r a m e t e r s
( ? d i s k
? from ? t o )
9
: p r e c o n d i t i o n
(and
( s m a l l e r
? d i s k
? t o )
10
( on ? d i s k
? from )
11
( c l e a r
? d i s k )
12
( c l e a r
? t o ) )
13
: e f f e c t
(and
( c l e a r ? from )
14
( on ? d i s k ? t o )
15
( not
( on ? d i s k
? from ) )
16
( not ( c l e a r
? t o ) ) ) ) )
Facts:
1 ( d e f i n e ( problem towers of hanoi three pegs four disks )
( : domain h a n o i )
3 ( : o b j e c t s d i s k 1 d i s k 2 d i s k 3 d i s k 4 peg1 peg2 peg3 )
( : i n i t
5
( on d i s k 1 d i s k 2 )
6
( on d i s k 2 d i s k 3 )
7
( on d i s k 3 d i s k 4 )
8
( on d i s k 4
peg1 )
9
( c l e a r d i s k 1 )
10
( c l e a r
peg2 )
11
( c l e a r
peg3 )
12
( s m a l l e r d i s k 1 d i s k 2 )
13
( s m a l l e r d i s k 1 d i s k 3 )
14
( s m a l l e r d i s k 1 d i s k 4 )
15
( s m a l l e r d i s k 2 d i s k 3 )
16
( s m a l l e r d i s k 2 d i s k 4 )
17
( s m a l l e r d i s k 3 d i s k 4 )
18
( s m a l l e r
d i s k 1
peg1 )
( s m a l l e r
d i s k 1
peg2 )
( s m a l l e r
d i s k 1
peg3 )
19
( s m a l l e r
d i s k 2
peg1 )
( s m a l l e r
d i s k 2
peg2 )
( s m a l l e r
d i s k 2
peg3 )
20
( s m a l l e r
d i s k 3
peg1 )
( s m a l l e r
d i s k 3
peg2 )
( s m a l l e r
d i s k 3
peg3 )
21
( s m a l l e r
d i s k 4
peg1 )
( s m a l l e r
d i s k 4
peg2 )
( s m a l l e r
d i s k 4
peg3 ) )
22
( : g o a l (and
( on
d i s k 1
d i s k 2 )
23
( on d i s k 2 d i s k 3 )
24
( on d i s k 3 d i s k 4 )
25
( on
d i s k 4
peg3 ) ) ) )
(10 pts) Download one or more of the following planners and use them to produce plans for your PDDL domains:
Blackbox: https://www.cs.rochester.edu/u/kautz/satplan/blackbox/
Madagascar: http://research.ics.aalto.fi/software/sat/madagascar/
TMKit: http://tmkit.dyalab.org/
What plans are produced by each planner for each instance (two and four disks)?
Three pegs and two disks Answer:
1
( move
disk
d i s k 1
d i s k 2
peg2 )
2
( move
disk
d i s k 2
peg1
peg3 )
3
( move
disk
d i s k 1
peg2
d i s k 2 )
2 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
(b) Three pegs and four disks Answer:
1
( move
disk
d i s k 1
d i s k 2
peg2 )
2
( move
disk
d i s k 2
d i s k 3
peg3 )
3
( move
disk
d i s k 1
peg2
d i s k 2 )
4
( move
disk
d i s k 3
d i s k 4
peg2 )
5
( move
disk
d i s k 1
d i s k 2
d i s k 4 )
6
( move
disk
d i s k 2
peg3
d i s k 3 )
7
( move
disk
d i s k 1
d i s k 4
d i s k 2 )
8
( move
disk d i s k 4 peg1 peg3 )
9
( move
disk
d i s k 1
d i s k 2
d i s k 4 )
10
( move
disk
d i s k 2
d i s k 3
peg1 )
11
( move
disk
d i s k 1
d i s k 4
d i s k 2 )
12
( move
disk
d i s k 3
peg2
d i s k 4 )
13
( move
disk
d i s k 1
d i s k 2
peg2 )
14
( move
disk
d i s k 2
peg1
d i s k 3 )
15
( move
disk
d i s k 1
peg2
d i s k 2 )
3. (15 pts) Encode the two-disk instance as a Boolean formula using the SATPlan method. Answer:
1
(and
( or
(NOT
n o o p c l e a r p e g 2
1 )
c l e a r
p e g 2
0
)
2
(
or
(NOT n o o p
c l e a r
p e g 3
1 )
c l e a r
p e g 3
0
)
3
(
or
(NOT n o o p
s m a l l e r
d i s k 1
d i s k 2
1 )
s m a l l e r
d i s k 1 d i s k 2
0
)
4
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
1 )
c l e a r
p e g 2
0
)
5
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
1 )
c l e a r
d i s k 1
0
)
6
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
1 )
o n d i s k 1 d i s k 2
0
)
7
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
1 )
s m a l l e r
d i s k 1
p e g 2
0
)
8
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
1 )
c l e a r
p e g 3
0
)
9
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
1 )
c l e a r
d i s k 1
0
)
10
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
1 )
o n
d i s k 1 d i s k 2
0
)
11
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
1 )
s m a l l e r
d i s k 1
p e g 3
0
)
12
(
or
(NOT n o o p
s m a l l e r
d i s k 1
p e g 2 1 )
s m a l l e r
d i s k 1
p e g 2
0
)
13
(
or
(NOT n o o p
s m a l l e r
d i s k 1
p e g 3
1 )
s m a l l e r
d i s k 1
p e g 3
0
)
14
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
1 )
o n
d i s k 1
d i s k 2
0
)
15
(
or
(NOT
n o o p
o n d i s k 2 p e g 1
1 )
o n
d i s k 2 p e g 1
0 )
16
(
or
(NOT n o o p
c l e a r
d i s k 1
1 )
c l e a r
d i s k 1
0 )
17
(
or
(NOT n o o p
s m a l l e r
d i s k 2
p e g 2 1 )
s m a l l e r
d i s k 2
p e g 2
0
)
18
(
or
(NOT n o o p
s m a l l e r
d i s k 2
p e g 3
1 )
s m a l l e r
d i s k 2
p e g 3
0
)
19
(
or
(NOT n o o p
c l e a r
p e g 3
2 )
c l e a r p e g 3
1
)
20
(
or
(NOT n o o p
s m a l l e r
d i s k 1
d i s k 2
2
)
s m a l l e r
d i s k 1 d i s k 2
1
)
21
(
or
(NOT
m o v e
d i s k
d i s k 1 p e g 3 d i s k 2
2 )
c l e a r
d i s k 2
1
)
22
(
or
(NOT
m o v e
d i s k
d i s k 1 p e g 3 d i s k 2
2
) c l e a r
d i s k 1
1
)
23
(
or
(NOT
m o v e
d i s k
d i s k 1 p e g 3 d i s k 2
2
)
o n
d i s k 1
p e g 3
1
)
24
(
or
(NOT
m o v e
d i s k
d i s k 1 p e g 3 d i s k 2
2
) s m a l l e r
d i s k 1
d i s k 2
1
)
25
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
2
) c l e a r
p e g 2
1
)
26
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
2
) c l e a r
d i s k 1
1
)
27
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
2
)
o n d i s k 1 d i s k 2
1
)
28
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
2
) s m a l l e r
d i s k 1
p e g 2
1
)
29
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
2
) c l e a r
p e g 3
1
)
30
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
2
) c l e a r
d i s k 1
1
)
31
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
2
)
o n
d i s k 1 d i s k 2
1
)
32
(
or
(NOT
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
2
) s m a l l e r
d i s k 1
p e g 3
1
)
33
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2 )
c l e a r
p e g 2
1
)
34
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2
)
c l e a r
d i s k 2
1
)
35
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2
)
o n d i s k 2 p e g 1
1
)
36
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2
)
s m a l l e r
d i s k 2
p e g 2
1
)
37
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2
)
c l e a r
p e g 2
1
)
38
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2
)
c l e a r
d i s k 1
1
)
39
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2
)
o n d i s k 1 p e g 3
1
)
40
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2
)
s m a l l e r
d i s k 1
p e g 2
1
)
41
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2
)
c l e a r
p e g 3
1
)
42
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2
)
c l e a r
d i s k 2
1
)
43
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2
)
o n d i s k 2 p e g 1
1
)
44
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2
)
s m a l l e r
d i s k 2
p e g 3
1
)
45
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
2 )
o n
d i s k 1
d i s k 2
1
)
46
(
or
(NOT
m o v e
d i s k
d i s k 1 p e g 2 d i s k 2
2 )
c l e a r
d i s k 2
1
)
47
(
or
(NOT
m o v e
d i s k
d i s k 1 p e g 2 d i s k 2
2 )
c l e a r
d i s k 1
1
)
48
(
or
(NOT
m o v e
d i s k
d i s k 1
p e g 2
d i s k 2
2 )
o n d i s k 1 p e g 2
1
)
3 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
49
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2 )
s m a l l e r
d i s k 1 d i s k 2
1
)
50
(
or
(NOT
n o o p
o n d i s k 2 p e g 1
2 )
o n
d i s k 2
p e g 1
1
)
51
(
or
(NOT
n o o p
c l e a r
d i s k 1
2 )
c l e a r
d i s k 1
1
)
52
(
or
(NOT
n o o p
c l e a r
d i s k 2
2 )
c l e a r
d i s k 2
1
)
53
(
or
(NOT
mov e
di sk di sk1 pe g2 pe g3
2 )
c l e a r
p e g 3
1
)
54
(
or
(NOT
mov e
di sk di sk1 pe g2 pe g3
2 )
c l e a r
d i s k 1
1
)
55
(
or
(NOT
mov e
di sk di sk1 pe g2 pe g3
2 )
o n d i s k 1 p e g 2
1
)
56
(
or
(NOT
mov e
di sk di sk1 pe g2 pe g3
2 )
s m a l l e r d i s k 1
p e g 3
1
)
57
(
or
(NOT
n o o p
o n d i s k 1 p e g 2
2 )
o n
d i s k 1
p e g 2
1
)
58
(
or
(NOT
n o o p
o n d i s k 1 p e g 3
2 )
o n
d i s k 1
p e g 3
1
)
59
(
or
(NOT
n o o p
s m a l l e r d i s k 2
p e g 3 2 )
s m a l l e r
d i s k 2
p e g 3
1
)
60
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3 )
c l e a r
p e g 3
2
)
61
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3 )
c l e a r
d i s k 2
2
)
62
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3 )
o n d i s k 2 p e g 2
2
)
63
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3 )
s m a l l e r d i s k 2
p e g 3
2
)
64
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3 )
c l e a r
d i s k 2
2
)
65
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3 )
c l e a r
d i s k 1
2
)
66
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3 )
o n
d i s k 1 p e g 3
2
)
67
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3 )
s m a l l e r
d i s k 1 d i s k 2
2
)
68
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
c l e a r
p e g 3
2
)
69
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
c l e a r
d i s k 2
2
)
70
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
o n d i s k 2 p e g 1
2
)
71
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
s m a l l e r d i s k 2
p e g 3
2
)
72
(
or
(NOT
n o o p
o n d i s k 1
d i s k 2 3 )
o n
d i s k 1 d i s k 2
2
)
73
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
3
)
c l e a r
d i s k 2
2
)
74
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
3
)
c l e a r
d i s k 1
2
)
75
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
3
)
o n
d i s k 1 p e g 2
2
)
76
(
or
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
3 )
s m a l l e r
d i s k 1 d i s k 2
2
)
77
(
or
(NOT
n o o p
o n d i s k 2 p e g 3
3
)
o n
d i s k 2
p e g 3
2
)
78
(
or
(NOT
c l e a r
p e g 3
1 )
n o o p c l e a r
p e g 3
1
)
79
(
or
(NOT
s m a l l e r
d i s k 2
p e g 2
1 )
n o o p s m a l l e r
d i s k 2
p e g 2
1
)
80
(
or
(NOT
s m a l l e r
d i s k 2
p e g 3
1 )
n o o p s m a l l e r
d i s k 2
p e g 3
1
)
81
(
or
(NOT
o n d i s k 1 p e g 2
1 )
m o v e
d i s k
d i s k 1 d i s k 2 p e g 2
1
)
82
(
or
(NOT
o n d i s k 1 p e g 3
1 )
m o v e
d i s k
d i s k 1 d i s k 2 p e g 3
1
)
83
(
or
(NOT
c l e a r
d i s k 1
1 )
n o o p
c l e a r
d i s k 1
1
)
84
(
or
(NOT
c l e a r
d i s k 2
1 )
m o v e d i s k
d i s k 1 d i s k 2
p e g 2
1
m o v e
d i s k d i s k 1
d i s k 2 p e g 3
1
)
85
(
or
(NOT
s m a l l e r
d i s k 1
d i s k 2
1 )
n o o p
s m a l l e r
d i s k 1
d i s k 2
1
)
86
(
or
(NOT
s m a l l e r
d i s k 1
p e g 2
1 )
n o o p s m a l l e r
d i s k 1
p e g 2
1
)
87
(
or
(NOT
s m a l l e r
d i s k 1
p e g 3
1 )
n o o p s m a l l e r
d i s k 1
p e g 3
1
)
88
(
or
(NOT
o n d i s k 1 d i s k 2
1 )
n o o p
o n d i s k 1
d i s k 2
1
)
89
(
or
(NOT
o n d i s k 2 p e g 1
1 )
n o o p
o n d i s k 2 p e g 1
1
)
90
(
or
(NOT
c l e a r
p e g 2
1 )
n o o p c l e a r
p e g 2
1
)
91
(
or
(NOT
n o o p
c l e a r
p e g 2
1 )
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 2
1
) )
92
(
or
(NOT
n o o p
c l e a r
p e g 3
1 )
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 3
1
) )
93
(
or
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 2
1 )
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
1 ) )
94
(
or
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 2
1 )
(NOT n o o p o n d i s k 1 d i s k 2
1
) )
95
(
or
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 3
1 )
(NOT n o o p o n d i s k 1 d i s k 2
1
) )
96
(
or
(NOT
o n d i s k 2 p e g 3
2 )
mov e
di sk di sk2 pe g1 pe g3
2
)
97
(
or
(NOT
c l e a r
p e g 3
2 )
n o o p c l e a r
p e g 3
2
m o v e
d i s k
d i s k 1
p e g 3
d i s k 2
2
move
di sk
di sk1 pe g3 pe g2
)
98
(
or
(NOT
s m a l l e r
d i s k 2
p e g 3
2 )
n o o p s m a l l e r
d i s k 2
p e g 3
2
)
99
(
or
(NOT
o n d i s k 1 p e g 2
2 )
n o o p
o n d i s k 1 p e g 2
2
move
di sk
di sk1 pe g3 pe g2
2
m o v e
d i s k d i s k 1 d i s k
100
(
or
(NOT
o n d i s k 1 p e g 3
2 )
n o o p
o n d i s k 1 p e g 3
2
move
di sk
di sk1
pe g2
pe g3
2
m o v e
d i s k d i s k 1 d i s k
101
(
or
(NOT
c l e a r
d i s k 1
2
)
n o o p
c l e a r
d i s k 1
2
)
102
(
or
(NOT
s m a l l e r
d i s k 1
d i s k 2
2 )
n o o p
s m a l l e r
d i s k 1
d i s k 2
2
)
103
(
or
(NOT
c l e a r
d i s k 2
2 )
n o o p
c l e a r
d i s k 2
2
m o v e
d i s k
d i s k 1
d i s k 2
p e g 2
2
m o v e
d i s k
d i s k 1
d i s k 2 p
)
104
(
or
(NOT
o n d i s k 1 d i s k 2
2 )
n o o p
o n
d i s k 1
d i s k 2
2
m o v e
d i s k
d i s k 1
p e g 2
d i s k 2
2
m o v e
d i s k
d i s k 1
)
105
(
or
(NOT
o n d i s k 2 p e g 1
2 )
n o o p
o n
d i s k 2 p e g 1
2
)
106
(
or
(NOT
o n d i s k 2 p e g 2
2 )
m ove
di sk di sk2 pe g1 pe g2
2
)
107
(
or
(NOT
n o o p
c l e a r
p e g 3
2 )
(NOT
m ove
di sk di sk1 pe g2 pe g3
2
) )
108
(
or
(NOT
n o o p
c l e a r
p e g 3
2 )
(NOT
m ove
di sk di sk2 pe g1 pe g3
2
) )
109
(
or
(NOT
n o o p
c l e a r
p e g 3
2 )
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2
) )
110
(
or
(NOT
n o o p
c l e a r
p e g 3
2 )
(NOT
m ove
di sk di sk1 pe g3 pe g2
2
) )
111
(
or
(NOT
n o o p
c l e a r
p e g 3
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2
) )
112
(
or
(NOT
n o o p
c l e a r
p e g 3
2 )
(NOT
n o o p
o n d i s k 1 p e g 3
2
) )
113
(
or
(NOT
m o v e
d i s k
d i s k 1
p e g 3
d i s k 2
2 )
(NOT
move
di sk di sk1 pe g2 pe g3
2
) )
4 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
114
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
move
di sk di sk1 pe g3 pe g2
2
) )
115
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
n o o p
o n d i s k 1 p e g 3
2
) )
116
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2
) )
117
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2
) )
118
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
move
di sk di sk2 pe g1 pe g2
2
) )
119
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
n o o p
c l e a r
d i s k 2
2
) )
120
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2
) )
121
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
n o o p
o n d i s k 1 p e g 2
2
) )
122
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
move
di sk di sk2 pe g1 pe g3
2
) )
123
(
or
(NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
2 )
(NOT
n o o p
o n d i s k 1
d i s k 2
2
) )
124
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2
) )
125
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
n o o p
o n d i s k 1
d i s k 2
2
) )
126
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
move
di sk di sk1 pe g2 pe g3
2
) )
127
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
move
di sk di sk1 pe g3 pe g2
2
) )
128
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
n o o p
o n d i s k 1 p e g 3
2
) )
129
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
move
di sk di sk2 pe g1 pe g3
2
) )
130
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
move
di sk di sk2 pe g1 pe g2
2
) )
131
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
n o o p
c l e a r
d i s k 2
2
) )
132
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2
) )
133
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 2
2 )
(NOT
n o o p
o n d i s k 1 p e g 2
2
) )
134
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
n o o p
o n d i s k 1
d i s k 2
2
) )
135
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
move
di sk di sk1 pe g2 pe g3
2
) )
136
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
n o o p
o n d i s k 1 p e g 2
2
) )
137
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2
) )
138
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
mo ve
di sk di sk2 pe g1 pe g3
2
) )
139
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
mo ve
di sk di sk2 pe g1 pe g2
2
) )
140
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
n o o p
c l e a r
d i s k 2
2
) )
141
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
move
di sk di sk1 pe g3 pe g2
2
) )
142
(
or
(NOT m o v e
d i s k d i s k 1 d i s k 2 p e g 3
2 )
(NOT
n o o p
o n d i s k 1 p e g 3
2
) )
143
(
or
(NOT mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT move
di sk di sk2 pe g1 pe g3
2
) )
144
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT
n o o p o n d i s k 2 p e g 1
2
) )
145
(
or
(NOT mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT move
di sk di sk1 pe g2 pe g3
2
) )
146
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
2
) )
147
(
or
(NOT mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT move
di sk di sk1 pe g3 pe g2
2
) )
148
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT
n o o p o n d i s k 1 d i s k 2
2
) )
149
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g2
2 )
(NOT
n o o p o n d i s k 1 p e g 2
2
) )
150
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2 )
(NOT
n o o p o n d i s k 1 p e g 3
2
) )
151
(
or
(NOT mov e
di sk di sk1 pe g3 pe g2
2 )
(NOT move
di sk di sk1 pe g2 pe g3
2
) )
152
(
or
(NOT mov e
di sk di sk1 pe g3 pe g2
2 )
(NOT move
di sk di sk2 pe g1 pe g3
2
) )
153
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2 )
(NOT
n o o p o n d i s k 1 d i s k 2
2
) )
154
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
2
) )
155
(
or
(NOT
mov e
di sk di sk1 pe g3 pe g2
2 )
(NOT
n o o p o n d i s k 1 p e g 2
2
) )
156
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
2
) )
157
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2 )
(NOT
n o o p o n d i s k 2 p e g 1
2
) )
158
(
or
(NOT mov e
di sk di sk2 pe g1 pe g3
2 )
(NOT move
di sk di sk1 pe g2 pe g3
2
) )
159
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2 )
(NOT
n o o p o n d i s k 1 d i s k 2
2
) )
160
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
2 )
(NOT
n o o p o n d i s k 1 p e g 3
2
) )
161
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
2 )
(NOT
n o o p o n d i s k 1 p e g 3
2
) )
162
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
2 )
(NOT
n o o p o n d i s k 1 p e g 2
2
) )
163
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
2 )
(NOT
m ove
di sk di sk1 pe g2 pe g3
2
) )
164
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
2 )
(NOT
n o o p
c l e a r d i s k 2
2
) )
165
(
or
(NOT n o o p
o n d i s k 1
d i s k 2
2 )
(NOT
m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2
) )
166
(
or
(NOT m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2 )
(NOT
move
di sk di sk1 pe g2 pe g3
2
) )
167
(
or
(NOT m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2 )
(NOT
n o o p
o n d i s k 1 p e g 2
2
) )
168
(
or
(NOT m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2 )
(NOT
n o o p
c l e a r
d i s k 2
2
) )
169
(
or
(NOT m o v e
d i s k d i s k 1 p e g 2 d i s k 2
2 )
(NOT
n o o p
o n d i s k 1 p e g 3
2
) )
170
(
or
(NOT
mov e
di sk di sk1 pe g2 pe g3
2 )
(NOT
n o o p o n d i s k 1 p e g 2
2
) )
171
(
or
(NOT
mov e
di sk di sk1 pe g2 pe g3
2 )
(NOT
n o o p o n d i s k 1 p e g 3
2
) )
172
(
or
(NOT n o o p
o n d i s k 1
p e g 2
2 )
(NOT
n o o p o n
d i s k 1
p e g 3 2
) )
173
(
or
n o o p o n d i s k 2 p e g 3
3
move
di sk di sk2 pe g1 pe g3
3
m ove
di sk di sk2 pe g2 pe g3 3
)
174
(
or
n o o p
o n d i s k 1 d i s k 2
3
m o v e
d i s k
d i s k 1 p e g 2 d i s k 2
3
m o v e d i s k d i s k 1
p e g 3 d i s k 2
3
)
175
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3
)
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
3
) )
176
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3
)
(NOT
m o v e
d i s k d i s k 1 p e g 3
d i s k 2
3
) )
177
(
or
(NOT mov e
di sk di sk2 pe g2 pe g3
3
)
(NOT move
di sk di sk2 pe g1 pe g3
3
) )
178
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3
)
(NOT
n o o p o n d i s k 1 d i s k 2
3
) )
179
(
or
(NOT
mov e
di sk di sk2 pe g2 pe g3
3
)
(NOT
n o o p o n d i s k 2 p e g 3
3
) )
180
(
or
(NOT
m o v e
d i s k d i s k 1
p e g 3 d i s k 2
3 )
(NOT
n o o p
o n d i s k 2
p e g 3
3
) )
5 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
181
(
or (NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3
)
(NOT
move
di sk di sk2 pe g1 pe g3
3
) )
182
(
or (NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3
)
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
3
) )
183
(
or (NOT m o v e
d i s k d i s k 1 p e g 3 d i s k 2
3 )
(NOT
n o o p o n d i s k 1 d i s k 2
3
) )
184
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
3
) )
185
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
(NOT
n o o p o n d i s k 1 d i s k 2
3
) )
186
(
or
(NOT
mov e
di sk di sk2 pe g1 pe g3
3 )
(NOT
n o o p o n d i s k 2 p e g 3 3
) )
187
(
or (NOT n o o p
o n
d i s k 1
d i s k 2
3 )
(NOT
n o o p o n d i s k 2 p e g 3 3
) )
188
(
or (NOT n o o p
o n
d i s k 1
d i s k 2
3 )
(NOT
m o v e
d i s k d i s k 1 p e g 2
d i s k 2
3
) )
189
c l e a r p e g 3
0
190
s m a l l e r
d i s k 2
p e g 2
0
191
s m a l l e r
d i s k 2
p e g 3
0
192
c l e a r d i s k 1
0
193
s m a l l e r
d i s k 1
d i s k 2 0
194
s m a l l e r
d i s k 1
p e g 2
0
195
s m a l l e r
d i s k 1
p e g 3
0
196
o n d i s k 1
d i s k 2
0
o n d i s k 2 p e g 1 0
198 c l e a r p e g 2 0
o n d i s k 2 p e g 3 3
200 o n d i s k 1 d i s k 2 3
)
4. (10 pts) Find the satisfying assignments for two-disk boolean formula using your DPLL implementation.
(a) What is the satisfying assignment?
(NOOP SMALLER DISK1 PEG2 1 . T)
2(NOOP SMALLER DISK1 PEG3 1 . T)
3(NOOP SMALLER DISK2 PEG2 1 . T)
4(NOOP SMALLER DISK2 PEG3 2 . T)
5(ON DISK1 PEG2 1 . T)
6(ON DISK1 PEG3 2)
7(NOOP ON DISK1 PEG2 2 . T)
8(NOOP CLEAR DISK2 2 . T)
(CLEAR PEG3 2)
(ON DISK1 DISK2 2)
(ON DISK1 DISK2 1)
(ON DISK2 PEG1 2)
(NOOP ON DISK1 DISK2 1)
(ON DISK2 PEG2 2)
(CLEAR PEG2 1)
(NOOP CLEAR PEG3 2)
(NOOP CLEAR PEG2 1)
(MOVE DISK DISK1 DISK2 PEG2 2)
(NOOP ON DISK2 PEG1 1 . T)
(MOVE DISK DISK1 DISK2 PEG3 2)
(MOVE DISK DISK1 DISK2 PEG2 1 . T)
(MOVE DISK DISK2 PEG1 PEG2 2)
(NOOP CLEAR DISK1 1 . T)
(MOVE DISK DISK1 PEG2 DISK2 2)
(NOOP SMALLER DISK2 PEG3 1 . T)
(NOOP ON DISK2 PEG1 2)
(SMALLER DISK2 PEG3 1 . T)
(MOVE DISK DISK1 PEG2 PEG3 2)
(ON DISK2 PEG1 1 . T)
(NOOP ON DISK1 DISK2 2)
(CLEAR DISK2 1 . T)
(MOVE DISK DISK2 PEG1 PEG3 2 . T)
(ON DISK2 PEG3 2 . T)
(NOOP SMALLER DISK1 DISK2 1 . T)
(SMALLER DISK1 DISK2 1 . T)
(NOOP SMALLER DISK1 DISK2 2 . T)
(CLEAR DISK1 1 . T)
(NOOP ON DISK2 PEG3 3 . T)
(NOOP CLEAR DISK1 2 . T)
(MOVE DISK DISK2 PEG2 PEG3 3)
(SMALLER DISK1 DISK2 2 . T)
(MOVE DISK DISK1 PEG3 DISK2 3)
6 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
(ON DISK1 PEG2 2 . T)
(MOVE DISK DISK2 PEG1 PEG3 3)
(CLEAR DISK1 2 . T)
(NOOP ON DISK1 DISK2 3)
(CLEAR DISK2 2 . T)
(MOVE DISK DISK1 PEG2 DISK2 3 . T)
(MOVE DISK DISK1 PEG3 PEG2 2)
(NOOP ON DISK1 PEG3 2)
(MOVE DISK DISK1 PEG3 DISK2 2)
(ON DISK1 PEG3 1)
(MOVE DISK DISK1 DISK2 PEG3 1)
(NOOP CLEAR PEG3 1 . T)
(CLEAR PEG3 1 . T)
(SMALLER DISK1 PEG3 0 . T)
(SMALLER DISK1 PEG2 0 . T)
(ON DISK1 DISK2 0 . T)
(SMALLER DISK1 DISK2 0 . T)
(ON DISK2 PEG1 0 . T)
(CLEAR DISK1 0 . T)
(CLEAR PEG2 0 . T)
(SMALLER DISK2 PEG3 0 . T)
(ON DISK2 PEG3 3 . T)
(SMALLER DISK2 PEG2 0 . T)
(ON DISK1 DISK2 3 . T)
(CLEAR PEG3 0 . T)
(b) What is the corresponding plan?
(NOOP SMALLER DISK1 PEG2 1 . T)
2(NOOP SMALLER DISK1 PEG3 1 . T)
3(NOOP SMALLER DISK2 PEG2 1 . T)
4(NOOP SMALLER DISK2 PEG3 2 . T)
5(ON DISK1 PEG2 1 . T)
6(NOOP ON DISK1 PEG2 2 . T)
7(NOOP CLEAR DISK2 2 . T)
8(NOOP ON DISK2 PEG1 1 . T)
9(MOVE DISK DISK1 DISK2 PEG2 1 . T)
(NOOP CLEAR DISK1 1 . T)
(NOOP SMALLER DISK2 PEG3 1 . T)
(SMALLER DISK2 PEG3 1 . T)
(ON DISK2 PEG1 1 . T)
(CLEAR DISK2 1 . T)
(MOVE DISK DISK2 PEG1 PEG3 2 . T)
(ON DISK2 PEG3 2 . T)
(NOOP SMALLER DISK1 DISK2 1 . T)
(SMALLER DISK1 DISK2 1 . T)
(NOOP SMALLER DISK1 DISK2 2 . T)
(CLEAR DISK1 1 . T)
(NOOP ON DISK2 PEG3 3 . T)
(NOOP CLEAR DISK1 2 . T)
(SMALLER DISK1 DISK2 2 . T)
(ON DISK1 PEG2 2 . T)
(CLEAR DISK1 2 . T)
(CLEAR DISK2 2 . T)
(MOVE DISK DISK1 PEG2 DISK2 3 . T)
(NOOP CLEAR PEG3 1 . T)
(CLEAR PEG3 1 . T)
(SMALLER DISK1 PEG3 0 . T)
(SMALLER DISK1 PEG2 0 . T)
(ON DISK1 DISK2 0 . T)
(SMALLER DISK1 DISK2 0 . T)
(ON DISK2 PEG1 0 . T)
(CLEAR DISK1 0 . T)
(CLEAR PEG2 0 . T)
(SMALLER DISK2 PEG3 0 . T)
(ON DISK2 PEG3 3 . T)
(SMALLER DISK2 PEG2 0 . T)
(ON DISK1 DISK2 3 . T)
(CLEAR PEG3 0 . T)
7 of 8
Names: Jonathan Evans, Hunter Johnson, Jane Lockshin, Sarah Person
Start Goal
Figure 1: Tower of Hanoi Puzzle with 3 pegs and 4 disks.
Extra Credit: Compare the performance/scalability of your DPLL implementation with one or more state-of-the-art SMT solvers such as:
Z3: https://github.com/Z3Prover/z3
CVC4: http://cvc4.cs.stanford.edu/web/
(Note: you might nd the Lisp TIME macro and SBCL’s statistical pro ler (http://www.sbcl.org/ manual/#Statistical-Profiler) useful to evaluate performance).
Extra Credit: Optimize your DPLL implementation. For example, you could improve the imple-mentation of DPLL-CHOOSE-LITERAL. Discuss the optimizations you implement and characterize the speedup (for example, using TIME or SBCL’s statistical pro ler).
8 of 8
