文章基本信息

标题：Strong ETH and Resolution via Games and the Multiplicity of Strategies
本地全文：下载
作者：Ilario Bonacina ; Navid Talebanfard
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：43
页码：248-257
DOI：10.4230/LIPIcs.IPEC.2015.248
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We consider a restriction of the Resolution proof system in which at most a fixed number of variables can be resolved more than once along each refutation path. This system lies between regular Resolution, in which no variable can be resolved more than once along any path, and general Resolution where there is no restriction on the number of such variables. We show that when the number of re-resolved variables is not too large, this proof system is consistent with the Strong Exponential Time Hypothesis (SETH). More precisely for large n and k we show that there are unsatisfiable k-CNF formulas which require Resolution refutations of size 2^{(1 - epsilon_k)n}, where n is the number of variables and epsilon_k=~O(k^{-1/5}), whenever in each refutation path we only allow at most ~O(k^{-1/5})n variables to be resolved multiple times. However, these re-resolved variables along different paths do not need to be the same. Prior to this work, the strongest proof system shown to be consistent with SETH was regular Resolution [Beck and Impagliazzo, STOC'13]. This work strengthens that result and gives a different and conceptually simpler game-theoretic proof for the case of regular Resolution.
关键词：Strong Exponential Time Hypothesis; resolution; proof systems