2026-04-13T04:10:00Zhttps://recercat.cat/oai/request
oai:recercat.cat:10459.1/572712024-12-05T21:28:11Zcom_2072_3622col_2072_479130
RECERCAT author Béjar Torres, Ramón author Cabiscol i Teixidó, Alba author Fernàndez Camon, César author Manyà Serres, Felip author Gomes, Carla 2024-12-05T21:28:11Z 2024-12-05T21:28:11Z 2016-06-23T08:15:26Z2025-01-012001 http://hdl.handle.net/10459.1/57271 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. (c) Elsevier, 2001 info:eu-repo/semantics/restrictedAccess Satisfiability Many–valued logics Extending the Reach of SAT with Many-Valued Logics article acceptedVersion