Extending the Reach of SAT with Many-Valued Logics
Issue date
2001Author
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.
Metadata
Show full item recordAbstract
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.
Is part of
Electronic Notes in Discrete Mathematics, 2001, vol. 9, p. 392-407European research projects
Related items
Showing items related by title, author, creator and subject.
-
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 (Elsevier, 2007)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 ... -
Generating Hard Satisfiable Scheduling Instances
Argelich Romà, Josep; Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla (European Conference on Planning, 2013)We present a random generator of partially complete round robin timetables that produces exclusively satisfiable instances, and provide experimental evidence that there is an easy-hard-easy pattern in the computational ... -
Capturing Structure with Satisfiability
Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla (Springer Verlag, 2001)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 ...