Name
Abstract | ||
|---|---|---|
This paper presents two new exact general purpose bit-parallel algorithms (BB-SAT and BBP-SAT) for the Boolean satisfiability problem (SAT). Based on the authors' recent successful bit-parallel algorithm for the maximum clique problem, the SAT formula is first reduced to a directed graph which is then bit encoded. As a result, search traverses a bit vector graph space. At present the encoding allows for an efficient bitwise computation of graph state transitions as well as unit clause and pure literal evaluation. Experiments carried out on a number of DIMACS instances are highly encouraging since BBP-SAT is already reasonably competitive employing just basic DPLL tactics with minor refinements. BBP-SAT is a fresh approach in an otherwise mature domain. Further additional bit encoded knowledge of the more recent successful SAT algorithms (e.g. bit parallel heuristic variable selection) should make BBP-SAT a competitive general purpose solver. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/ICTAI.2008.127 | ICTAI |
Keywords | Field | DocType |
computability,directed graphs,BB-SAT,BBP-SAT,Boolean satisfiability problem,bit vector graph space,directed graph,exact general purpose bit-parallel algorithms,graph state transitions,maximum clique problem,Boolean satisfiability,SAT,bit vector,bit-parallelism,directed graphs,exact algorithms | Bitwise operation,Parallel algorithm,Computer science,Boolean satisfiability problem,Directed graph,DPLL algorithm,Artificial intelligence,Graph state,Bit array,Clique problem,Machine learning | Conference |
Volume | ISSN | Citations |
2 | 1082-3409 | 1 |
PageRank | References | Authors |
0.38 | 9 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pablo San Segundo | 1 | 212 | 13.79 |
| Cristóbal Tapia | 2 | 1 | 0.38 |
| Julio Puente | 3 | 1 | 0.38 |
| Diego Rodríguez-losada | 4 | 156 | 11.30 |