一句话：为所有基于归结的 QBF 证明系统建立可行插值技术，并给出首个通用指数下界方法。
经典证明复杂度已有多种下界技术，但 QBF 证明系统长期缺乏通用下界方法。本文为所有基于归结的 QBF 证明系统建立可行插值技术，涵盖以 CDCL 和 expansion-based 求解为模型的系统，显著扩展了经典可行插值的适用范围。作者将该技术应用于一类基于团问题的新 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BeyersdorffCMS17,
title = {Feasible Interpolation for QBF Resolution Calculi},
author = {Olaf Beyersdorff and Leroy Chew and Meena Mahajan and Anil Shukla},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:7)2017}
}