We study the relationship between the existence of optimal proof systems and recursive jump operators, two central open problems in proof complexity. For a set L, an optimal proof system is a strongest proof system in terms of proof length, whereas a recursive jump operator uniformly transforms any proof system for L into a stronger one with respect to proof length, thereby witnessing non-optimality. It is clear that the existence of a recursive jump operator for L rules out optimal proof systems for L. Khaniki (FOCS 2024) is interested in the converse of this implication and explicitly poses the following question, where TAUT denotes the set of propositional tautologies. Q: Does the non-existence of optimal proof systems for TAUT imply the existence of recursive jump operators for TAUT? We generalize and address this question from both a relativized and an unrelativized perspective. We show that proving a positive answer for Q is provably hard by constructing the following oracle. O: The polynomial-time hierarchy is infinite, TAUT has no optimal proof systems, and TAUT has no recursive jump operators. This shows that Khaniki's question can not be answered in the positive by relativizable means, even under the standard complexity-theoretic assumption that the polynomial-time hierarchy is infinite. In contrast, we obtain positive results when the question Q is posed for sets different from TAUT. We prove that the existence of recursive jump operators is upward closed under $\leq_{\text{m}}^{\text{p}}$-reducibility, a result that so far was only known for the non-existence of optimal proof systems. Furthermore, we show that the sets known to have no optimal proof systems by Messner (STACS 1999) in fact admit recursive jump operators. Thus, essentially all sets currently known to have no optimal proof systems have recursive jump operators.


翻译:我们研究了最优证明系统的存在性与递归跳跃算子之间的关系,这是证明复杂性中两个核心未解问题。对于集合L,最优证明系统是指在证明长度方面最强的证明系统,而递归跳跃算子则能将L的任何证明系统一致地转化为一个在证明长度上更强的系统,从而表明其非最优性。显然,L上递归跳跃算子的存在排除了L的最优证明系统。Khaniki(FOCS 2024)对该蕴涵的逆命题感兴趣,并明确提出了以下问题,其中TAUT表示命题重言式集合。问:TAUT不存在最优证明系统是否蕴涵TAUT存在递归跳跃算子?我们从相对化和非相对化两个角度对该问题进行了推广和研究。我们通过构造以下谕示证明了Q的肯定回答是难以证明的。O:多项式层次是无穷的,TAUT没有最优证明系统,且TAUT没有递归跳跃算子。这表明,即使在标准复杂性理论假设(多项式层次无穷)下,Khaniki的问题也无法通过相对化方法得到肯定回答。相比之下,当问题Q针对不同于TAUT的集合提出时,我们得到了肯定结果。我们证明了递归跳跃算子的存在性在$\leq_{\text{m}}^{\text{p}}$-可归约性下向上封闭,这一结果此前仅对最优证明系统的不存在性成立。此外,我们证明了Messner(STACS 1999)已知没有最优证明系统的集合实际上承认递归跳跃算子。因此,当前已知没有最优证明系统的所有集合本质上都具有递归跳跃算子。

0
下载
关闭预览

相关内容

【剑桥大学-算法手册】Advanced Algorithms, Artificial Intelligence
专知会员服务
37+阅读 · 2024年11月11日
南大《优化方法 (Optimization Methods》课程,推荐!
专知会员服务
80+阅读 · 2022年4月3日
专知会员服务
37+阅读 · 2021年9月12日
机器学习中的最优化算法总结
人工智能前沿讲习班
22+阅读 · 2019年3月22日
推荐系统算法合集,满满都是干货(建议收藏)
七月在线实验室
17+阅读 · 2018年7月23日
干货|掌握机器学习数学基础之优化[1](重点知识)
机器学习研究会
10+阅读 · 2017年11月19日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Arxiv
0+阅读 · 5月31日
VIP会员
最新内容
《边缘计算关键技术分析及美军作战实践应用》
专知会员服务
0+阅读 · 今天14:08
边缘计算的军事应用
专知会员服务
1+阅读 · 今天13:50
一种考虑资源机动性的武器目标分配混合算法
专知会员服务
4+阅读 · 8月8日
《多域冲突比较支持模型》60页
专知会员服务
10+阅读 · 8月7日
相关资讯
机器学习中的最优化算法总结
人工智能前沿讲习班
22+阅读 · 2019年3月22日
推荐系统算法合集,满满都是干货(建议收藏)
七月在线实验室
17+阅读 · 2018年7月23日
干货|掌握机器学习数学基础之优化[1](重点知识)
机器学习研究会
10+阅读 · 2017年11月19日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员