Capturing Structure with Satisfiability
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)
.
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.
Metadata
Show full item recordAbstract
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.
Is part of
Lecture Notes in Computer Science, 2001, vol. 2239, p. 137-152European research projects
Related items
Showing items related by title, author, creator and subject.
-
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 ... -
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 ... -
Extending the Reach of SAT with Many-Valued Logics
Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla (Elsevier, 2001)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 ...