Name
Abstract | ||
|---|---|---|
Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-34188-5_8 | Haifa Verification Conference |
Keywords | Field | DocType |
hard competition benchmarks,sat solvers,sat problem,conflict-driven solvers,practical sat,hard instance,two-phase approach,hybrid approach,cdcl sat solvers,new approach,conflict-driven solver | Computer science,Satisfiability,Theoretical computer science,Solver,Formal verification,Scalability,Cube | Conference |
Citations | PageRank | References |
37 | 1.28 | 13 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marijn J. H. Heule | 1 | 605 | 49.51 |
| Oliver Kullmann | 2 | 527 | 33.85 |
| Siert Wieringa | 3 | 88 | 4.99 |
| Armin Biere | 4 | 4106 | 245.11 |