从扩展弗雷格下界出发探索P≠NP问题

《Journal of the ACM》：Towards P≠NP from Extended Frege lower bounds

证明复杂度下界与布尔电路下界的关联性研究，发现通过见证公式w_n^k(f)可建立NEXP与布尔电路多项式大小的无条件等价性。研究涉及离散对数问题的电路复杂度与证明复杂度的双向联系，以及自证明上界在复杂度理论中的应用。

　　

摘要AI 摘要

要查看此由 AI 生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

我们提出了一种新的方法来解决一个基本问题：即具体的命题证明系统的证明复杂性下界是否意味着超多项式布尔电路的下界。我们观察到，从命题证明系统的证明复杂性下界到超多项式布尔电路下界的任何一般性推论都无条件地表明\({\sf NEXP}\)不存在多项式大小的布尔电路。我们探索了在不解决这个长期存在且极其困难的开问题情况下可能建立的联系。

对于任何多项式时间可计算的函数 f，我们定义了见证公式 \(w_n^k(f)\)，这些公式表明：对于任何在 n 个变量上的大小为 n^k 的电路 C，以及任何大小为 n 的公式 ?，要么 C 能计算出满足 ? 的赋值，要么 f 能验证地反驳 C 在长度为 n 的实例上计算出 \({\sf SAT}\)。我们证明了，如果见证公式是重言式，那么任何加上 \(w_n^k(f)\) 公理的扩展弗雷格（Extended Frege）系统的超多项式下界都意味着 \({\sf SAT}\) 需要超多项式大小的布尔电路。我们还给出了离散对数问题的电路下界与证明复杂性下界（用于高效编码离散对数问题可由小型电路计算这一陈述的命题公式）之间的无条件等价关系，这些证明复杂性下界是针对一个具体定义的强（非均匀）命题证明系统而言的。

我们的发现对计算复杂性领域中的几个重要问题的元数学有重要影响，包括：单向函数是否可以基于 NP 类问题的最坏情况难度；单向函数与在均匀分布上使用成员查询的最坏情况学习之间是否存在二分法；以及是否可以构造出可行的可满足性验证器。我们表明，对于这些问题中的每一个，如果在几乎任何标准数学理论中都能证明出肯定的答案，那么这都将意味着命题证明复杂性和电路复杂性之间的新联系。

我们的结果依赖于一种新的“自证明”上界概念，这一概念本身也可能具有独立的研究价值，并且涉及将随机自归约（random self-reducibility）应用于证明复杂性的新颖方法。

AI 摘要

AI 生成的摘要（实验性）

此摘要是使用自动化工具生成的，并非由文章作者编写或审核。它旨在帮助发现新信息、帮助读者评估内容的相关性，并协助来自相关研究领域的读者理解该工作。它旨在补充作者提供的摘要，后者仍然是论文的主要总结。完整文章才是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的摘要版本。

要查看此由 AI 生成的通俗语言摘要，您必须具有高级访问权限。