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

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.