Detail publikace

Solving dependency quantified Boolean formulas using quantifier localization

GE-ERNST Aile, SCHOLL Christoph, SÍČ Juraj a WIMMER Ralf. Solving dependency quantified Boolean formulas using quantifier localization. Theoretical Computer Science, roč. 2022, č. 925, s. 1-24. ISSN 0304-3975. Dostupné z: https://dx.doi.org/10.1016/j.tcs.2022.03.029
Název česky
Řešení závislostně kvantifikovaných Booleovských formulí pomocí lokalizace kvantifikátorů
Typ
článek v časopise
Jazyk
angličtina
Autoři
Ge-Ernst Aile (UNI Freiburg)
Scholl Christoph (UNI Freiburg)
Síč Juraj, Mgr. (UITS FIT VUT)
Wimmer Ralf (UNI Freiburg)
URL
Klíčová slova

Závislostně kvantifikované booleovské formule, Henkinův kvantifikátor, Lokalizace kvantifikátoru, Splnitelnost, Technologie solveru

Abstrakt

Závislostně kvantifikované Booleovské formule (DQBF) jsou mocným formalismem, který zastřešuje kvantifikované Booleovské formule (QBF) a umožňuje explicitní specifikaci závislostí existenčních proměnných na univerzálních proměnných. V posledních několika letech se pod vlivem potřeb různých aplikací, které lze přirozeným, kompaktním a elegantním způsobem zakódovat pomocí DQBF, rozvinul výzkum řešení DQBF. Výzkum se však soustředil na uzavřené DQBF v prenexové formě (kde jsou všechny kvantifikátory umístěny před výrokovou formulí), zatímco neprenexové DQBF nebyly v literatuře téměř studovány. V tomto příspěvku podáváme formální definici syntaxe a sémantiky neuzavřených neprenektických DQBF a dokazujeme užitečné vlastnosti umožňující lokalizaci kvantifikátorů. Navíc využíváme naši teorii tím, že integrujeme lokalizaci kvantifikátorů do moderního řešitele DQBF. Experimenty s prenexovými DQBF benchmarky, včetně všech instancí ze soutěží QBFEVAL'18-'20, jasně ukazují, že lokalizace kvantifikátorů se v tomto kontextu vyplatí.

Rok
2022
Strany
1-24
Časopis
Theoretical Computer Science, roč. 2022, č. 925, ISSN 0304-3975
Vydavatel
Elsevier Science
DOI
10.1016/j.tcs.2022.03.029
UT WoS
000828170700001
EID Scopus
2-s2.0-85127740569
BibTeX 
@ARTICLE{FITPUB12801,
   author = "Aile Ge-Ernst and Christoph Scholl and Juraj S\'{i}\v{c} and Ralf Wimmer",
   title = "Solving dependency quantified Boolean formulas using quantifier localization",
   pages = "1--24",
   journal = "Theoretical Computer Science",
   volume = 2022,
   number = 925,
   year = 2022,
   ISSN = "0304-3975",
   doi = "10.1016/j.tcs.2022.03.029",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12801"
}
Nahoru