SAT-encoded Towers of Hanoi Problems
The Towers of Hanoi is the following well known problem:
One is given three pins and a stack of n discs of decreasing
diameter on one of the pins. The problem then is to transfer these
n discs to one of the other pins according to the following rules:
- (1) A move places a disc on another pin
- (2) Only one disc at a time can be moved
- (3) A disc may not be placed on top of a smaller disc
The problem then involves finding a sequence of moves which, when
applied to the initial configuration, lead to the goal situation.
Benchmark instances
There are two SAT-encoded instances available from the original DIMACS
challenge set; both instances had been contributed by Bart Selman and
Henry Kautz. The instances involve 4 and 5 discs, respectively. The
instances are described in Table 1; they belong to some of the hardest
instances of our benchmark suit.
instance |
discs |
vars |
clauses |
satisfiable? |
hanoi4.cnf |
4 |
718 |
4934 |
yes |
hanoi5.cnf |
5 |
1931 |
14468 |
yes |
Table 1: SAT-encodings of the Towers of Hanoi problem
Acknowledgements
The instances have originally been contributed to the DIMACS benchmark
set by Bart Selman
and Henry Kautz.