大小、成本和容量：一种用于难度随机QBF的语义技术
摘要：量化布尔公式（QBF）的证明系统是SAT问题的自然延伸，许多证明系统扩展了命题证明系统以处理全称量化。通过将从命题证明系统中添加全称约简获得的QBF证明系统构建形式化（Beyersdorff，Bonacina＆Chew，ITCS'16），我们提出了一种新技术来证明这些系统中证明大小的下界。该技术仅依赖于两个语义度量：QBF的成本和证明的容量。通过检查几个QBF系统中的证明容量，我们能够使用这种技术仅基于成本获得下界。 作为技术的应用，我们首先证明了一个新的简单QBF族表示相等性的指数下界。主要应用是以高概率证明一类随机生成的QBF的指数下界，这是首次应用于解析、割平面和多项式演算的“真正的”此类下界。 最后，我们使用这种技术简单证明了Kleine B"uning，Karpinski和Fl"ogel的著名公式的难度。
作者：Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde
论文ID：1712.03626
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22