Capturing Structure with Satisfiability

Abstract

We present Regular-SAT, an extension of Boolean Satisfiability basedon a class of many-valuedCNF formulas. Regular-SAT shares many properties with Boolean SAT, which allows us to generalize some of the best known SAT results and apply them to Regular-SAT. In addition, Regular-SAT has a number of advantages over Boolean SAT. Most importantly, it produces more compact encodings that capture problem structure more naturally. Furthermore, its simplicity allows us to develop Regular-SAT solvers that are competitive with SAT andCSP procedures. We present a detailed performance analysis of Regular-SAT on several benchmark domains. These results show a clear computational advantage of using a Regular-SAT approach over a pure Boolean SAT or CSP approach, at least on the domains under consideration. We therefore believe that an approach basedon Regular-SAT provides a compelling intermediate approach between SAT and CSPs, bringing together some of the best features of each paradigm.

This research was partially funded by the DARPA contracts F30602-00-2-0530 and F30602-00-2-0596, and project CICYT TIC96-1038-C04-03. The fourth author was supported by the “Secretar´ıa de Estado de Educaci´on y Universidades”. This research was also partially funded by the Intelligent Information Systems Institute, Cornell University, funded by AFRL/AFOSR (F49620-01-1).