Failure of Feasible Disjunction Property for k-DNF Resolution and NP-hardness of Automating It

arXiv2003.10230MaRDI QIDQ6337237FDOQ6337237

Authors: Michal Garlík 

Publication date: 19 March 2020

Abstract: We show that for every integer $kgeq2$, the Res($k$) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a recent result of Atserias and M"uller [FOCS, 2019] to Res($k$). We show that if NP is not included in P (resp. QP, SUBEXP) then for every integer $kgeq1$, Res($k$) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.

Mathematics Subject Classification ID

Complexity of proofs (03F20)

This page was built for publication: Failure of Feasible Disjunction Property for $k$-DNF Resolution and NP-hardness of Automating It

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6337237)