A game characterisation of tree-like Q-Resolution size
A game characterisation of tree-like Q-Resolution size
复制标题
DOI：
10.1016/j.jcss.2016.11.011
复制
发表时间：
2019-09-01
影响因子：
1.1
通讯作者：
Sreenivasaiah, Karteek
中科院分区：
文献类型：
--
作者：
Beyersdorff, Olaf;Chew, Leroy;Sreenivasaiah, Karteek
我们提供了一个表征的证明在树型Q-分辨率和树型QU-分辨率的证明大小的证明延迟游戏，这是由一个类似的表征的经典树型分辨率的证明大小的启发。这给出了一个第一次成功的转让之一的下界技术的经典证明系统的QBF证明系统。我们应用我们的技术来显示三类树形Q分辨率公式的难度。特别地，我们给出了Beyersdorff等人（2015）[10]的树型Q-分辨率的奇偶公式和Kleine Buning等人（1995）[29]的树型QU-分辨率公式的硬度证明。(C)2017作者爱思唯尔公司出版
We provide a characterisation for the size of proofs in tree-like Q-Resolution and tree-like QU-Resolution by a Prover-Delayer game, which is inspired by a similar characterisation for the proof size in classical tree-like Resolution. This gives one of the first successful transfers of one of the lower bound techniques for classical proof systems to QBF proof systems. We apply our technique to show the hardness of three classes of formulas for tree-like Q-Resolution. In particular, we give a proof of the hardness of the parity formulas from Beyersdorff et al. (2015) [10] for tree-like Q-Resolution and of the formulas of Kleine Buning et al. (1995) [29] for tree-like QU-Resolution. (C) 2017 The Authors. Published by Elsevier Inc.