Publication result detail

DQBDD: An Efficient BDD-Based DQBF Solver

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

Original Title

DQBDD: An Efficient BDD-Based DQBF Solver

English Title

DQBDD: An Efficient BDD-Based DQBF Solver

Type

Paper in proceedings (conference paper)

Original 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.

English 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.

Keywords

BDD, DQBF, DQBDD, solver

Key words in English

BDD, DQBF, DQBDD, solver

Authors

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

RIV year

2022

Released

02.07.2021

Publisher

Springer Verlag

Location

Heidelberg

Book

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

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

12831

State

Federal Republic of Germany

Pages from

535

Pages to

544

Pages count

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