“A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors” by Liana Hadarean, Clark Barrett, Dejan Jovanovic, Cesare Tinelli, and Kshitij Bansal. In Proceedings of the 26^th International Conference on Computer Aided Verification (CAV '14), (Armin Biere and Roderick Bloem, eds.), July 2014, pp. 680-695. Vienna, Austria.
The standard method for deciding bit-vector constraints is via eager reduction to propositional logic. This is usually done after first applying powerful rewrite techniques. While often efficient in practice, this method does not scale on problems for which top-level rewrites cannot reduce the problem size sufficiently. A lazy solver can target such problems by doing many satisfiability checks, each of which only reasons about a small subset of the problem. In addition, the lazy approach enables a wide range of optimization techniques that are not available to the eager approach. In this paper we describe the architecture and features of our lazy solver (LBV). We provide a comparative analysis of the eager and lazy approaches, and show how they are complementary in terms of the types of problems they can efficiently solve. For this reason, we propose a portfolio approach that runs a lazy and eager solver in parallel. Our empirical evaluation shows that the lazy solver can solve problems none of the eager solvers can and that the portfolio solver outperforms other solvers both in terms of total number of problems solved and the time taken to solve them.
BibTeX entry:
@inproceedings{HBJ+14,
author = {Liana Hadarean and Clark Barrett and Dejan Jovanovi{\'c} and
Cesare Tinelli and Kshitij Bansal},
editor = {Armin Biere and Roderick Bloem},
title = {A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors},
booktitle = {Proceedings of the {\it 26^{th}} International Conference
on Computer Aided Verification (CAV '14)},
series = {Lecture Notes in Computer Science},
volume = {8559},
pages = {680--695},
publisher = {Springer},
month = jul,
year = {2014},
note = {Vienna, Austria},
url = {http://theory.stanford.edu/~barrett/pubs/HBJ+14.pdf}
}
(This webpage was created with bibtex2web.)