Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

JONÁŠ, Martin a 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, s. 267-283. ISBN 978-3-319-40969-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-40970-2_17.

Základní údaje

Originální název

Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams

Autoři

JONÁŠ, Martin (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

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

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088245

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-40969-6

ISSN

DOI

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

UT WoS

000387430600017

Klíčová slova anglicky

SMT solving; quantified bit-vector formulas; BDD

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

---

Návaznosti

GBP202/12/G061, projekt VaV	Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI) Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
MUNI/A/0935/2015, interní kód MU	Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0945/2015, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V. Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty