Regular-SAT: A many-valued approach to solving combinatorial problems

Abstract

Regular-SAT is a constraint programming language between CSP and SAT that—by combining many of the good properties of each paradigm—offers a good compromise between performance and expressive power. Its similarity to SAT allows us to define a uniform encoding formalism, to extend existing SAT algorithms to Regular-SAT without incurring excessive overhead in terms of computational cost, and to identify phase transition phenomena in randomly generated instances. On the other hand, Regular-SAT inherits from CSP more compact and natural encodings that maintain more the structure of the original problem. Our experimental results—using a range of benchmark problems—provide evidence that Regular-SAT offers practical computational advantages for solving combinatorial problems.

Research partially supported by projects TIN2004-07933-C03-03 and TIC2003-00950 funded by the Ministerio de Educación y Ciencia, by the DARPA contracts F30602-00-2-0530 and F30602-00-2-0596 and by the Intelligent Information Systems Institute, Cornell University, funded by AFRL/AFOSR (F49620-01-1). The second author is supported by a grant Ramón y Cajal.