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

2020/03/20 by Garlík, Michal · 1 citation
#03F20 #Computational Complexity (cs.CC) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2003.10230

Abstract

We show that for every integer k ≥ 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 ≥ 1, Res(k) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.

Cited by

• The Proof Analysis Problem

Related

• Automating Resolution is NP-Hard
• Resolution and the binary encoding of combinatorial principles
• The Proof Analysis Problem
• Cut-free LK quasi-polynomially simulates resolution
• Resolution Lower Bounds for Refutation Statements