Name
Abstract | ||
|---|---|---|
We present Regular-SAT, an extension of Boolean Satisfiability based on a class of many-valued CNF 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 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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1016/S1571-0653(04)00336-1 | Electronic Notes in Discrete Mathematics |
Keywords | Field | DocType |
satisfiability,many-valued logics | Maximum satisfiability problem,Discrete mathematics,#SAT,Combinatorics,Satisfiability,Boolean satisfiability problem,Boolean expression,Mathematics | Journal |
Volume | ISSN | Citations |
9 | 1571-0653 | 3 |
PageRank | References | Authors |
0.39 | 13 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ramón Béjar | 1 | 305 | 36.72 |
| Alba Cabiscol | 2 | 31 | 3.86 |
| Cèsar Fernández | 3 | 157 | 19.19 |
| Felip Manyà | 4 | 787 | 59.52 |
| Carla P. Gomes | 5 | 2344 | 179.21 |