تقرير
Towards P$\ne$NP from Extended Frege lower bounds
| العنوان: | Towards P$\ne$NP from Extended Frege lower bounds |
|---|---|
| المؤلفون: | Pich, Jan, Santhanam, Rahul |
| سنة النشر: | 2023 |
| المجموعة: | Mathematics |
| مصطلحات موضوعية: | Mathematics - Logic |
| الوصف: | We prove that if conditions I-II (below) hold and there is a sequence of Boolean functions $f_n$ hard to approximate by p-size circuits such that p-size circuit lower bounds for $f_n$ do not have p-size proofs in Extended Frege system EF, then $P\ne NP$. I. $S^1_2$ proves that a concrete function in ${\sf E}$ is hard to approximate by subexponential-size circuits. II. [Learning from $\neg\exists$ OWF.] $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits learning p-size circuits over the uniform distribution, with membership queries. Here, $S^1_2$ is Buss's theory of bounded arithmetic formalizing p-time reasoning. Further, we show that any of the following assumptions implies that $P\ne NP$, if EF is not p-bounded: 1. [Feasible anticheckers.] $S^1_2$ proves that a p-time function generates anticheckers for SAT. 2. [Witnessing $NP\not\subseteq P/poly$.] $S^1_2$ proves that a p-time function witnesses an error of each p-size circuit which fails to solve SAT. 3. [OWF from $NP\not\subseteq P/poly$ $\&$ hardness of ${\sf E}$.] Condition I holds and $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits computing SAT. The results generalize to stronger theories and proof systems. Comment: arXiv admin note: text overlap with arXiv:2111.10626 |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2312.08163 |
| رقم الأكسشن: | edsarx.2312.08163 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |