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:
The problem then involves finding a sequence of moves which, when
applied to the initial configuration, lead to the goal situation.
- (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
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.
Table 1: SAT-encodings of the Towers of Hanoi problem
The instances have originally been contributed to the DIMACS benchmark
set by Bart Selman
and Henry Kautz.