一句话：用量化布尔公式的电路复杂度紧刻画 QBF 归结证明大小，提出决策表模型并给出大小-宽度下界。
本文研究量化布尔公式（QBF）归结证明系统的证明复杂度。此前 Beyersdorff 与 Pich 已对 QBF Frege 系统层级给出基于电路复杂度的证明大小刻画，但 QBF 归结这一最重要情形仍未解决。本文填补该空白，给出 QBF 归结证明大小的紧电路复杂度刻画。与 Frege 情形不同，该刻画采用一种新的决策表（decision lists）电路模型；它比归结系统所用的 CNF 更强，且特别适合为 QBF 计算反模型。论文同时给出 size-width 下界。
We provide a tight characterisation of proof size in resolution for quantified Boolean formulas (QBF) by circuit complexity. Such a characterisation was previously obtained for a hierarchy of QBF Frege systems (Beyersdorff & Pich, LICS 2016), but leaving open the most important case of QBF resolution. Different from the Frege case, our characterisation uses a new version of decision lists as its circuit model, which is stronger than the CNFs the system works with. Our decision list model is well suited to compute countermodels for QBFs.
DOI 原文 ·
@inproceedings{paperbot5534,
title = {Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution},
author = {Olaf Beyersdorff and Joshua Blinkhorn and Meena Mahajan},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394793}
}