Name
Abstract | ||
|---|---|---|
This paper proposes an efficient algorithm for the systematic learning of implications. This is done as part of a new search and restart strategy in the SAT solver. We evaluate the new algorithm within a number of applications, including BMC and induction with invariant strengthening for equivalence checking. We provide extensive experimental evidence attesting to a speedup of one and often two orders of magnitude with our algorithm, on a representative set of industrial and publicly available test suites, as compared to a basic version of invariant strengthening. Moreover, we show that the new invariant strengthening algorithm alone performs better than induction and interpolation, and that the absolutely best result is achieved when it is combined with interpolation. In addition, we experimentally demonstrate the superiority of an application of our new algorithm to BMC. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-34188-5_9 | Haifa Verification Conference |
Keywords | Field | DocType |
invariant strengthening,equivalence checking,new search,available test suite,new invariant,implicative simultaneous satisfiability,best result,basic version,sat solver,new algorithm,efficient algorithm | Formal equivalence checking,Computer science,Boolean satisfiability problem,Satisfiability,Interpolation,Algorithm,Theoretical computer science,Invariant (mathematics),Order of magnitude,Speedup | Conference |
Citations | PageRank | References |
6 | 0.45 | 19 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zurab Khasidashvili | 1 | 307 | 25.40 |
| Alexander Nadel | 2 | 213 | 13.95 |