一句话：提出基于成本与容量的语义技术，为多个 QBF 证明系统证明指数级下界，包括随机 QBF。
本文研究量化布尔公式（QBF）证明系统的证明规模下界。作者形式化了由命题证明系统加入全称归约得到 QBF 证明系统的构造，并提出仅依赖两个语义度量的新技术：QBF 的成本（cost）与证明的容量（capacity）。通过分析若干 QBF 系统中证明的容量，可将下界归结为成本。应用上，作者为表示等式的简单 QBF 族证明指数下界；核心结果是对一类随机生成的 QBF 以高概率证明指数下界，这是该类型首个“真正的”下界，适用于 resolution、Cutting Planes 与 Polynomial Calculus 的 QBF 类比。该技术还为 Kleine Büning、Karpinski 和 Flögel 的著名公式给出简单难度证明。
As a natural extension of the SAT problem, an array of proof systems for quantified Boolean formulas (QBF) have been proposed, many of which extend a propositional proof system to handle universal quantification. By formalising the construction of the QBF proof system obtained from a propositional proof system by adding universal reduction (Beyersdorff, Bonacina & Chew, ITCS `16), we present a new technique for proving proof-size lower bounds in these systems. The technique relies only on two semantic measures: the cost of a QBF, and the capacity of a proof. By examining the capacity of proofs in several QBF systems, we are able to use the technique to obtain lower bounds based on cost alone. As applications of the technique, we first prove exponential lower bounds for a new family of simple QBFs representing equality. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first `genuine' lower bounds of this kind, which apply to the QBF analogues of resolution, Cutting Planes, and Polynomial Calculus. Finally, we employ the technique to give a simple proof of hardness for the prominent formulas of Kleine B\"uning, Karpinski and Fl\"ogel.
@article{paperbot828,
title = {Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs},
author = {Olaf Beyersdorff and Joshua Blinkhorn and Luke Hinde},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:13)2019}
}