Detail výsledku

DQBDD: An Efficient BDD-Based DQBF Solver

SÍČ, J.; STREJČEK, J. DQBDD: An Efficient BDD-Based DQBF Solver. In Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2021. no. 12831, p. 535-544. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Síč Juraj, Mgr., UITS (FIT)
Strejček Jan, prof. RNDr., Ph.D., FIT (FIT)
Abstrakt

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.

Klíčová slova

BDD, DQBF, DQBDD, solver

URL
Rok
2021
Strany
535–544
Časopis
Lecture Notes in Computer Science, č. 12831, ISSN 0302-9743
Sborník
Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing
Konference
24th International Conference on Theory and Applications of Satisfiability Testing
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-030-80223-3_36
UT WoS
000709570900036
EID Scopus
2-s2.0-85112166650
BibTeX 
@inproceedings{BUT175796,
  author="Juraj {Síč} and Jan {Strejček}",
  title="DQBDD: An Efficient BDD-Based DQBF Solver",
  booktitle="Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing",
  year="2021",
  journal="Lecture Notes in Computer Science",
  number="12831",
  pages="535--544",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-030-80223-3\{_}36",
  issn="0302-9743",
  url="http://dx.doi.org/10.1007/978-3-030-80223-3_36"
}
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
Spolehlivé, bezpečné a efektivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-20-6427, zahájení: 2020-03-01, ukončení: 2023-02-28, ukončen
Výzkumné skupiny
Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru