Detail publikačního výsledku

DQBDD: An Efficient BDD-Based DQBF Solver

SÍČ, J.; STREJČEK, J.

Originální název

DQBDD: An Efficient BDD-Based DQBF Solver

Anglický název

DQBDD: An Efficient BDD-Based DQBF Solver

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální 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.

Anglický 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

Klíčová slova v angličtině

BDD, DQBF, DQBDD, solver

Autoři

SÍČ, J.; STREJČEK, J.

Rok RIV

2022

Vydáno

02.07.2021

Nakladatel

Springer Verlag

Místo

Heidelberg

Kniha

Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

12831

Stát

Spolková republika Německo

Strany od

535

Strany do

544

Strany počet

10

URL

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

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"
}