Detail publikace

DQBDD: An Efficient BDD-Based DQBF Solver

SÍČ Juraj a 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, s. 535-544. ISSN 0302-9743. Dostupné z: http://dx.doi.org/10.1007/978-3-030-80223-3_36
Název česky
DQBDD: efektivní DQBF řešič založen na BDD
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Síč Juraj, Mgr. (UITS FIT VUT)
Strejček Jan, prof. RNDr., Ph.D. (FI MUNI)
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, DE
DOI
UT WoS
000709570900036
EID Scopus
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"
}
Nahoru