Name
Abstract | ||
|---|---|---|
Abstract In recent years, prepositional satisfiability (SAT) has become increasingly popular outside its traditional AI and automated reasoning niche. Applications from diverse fields require efficient and sophisticated SAT solvers that can be easily integrated into existing tools. In this paper we outline a path towards an efficient library for SAT that should meet the rising standards of research and applications. Our first milestone is SIM, a library for clausal SAT based on the well known Davis-Logemann-Loveland (DLL) method. SIM provides a choice of heuristics and optimizations that are found separately in most state-of-the-art DLL-based solvers, and extensive experimental evaluation confirms that SIM's generality does not hinder its performance. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1016/S1571-0653(04)00329-4 | Electronic Notes in Discrete Mathematics |
Keywords | Field | DocType |
satisfiability,automated reasoning,sat solver | Automated reasoning,Computer science,Satisfiability,Theoretical computer science,Heuristics,Manifesto,Generality | Journal |
Volume | ISSN | Citations |
9 | 1571-0653 | 2 |
PageRank | References | Authors |
0.74 | 23 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Enrico Giunchiglia | 1 | 2380 | 164.28 |
| Massimo Narizzano | 2 | 451 | 30.41 |
| Armando Tacchella | 3 | 1448 | 108.82 |
| Moshe Y. Vardi | 4 | 13413 | 2267.07 |