Preprint:
Sam Buss, Albert Atserias and Moritz Müller
On the Consistency of Circuit Lower Bounds for
Non-Deterministic Time
In: Proc. 55th ACM Symposium on Theory of Computing (STOC), 2023, pp. 1257-1270.
Download full length preprint.
Download STOC proceedings version.
Associated talk slides: Bounded Arithmetic and a Consistency Result for EXP vs P/poly.
Abstract: We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory V02 is consistent with the conjecture that NEXP⊈P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. The same techniques establish the same results with NEXP replaced by the class of problems decidable in non-deterministic barely superpolynomial time such as NTIME(nO(log log log n)). Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.