Why are proof complexity lower bounds hard?

0523286 - MÚ 2020 RIV US eng C - Conference Paper (international conference)
Pich, Ján - Santhanamz, R.
Why are proof complexity lower bounds hard?
2019 IEEE 60th Annual Symposium on Foundations of Computer Science (FOCS 2019). Los Alamitos: IEEE, 2019, s. 1305-1324. Annual IEEE Symposium on Foundations of Computer Science. ISBN 978-1-7281-4952-3. ISSN 0272-5428.
[60th IEEE Annual Symposium on Foundations of Computer Science (FOCS). Baltimore (US), 09.11.2019-12.11.2019]
R&D Projects: GA ČR(CZ) GA19-05497S
Institutional support: RVO:67985840
Keywords : computational complexity * proof complexity * circuit lower bounds
OECD category: Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
https://ieeexplore.ieee.org/document/8948624

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.
Permanent Link: http://hdl.handle.net/11104/0307653