Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

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í 2016
Druh Článek ve sborníku
Konference Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-40970-2_17
Obor Informatika
Klíčová slova SMT solving; quantified bit-vector formulas; BDD
Popis We describe a new approach to deciding satisfiability of quantified bit-vector formulas using binary decision diagrams and approximations. The approach is motivated by the observation that the binary decision diagram for a quantified formula is typically significantly smaller than the diagram for the subformula within the quantifier scope. The suggested approach has been implemented and the experimental results show that it decides more benchmarks from the SMT-LIB repository than state-of-the-art SMT solvers for this theory, namely Z3 and CVC4.
Související projekty:

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