Detail publikace

Solving dependency quantified Boolean formulas using quantifier localization

SÍČ, J.; GE-ERNST, A.; SCHOLL, C.; WIMMER, R. Solving dependency quantified Boolean formulas using quantifier localization. Theoretical Computer Science, 2022, vol. 2022, no. 925, p. 1-24. ISSN: 0304-3975.
Název česky
Řešení závislostně kvantifikovaných Booleovských formulí pomocí lokalizace kvantifikátorů
Typ
článek v časopise
Jazyk
anglicky
Autoři
Síč Juraj, Mgr. (UITS)
Ge-Ernst Aile
Scholl Christoph
Wimmer Ralf
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
DOI
10.1016/j.tcs.2022.03.029
UT WoS
000828170700001
EID Scopus
2-s2.0-85127740569
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"
}
Nahoru