Detail publikace

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. p. 535-544. ISSN: 0302-9743.
Název česky
DQBDD: efektivní DQBF řešič založen na BDD
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Síč Juraj, Mgr. (UITS)
Strejček Jan, prof. RNDr., Ph.D.
URL
Klíčová slova

BDD, DQBF, DQBDD, řešič

Abstrakt

Tento článek představuje nový řešič DQBF s názvem DQBF, který je založen na lokalizaci kvantifikátorů, eliminaci kvantifikátorů a překladu formulí do binárních rozhodovacích diagramů (BDD). V roce 2020 se DQBF poprvé zúčastnil soutěže Competitive Evaluation of QBF Solvers (QBFEVAL'20) a s velkým náskokem zvítězil v kategorii DQBF Solvers Track.

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, Barcelona, ES
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"
}
Nahoru