Name
Abstract | ||
|---|---|---|
Incremental SAT solving under assumptions, introduced in Minisat, is in wide use. However, Minisat's algorithm for incremental SAT solving under assumptions has two main drawbacks which hinder performance considerably. First, it is not compliant with the highly effective and commonly used preprocessor SatELite. Second, all the assumptions are left in the formula, rather than being represented as unit clauses, propagated, and eliminated. Two previous attempts to overcome these problems solve either the first or the second of them, but not both. This paper remedies this situation by proposing a comprehensive solution for incremental SAT solving under assumptions, where SatELite is applied and all the assumptions are propagated. Our algorithm outperforms existing approaches over publicly available instances generated by a prominent industrial application in hardware validation. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-09284-3_16 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Variable elimination,Computer science,Theoretical computer science,Preprocessor,Symbolic execution,Artificial intelligence | Conference | 8561 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.39 |
References | Authors | |
10 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexander Nadel | 1 | 213 | 13.95 |
| Vadim Ryvchin | 2 | 75 | 5.68 |
| Ofer Strichman | 3 | 1071 | 63.61 |