On the computational complexity of finding hard tautologies

TL;DR

This paper investigates the computational difficulty of identifying hard tautologies and related formulas, connecting proof complexity, cryptographic assumptions, and the limitations of certain algorithms under strong hypotheses.

Contribution

It introduces new search problems related to hard tautologies and proves their computational hardness assuming cryptographic and proof complexity hypotheses.

Findings

Cert cannot be solved in exponential time under certain cryptographic assumptions

Both Cert and Find are only partially defined for infinitely many input sizes

Results link proof complexity with cryptographic hardness assumptions

Abstract

It is well-known (cf. K.-Pudl\'ak 1989) that a polynomial time algorithm finding tautologies hard for a propositional proof system $P$ exists iff $P$ is not optimal. Such an algorithm takes $1^{(k)}$ and outputs a tautology $\tau_k$ of size at least $k$ such that $P$ is not p-bounded on the set of all $\tau_k$'s. We consider two more general search problems involving finding a hard formula, {\bf Cert} and {\bf Find}, motivated by two hypothetical situations: that one can prove that $\np \neq co\np$ and that no optimal proof system exists. In {\bf Cert} one is asked to find a witness that a given non-deterministic circuit with $k$ inputs does not define $TAUT \cap \kk$. In {\bf Find}, given $1^{(k)}$ and a tautology $\alpha$ of size at most $k^{c_0}$, one should output a size $k$ tautology $\beta$ that has no size $k^{c_1}$ $P$-proof from substitution instances of $\alpha$. We shall prove, assuming the existence of an exponentially hard one-way permutation, that {\bf Cert} cannot be solved by a time $2^{O(k)}$ algorithm. Using a stronger hypothesis about the proof complexity of Nisan-Wigderson generator we show that both problems {\bf Cert} and {\bf Find} are actually only partially defined for infinitely many $k$ (i.e. there are inputs corresponding to $k$ for which the problem has no solution). The results are based on interpreting the Nisan-Wigderson generator as a proof system.