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

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JONÁŠ Martin STREJČEK Jan

Rok publikování 2020
Druh Článek ve sborníku
Konference Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www 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
Klíčová slova SMT solving; bit-vector logic; Boolector; Q3B
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.