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

Béjar Torres, Ramón; Manyà Serres, Felip; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Gomes, Carla

doi:https://doi.org/10.1016/j.dam.2005.10.020

View/Open

011049.pdf (411.3Kb)
Sol·licita una còpia

Issue date

2007

Author

Béjar Torres, Ramón

Manyà Serres, Felip

Cabiscol i Teixidó, Alba

Fernàndez Camon, César

Gomes, Carla

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.

URI

http://hdl.handle.net/10459.1/57349

DOI

https://doi.org/10.1016/j.dam.2005.10.020

Is part of

Discrete Applied Mathematics, 2007, vol. 155, núm. 12, p. 1613-1626