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

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JONÁŠ Martin STREJČEK Jan

Year of publication 2020
Type Article in Proceedings
Conference Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007%2F978-3-030-51825-7_27
Doi http://dx.doi.org/10.1007/978-3-030-51825-7_27
Keywords SMT solving; bit-vector logic; Boolector; Q3B
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info