A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors

by Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal
Abstract:
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.
Reference:
A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (Liana Hadarean, Clark Barrett, Dejan Jovanović, Cesare Tinelli, Kshitij Bansal), In Proceedings of the 26th International Conference on Computer Aided Verification (CAV ’14) (Armin Biere, Roderick Bloem, eds.), Springer, volume 8559, 2014. (Vienna, Austria)
Bibtex Entry:
@inproceedings{HBJ+14,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/HBJ+14.pdf",
  author    = "Liana Hadarean and Clark Barrett and Dejan Jovanović and
               Cesare Tinelli and Kshitij Bansal",
  title     = "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors",
  booktitle = "Proceedings of the 26th International Conference on Computer Aided Verification (CAV '14)",
  series    = "Lecture Notes in Computer Science",
  volume    = 8559,
  publisher = "Springer",
  editor    = "Armin Biere and Roderick Bloem",
  pages     = "680--695",
  month     = jul,
  year      = 2014,
  note      = "Vienna, Austria",
  category  = "Conference Publications",
  abstract  = "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."
}

Fork me on GitHub