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.