Capturing Structure with Satisfiability

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

doi:https://doi.org/10.1007/3-540-45578-7_10

View/Open

007314.pdf (734.0Kb)
Sol·licita una còpia

Issue date

2001

Author

Béjar Torres, Ramón

Cabiscol i Teixidó, Alba

Fernàndez Camon, César

Manyà Serres, Felip

Gomes, Carla

Suggested citation

Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla; . (2001) . Capturing Structure with Satisfiability. Lecture Notes in Computer Science, 2001, vol. 2239, p. 137-152. https://doi.org/10.1007/3-540-45578-7_10.

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.

URI

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

DOI

https://doi.org/10.1007/3-540-45578-7_10

Is part of

Lecture Notes in Computer Science, 2001, vol. 2239, p. 137-152