Solving dependency quantified Boolean formulas using quantifier localization

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F22%3APU145734" target="_blank" >RIV/00216305:26230/22:PU145734 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/00216224:14330/22:00128980

Výsledek na webu

<a href="https://dx.doi.org/10.1016/j.tcs.2022.03.029" target="_blank" >https://dx.doi.org/10.1016/j.tcs.2022.03.029</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.tcs.2022.03.029" target="_blank" >10.1016/j.tcs.2022.03.029</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Solving dependency quantified Boolean formulas using quantifier localization

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Solving dependency quantified Boolean formulas using quantifier localization

Popis výsledku anglicky

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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/LL1908" target="_blank" >LL1908: Efektivní konečné automaty pro automatické usuzování</a><br>

Návaznosti

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

Rok uplatnění

2022

Kód důvěrnosti údajů

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

Název periodika

Theoretical Computer Science

ISSN

0304-3975

e-ISSN

1879-2294

Svazek periodika

2022

Číslo periodika v rámci svazku

925

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

24

Strana od-do

1-24

Kód UT WoS článku

000828170700001

EID výsledku v databázi Scopus

2-s2.0-85127740569