A tale of two solvers: Eager and lazy approaches to bit-vectors

Liana Hadarean, Kshitij Bansal, Dejan Jovanović, Clark Barrett, Cesare Tinelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PublisherSpringer Verlag
Pages680-695
Number of pages16
Volume8559 LNCS
ISBN (Print)9783319088662
DOIs
StatePublished - 2014
Event26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna, Austria
Duration: Jul 18 2014Jul 22 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8559 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
CountryAustria
CityVienna
Period7/18/147/22/14

Fingerprint

Propositional Logic
Narrative
Comparative Analysis
Optimization Techniques
Target
Subset
Evaluation
Range of data
Architecture
Standards

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Hadarean, L., Bansal, K., Jovanović, D., Barrett, C., & Tinelli, C. (2014). A tale of two solvers: Eager and lazy approaches to bit-vectors. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings (Vol. 8559 LNCS, pp. 680-695). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_45

A tale of two solvers : Eager and lazy approaches to bit-vectors. / Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare.

Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Vol. 8559 LNCS Springer Verlag, 2014. p. 680-695 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8559 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hadarean, L, Bansal, K, Jovanović, D, Barrett, C & Tinelli, C 2014, A tale of two solvers: Eager and lazy approaches to bit-vectors. in Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. vol. 8559 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8559 LNCS, Springer Verlag, pp. 680-695, 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 7/18/14. https://doi.org/10.1007/978-3-319-08867-9_45
Hadarean L, Bansal K, Jovanović D, Barrett C, Tinelli C. A tale of two solvers: Eager and lazy approaches to bit-vectors. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Vol. 8559 LNCS. Springer Verlag. 2014. p. 680-695. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-08867-9_45
Hadarean, Liana ; Bansal, Kshitij ; Jovanović, Dejan ; Barrett, Clark ; Tinelli, Cesare. / A tale of two solvers : Eager and lazy approaches to bit-vectors. Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Vol. 8559 LNCS Springer Verlag, 2014. pp. 680-695 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{ca8e97baba9449e38f5251ff083294c3,
title = "A tale of two solvers: Eager and lazy approaches to bit-vectors",
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.",
author = "Liana Hadarean and Kshitij Bansal and Dejan Jovanović and Clark Barrett and Cesare Tinelli",
year = "2014",
doi = "10.1007/978-3-319-08867-9_45",
language = "English (US)",
isbn = "9783319088662",
volume = "8559 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "680--695",
booktitle = "Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings",

}

TY - GEN

T1 - A tale of two solvers

T2 - Eager and lazy approaches to bit-vectors

AU - Hadarean, Liana

AU - Bansal, Kshitij

AU - Jovanović, Dejan

AU - Barrett, Clark

AU - Tinelli, Cesare

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84904817199&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84904817199&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-08867-9_45

DO - 10.1007/978-3-319-08867-9_45

M3 - Conference contribution

SN - 9783319088662

VL - 8559 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 680

EP - 695

BT - Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings

PB - Springer Verlag

ER -