DQBDD: An Efficient BDD-Based DQBF Solver

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F21%3APU142919" target="_blank" >RIV/00216305:26230/21:PU142919 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1007/978-3-030-80223-3_36" target="_blank" >http://dx.doi.org/10.1007/978-3-030-80223-3_36</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-80223-3_36" target="_blank" >10.1007/978-3-030-80223-3_36</a>

Result language

angličtina

Original language name

DQBDD: An Efficient BDD-Based DQBF Solver

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/LL1908" target="_blank" >LL1908: Efficient Finite Automata for Automated Reasoning</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2021

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

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

ISBN

—

ISSN

0302-9743

e-ISSN

—

Number of pages

10

Pages from-to

535-544

Publisher name

Springer Verlag

Place of publication

Heidelberg

Event location

Barcelona

Event date

Jul 5, 2021

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000709570900036