Extending the Reach of SAT with Many-Valued Logics

Thumbnail
View/Open
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) . Extending the Reach of SAT with Many-Valued Logics. Electronic Notes in Discrete Mathematics, 2001, vol. 9, p. 392-407. https://doi.org/10.1016/S1571-0653(04)00336-1.
Impact

Google Scholar logo  Google Scholar
Share
Export to Mendeley
Metadata
Show full item record
Abstract
We present Regular-SAT, an extension of Boolean Satisfiability based on a class of many-valued CNFform ulas. 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 and CSP 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 based on 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/57271
DOI
https://doi.org/10.1016/S1571-0653(04)00336-1
Is part of
Electronic Notes in Discrete Mathematics, 2001, vol. 9, p. 392-407
Collections