文章基本信息

标题：Short Proofs Are Hard to Find
本地全文：下载
作者：Ian Mertz ; Toniann Pitassi ; Yuanhao Wei 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：132
页码：1-16
DOI：10.4230/LIPIcs.ICALP.2019.84
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We obtain a streamlined proof of an important result by Alekhnovich and Razborov [Michael Alekhnovich and Alexander A. Razborov, 2008], showing that it is hard to automatize both tree-like and general Resolution. Under a different assumption than [Michael Alekhnovich and Alexander A. Razborov, 2008], our simplified proof gives improved bounds: we show under ETH that these proof systems are not automatizable in time n^f(n), whenever f(n) = o(log^{1/7 - epsilon} log n) for any epsilon > 0. Previously non-automatizability was only known for f(n) = O(1). Our proof also extends fairly straightforwardly to prove similar hardness results for PCR and Res(r).
关键词：automatizability; Resolution; SAT solvers; proof complexity