Why are Proof Complexity Lower Bounds Hard?

被引:8
作者
Pich, Jan [1 ]
Santhanam, Rahul [1 ]
机构
[1] Univ Oxford, Dept Comp Sci, Oxford, England
来源
2019 IEEE 60TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE (FOCS 2019) | 2019年
基金
欧洲研究理事会;
关键词
Computational complexity; proof complexity; circuit lower bounds; barriers; PSEUDORANDOM GENERATORS; PROVABILITY; RESOLUTION; SIZE;
D O I
10.1109/FOCS.2019.00080
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We formalize and study the question of whether there are inherent difficulties to showing lower bounds on propositional proof complexity. We establish the following unconditional result: Propositional proof systems cannot efficiently show that truth tables of random Boolean functions lack polynomial size non-uniform proofs of hardness. Assuming a conjecture of Rudich, propositional proof systems also cannot efficiently show that random k-CNFs of linear density lack polynomial size non-uniform proofs of unsatisfiability. Since the statements in question assert the average-case hardness of standard NP problems (MCSP and 3-SAT respectively) against co-nondeterministic circuits for natural distributions, one interpretation of our result is that propositional proof systems are inherently incapable of efficiently proving strong complexity lower bounds in our formalization. Another interpretation is that an analogue of the Razborov-Rudich 'natural proofs' barrier holds in proof complexity: under reasonable hardness assumptions, there are natural distributions on hard tautologies for which it is infeasible to show proof complexity lower bounds for strong enough proof systems. For the specific case of the Extended Frege (EF) propositional proof system, we show that at least one of the following cases holds: (1) EF has no efficient proofs of superpolynomial circuit lower bound tautologies for any Boolean function or (2) There is an explicit family of tautologies of each length such that under reasonable hardness assumptions, most tautologies are hard but no propositional proof system can efficiently establish hardness for most tautologies in the family. Thus, under reasonable hardness assumptions, either the Circuit Lower Bounds program toward complexity separations cannot be implemented in EF, or there are inherent obstacles to implementing the Cook-Reckhow program for EF.
引用
收藏
页码:1305 / 1324
页数:20
相关论文
共 47 条
[1]  
Aaronson S., 2003, Bulletin of the European Association for Theoretical Computer Science, P109
[2]   SIGMA-11-FORMULAE ON FINITE STRUCTURES [J].
AJTAI, M .
ANNALS OF PURE AND APPLIED LOGIC, 1983, 24 (01) :1-48
[3]   THE COMPLEXITY OF THE PIGEONHOLE PRINCIPLE [J].
AJTAI, M .
COMBINATORICA, 1994, 14 (04) :417-433
[4]   Pseudorandom generators in propositional proof complexity [J].
Alekhnovich, M ;
Ben-Sasson, E ;
Razborov, AA ;
Wigderson, A .
SIAM JOURNAL ON COMPUTING, 2004, 34 (01) :67-88
[5]   Power from random strings [J].
Allender, E ;
Buhrman, H ;
Koucky, M ;
Van Melkebeek, D ;
Ronneburger, D .
SIAM JOURNAL ON COMPUTING, 2006, 35 (06) :1467-1493
[6]  
Allender E., 2001, INT C FDN SOFTW TECH, P1
[7]  
[Anonymous], 1971, P 3 ANN ACM S THEOR
[8]  
[Anonymous], 1975, P 7 ANN ACM S THEOR, DOI DOI 10.1145/800116.8037567,8
[9]  
[Anonymous], 1986, The Eighteenth Annual ACM Symposium on Theory of Computing (STOC'86)
[10]  
[Anonymous], 1987, P 19 ANN ACM S THEOR