$k$ - DNF归结的可行析取性质的失效及其自动化的NP困难性
Failure of Feasible Disjunction Property for $k$-DNF Resolution and NP-hardness of Automating It
摘要：
我们证明了对于任意整数$k \geq 2$，Res（$k$）命题证明系统不具有弱可行析取性质.接下来，我们将Atserias和Müller [FOCS，2019]的最近结果推广到Res（$k$）。我们证明，如果NP不包括在P（resp. QP，SUBEXP），则对于每个整数$k \geq 1$，Res（$k$）在多项式中不是可自动化的（分别为准多项式、次指数）时间。
英文摘要：
We show that for every integer $k \geq 2$, the Res($k$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and Müller [FOCS, 2019] to Res($k$). We show that if NP is not included in P (resp. QP, SUBEXP) then for every integer $k \geq 1$, Res($k$) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
