Detail publikačního výsledku

Solving dependency quantified Boolean formulas using quantifier localization

SÍČ, J.; GE-ERNST, A.; SCHOLL, C.; WIMMER, R.

Originální název

Solving dependency quantified Boolean formulas using quantifier localization

Anglický název

Solving dependency quantified Boolean formulas using quantifier localization

Druh

Článek WoS

Originální abstrakt

Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), while non-prenex DQBFs have almost not been studied in the literature. In this paper, we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks, including all instances from the QBFEVAL'18'20 competitions, clearly show that quantifier localization pays off in this context.

Anglický abstrakt

Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), while non-prenex DQBFs have almost not been studied in the literature. In this paper, we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks, including all instances from the QBFEVAL'18'20 competitions, clearly show that quantifier localization pays off in this context.

Klíčová slova

Dependency quantified Boolean formulas, Henkin quantifier, Quantifier localization, Satisfiability, Solver technology

Klíčová slova v angličtině

Dependency quantified Boolean formulas, Henkin quantifier, Quantifier localization, Satisfiability, Solver technology

Autoři

SÍČ, J.; GE-ERNST, A.; SCHOLL, C.; WIMMER, R.

Rok RIV

2023

Vydáno

10.08.2022

ISSN

0304-3975

Periodikum

Theoretical Computer Science

Svazek

2022

Číslo

925

Stát

Nizozemsko

Strany od

1

Strany do

24

Strany počet

24

URL

https://dx.doi.org/10.1016/j.tcs.2022.03.029

BibTex

@article{BUT179364,
  author="Juraj {Síč} and Aile {Ge-Ernst} and Christoph {Scholl} and Ralf {Wimmer}",
  title="Solving dependency quantified Boolean formulas using quantifier localization",
  journal="Theoretical Computer Science",
  year="2022",
  volume="2022",
  number="925",
  pages="1--24",
  doi="10.1016/j.tcs.2022.03.029",
  issn="0304-3975",
  url="https://dx.doi.org/10.1016/j.tcs.2022.03.029"
}