Regular-SAT: A many-valued approach to solving combinatorial problems
Issue date
2007Author
Manyà Serres, Felip
Gomes, Carla
Suggested citation
Béjar Torres, Ramón;
Manyà Serres, Felip;
Cabiscol i Teixidó, Alba;
Fernàndez Camon, César;
Gomes, Carla;
.
(2007)
.
Regular-SAT: A many-valued approach to solving combinatorial problems.
Discrete Applied Mathematics, 2007, vol. 155, núm. 12, p. 1613-1626.
https://doi.org/10.1016/j.dam.2005.10.020.
Metadata
Show full item recordAbstract
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.