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.

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  718  4934  yes 
hanoi5.cnf 1931  14468  yes 

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.