Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I
Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I
复制标题
自动机、语言和编程 - 第 42 届国际学术讨论会，ICALP 2015，日本京都，2015 年 7 月 6-10 日，会议记录，第一部分
DOI：
10.1007/978-3-662-47672-7_15
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Beyersdorff O
中科院分区：
文献类型：
--
作者：
Beyersdorff O
与经典的证明复杂性形成鲜明对比的是，我们目前缺乏QBF证明系统的下界技术。在本文中，我们建立了可行的插值技术的所有分辨率为基础的QBF系统，无论是建模CDCL或基于扩展的解决方案。这既为QBF证明系统提供了第一个通用的下界方法，也大大扩展了经典可行插值的范围。我们应用我们的技术，以获得新的指数下界的所有分辨率为基础的QBF系统的一类新的QBF公式的基础上团问题。最后，我们展示了可行的插值与最近建立的基于策略提取的下限方法的关系。
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF proof systems as well as largely extends the scope of classical feasible interpolation. We apply our technique to obtain new exponential lower bounds to all resolution-based QBF systems for a new class of QBF formulas based on the clique problem. Finally, we show how feasible interpolation relates to the recently established lower bound method based on strategy extraction.