arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2102.06673cs.CCcs.LOmath.LO
收藏

正分支程序的证明复杂性

Proof complexity of positive branching programs

Anupam Das, Avgerinos Delkos

AI总结:

本文研究正分支程序系统的证明复杂性,提出系统eLNDT+,证明其可在正矢列上多项式模拟eLNDT,并形式化计数函数性质及给出鸽巢原理的多项式大小证明。

摘要:

我们研究基于正分支程序的系统的证明复杂性,即非确定性分支程序(NBPs),其中对于任意两个节点之间的0-转移,也存在一个1-转移。正NBPs计算单调布尔函数,就像无否定电路或公式一样,但构成的是(非均匀)NL的正版本,而不是分别为P或NC1的正版本。NBPs的证明复杂性在Buss、Das和Knop的先前工作中已被研究,他们使用扩展变量来表示有向无环图结构,在(非确定性)决策树语言上得到了系统eLNDT。我们的系统eLNDT+是通过将他们的系统限制为正语法而得到的,类似于“单调矢列演算”MLK是通过将通常的矢列演算LK限制为无否定公式而得到的。我们的主要结果是eLNDT+在正矢列上多项式模拟eLNDT。我们的证明方法受到Atserias、Galesi和Pudlák关于MLK的类似结果的启发,该结果最近通过Jeřábek以及Buss、Kabanets、Kolokolova和Koucký的工作被改进为真正的多项式模拟。在此过程中,我们在eLNDT+内通过多项式大小证明形式化了计数函数的若干性质,并作为案例研究,给出了命题鸽巢原理的显式多项式大小证明。

英文摘要:

We investigate the proof complexity of systems based on positive branching programs, i.e. non-deterministic branching programs (NBPs) where, for any 0-transition between two nodes, there is also a 1-transition. Positive NBPs compute monotone Boolean functions, just like negation-free circuits or formulas, but constitute a positive version of (non-uniform) NL, rather than P or NC1, respectively. The proof complexity of NBPs was investigated in previous work by Buss, Das and Knop, using extension variables to represent the dag-structure, over a language of (non-deterministic) decision trees, yielding the system eLNDT. Our system eLNDT+ is obtained by restricting their systems to a positive syntax, similarly to how the 'monotone sequent calculus' MLK is obtained from the usual sequent calculus LK by restricting to negation-free formulas. Our main result is that eLNDT+ polynomially simulates eLNDT over positive sequents. Our proof method is inspired by a similar result for MLK by Atserias, Galesi and Pudlák, that was recently improved to a bona fide polynomial simulation via works of Jeřábek and Buss, Kabanets, Kolokolova and Koucký. Along the way we formalise several properties of counting functions within eLNDT+ by polynomial-size proofs and, as a case study, give explicit polynomial-size poofs of the propositional pigeonhole principle.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑