Publication Details

DQBDD: An Efficient BDD-Based DQBF Solver

SÍČ Juraj and STREJČEK Jan. DQBDD: An Efficient BDD-Based DQBF Solver. In: Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing. Heidelberg: Springer Verlag, 2021, pp. 535-544. ISSN 0302-9743. Available from: http://dx.doi.org/10.1007/978-3-030-80223-3_36
Czech title
DQBDD: efektivní DQBF řešič založen na BDD
Type
conference paper
Language
english
Authors
Síč Juraj, Mgr. (DITS FIT BUT)
Strejček Jan, prof. RNDr., Ph.D. (FI MUNI)
URL
Keywords

BDD, DQBF, DQBDD, solver

Abstract

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

Published
2021
Pages
535-544
Journal
Lecture Notes in Computer Science, no. 12831, ISSN 0302-9743
Proceedings
Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing
Conference
24th International Conference on Theory and Applications of Satisfiability Testing, Barcelona, ES
Publisher
Springer Verlag
Place
Heidelberg, DE
DOI
10.1007/978-3-030-80223-3_36
UT WoS
000709570900036
EID Scopus
2-s2.0-85112166650
BibTeX 
@INPROCEEDINGS{FITPUB12526,
   author = "Juraj S\'{i}\v{c} and Jan Strej\v{c}ek",
   title = "DQBDD: An Efficient BDD-Based DQBF Solver",
   pages = "535--544",
   booktitle = "Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing",
   journal = "Lecture Notes in Computer Science",
   number = 12831,
   year = 2021,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-030-80223-3\_36",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12526"
}
Back to top