Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

JONÁŠ, Martin and Jan STREJČEK. Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams. In Nadia Creignou and Daniel Le Berre. Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference. Berlin, Heidelberg: Springer, 2016, p. 267-283. ISBN 978-3-319-40969-6. Available from: https://dx.doi.org/10.1007/978-3-319-40970-2_17.

Basic information

Original name

Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

Authors

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

Edition

Berlin, Heidelberg, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, p. 267-283, 17 pp. 2016

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

Germany

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00088245

Organization unit

Faculty of Informatics

ISBN

978-3-319-40969-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-40970-2_17

UT WoS

000387430600017

Keywords in English

SMT solving; quantified bit-vector formulas; BDD

Tags

core_A, firank_A, formela-conference

Tags

International impact, Reviewed

---

Abstract

V originále

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.

---

Links

GBP202/12/G061, research and development project	Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI) Investor: Czech Science Foundation
MUNI/A/0935/2015, interní kód MU	Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU) Investor: Masaryk University, Category A
MUNI/A/0945/2015, interní kód MU	Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V. Investor: Masaryk University, Category A