DQBDD: An Efficient BDD-Based DQBF Solver

EasyChair Preprint 5948

Abstract

This paper introduces a new DQBF solver called DQBDD, which is based on quantifier localization, quantifier elimination, and translation of formulas to binary decision diagrams (BDDs). In 2020, DQBDD participated for the first time in the Competitive Evaluation of QBF Solvers (QBFEVAL’20) and won the DQBF Solvers Track by a large margin.

Keyphrases: BDD, Binary Decision Diagram, DQBDD, DQBF, Quantifier Localization, bdd based solver, dependency quantified Boolean formula, quantifier elimination, solver

@booklet{EasyChair:5948,
  author    = {Juraj Síč and Jan Strejček},
  title     = {DQBDD: An Efficient BDD-Based DQBF Solver},
  howpublished = {EasyChair Preprint 5948},
  year      = {EasyChair, 2021}}