Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width
Reductions and Extensions

D 2020

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

JONÁŠ, Martin and Jan STREJČEK

Basic information

Original name

Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Authors

JONÁŠ, Martin (203 Czech Republic) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

Cham (Switzerland), Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, p. 378-393, 16 pp. 2020

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/20:00114392

Organization unit

Faculty of Informatics

ISBN

978-3-030-51824-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-51825-7_27

UT WoS

000711645300027

Keywords in English

SMT solving; bit-vector logic; Boolector; Q3B

Abstract

V originále

Recent experiments have shown that satisfiability of a quantified bit-vector formula coming from practical applications almost never changes after reducing all bit-widths in the formula to a small number of bits. This paper proposes a novel technique based on this observation. Roughly speaking, a given quantified bit-vector formula is reduced and sent to a solver, an obtained model is then extended to the original bit-widths and verified against the original formula. We also present an experimental evaluation demonstrating that this technique can significantly improve the performance of state-of-the-art smt solvers Boolector, CVC4, and Q3B on quantified bit-vector formulas from the smt-lib repository.

Links

GA18-02177S, research and development project

Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor: Czech Science Foundation

Citovat

JONÁŠ, Martin and Jan STREJČEK. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Online. In Luca Pulina and Martina Seidl. Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings. Cham (Switzerland): Springer, 2020, p. 378-393. ISBN 978-3-030-51824-0. Available from: https://dx.doi.org/10.1007/978-3-030-51825-7_27.

@inproceedings{1686869,
   author = {Jonáš, Martin and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-51825-7_27},
   editor = {Luca Pulina and Martina Seidl},
   keywords = {SMT solving; bit-vector logic; Boolector; Q3B},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-51824-0},
   pages = {378-393},
   publisher = {Springer},
   title = {Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27},
   year = {2020}
}

TY  - JOUR
ID  - 1686869
AU  - Jonáš, Martin - Strejček, Jan
PY  - 2020
TI  - Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030518240
KW  - SMT solving
KW  - bit-vector logic
KW  - Boolector
KW  - Q3B
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27
L2  - https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27
N2  - Recent experiments have shown that satisfiability of a quantified bit-vector formula coming from practical applications almost never changes after reducing all bit-widths in the formula to a small number of bits. This paper proposes a novel technique based on this observation. Roughly speaking, a given quantified bit-vector formula is reduced and sent to a solver, an obtained model is then extended to the original bit-widths and verified against the original formula. We also present an experimental evaluation demonstrating that this technique can significantly improve the performance of state-of-the-art smt solvers Boolector, CVC4, and Q3B on quantified bit-vector formulas from the smt-lib repository.
ER  -

JONÁŠ, Martin and Jan STREJČEK. Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions. Online. In Luca Pulina and Martina Seidl. \textit{Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings}. Cham (Switzerland): Springer, 2020, p.~378-393. ISBN~978-3-030-51824-0. Available from: https://dx.doi.org/10.1007/978-3-030-51825-7\_{}27.

Detailed Information on Publication Record