|
Título:
|
Extending the Reach of SAT with Many-Valued Logics
|
|
Autor/a:
|
Béjar Torres, Ramón; Cabiscol i Teixidó, Alba; Fernàndez Camon, César; Manyà Serres, Felip; Gomes, Carla
|
|
Notas:
|
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. |
|
Materia(s):
|
-Satisfiability
-Many–valued logics |
|
Derechos:
|
(c) Elsevier, 2001
info:eu-repo/semantics/restrictedAccess |
|
Tipo de documento:
|
article
acceptedVersion |
|
Editor:
|
Elsevier
|
|
Compartir:
|
|
