Effective CNF Encodings for the Towers of Hanoi
Ruben Martins, Inês Lynce · 2008
Abstract. One of the most well-known CNF benchmark encodes the problem of the Towers of Hanoi. This benchmark is available from SATlib and has been part of the set of problem instances used in more than one edition of the SAT competition. The existing CNF instances build upon an encoding using the STRIPS language. Although the available instances (ranging from 4 to 6 disks) are hard to solve for most of the solvers, we introduce improvements over the existing encodings and present a new CNF encoding that makes these problem instances trivial to solve using only unit propagation. This new encoding is also based on the STRIPS language and makes it possible to solve the problem of 18 disks in a reasonable amount of time. 1