DQBDD: An Efficient BDD-Based DQBF Solver

SÍČ, Juraj a Jan STREJČEK. DQBDD: An Efficient BDD-Based DQBF Solver. Online. In Chu-Min Li and Felip Manyà. Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings. Cham (Switzerland): Springer, 2021, s. 535-544. ISBN 978-3-030-80222-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-80223-3_36.

Základní údaje

Originální název

DQBDD: An Efficient BDD-Based DQBF Solver

Autoři

SÍČ, Juraj (703 Slovensko) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Switzerland), Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, od s. 535-544, 10 s. 2021

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/21:00122203

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-80222-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-80223-3_36

UT WoS

000709570900036

Klíčová slova anglicky

dependency quantified Boolean formulas; DQBF; binary decision diagrams; BDD; DQBDD

Štítky

core_A, firank_A, formela-aut, satisfiability, SMT solving

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

This paper introduces a new DQBF solver called DQBDD, which is based on quantifier localization, quantifier elimination, and translation of formulas to binary decision diagrams (BDDs). In 2020, DQBDD participated for the first time in the Competitive Evaluation of QBF Solvers (QBFEVAL’20) and won the DQBF Solvers Track by a large margin.