Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities

Abstract. We continue a study initiated by Kraj´ıˇcek of a Resolutionlike proof system working with clauses of linear inequalities, R(CP). For all proof systems of this kind Kraj´ıˇcek proved in [1] an exponential lower bound of the form: exp(nΩ(1) ) MO(W log2 n) , where M is the maximal absolute value of coefficients in a given proof and W is the maximal clause width. In this paper we improve this lower bound. For tree-like R(CP)-like proof systems we remove a dependence on the maximal absolute value of coefficients M, hence, we give the answer to an open question from [2]. Proof follows from an upper bound on the real communication complexity of a polyhedra. Key words: propositional proof complexity, integer programming, cutting planes Many well known methods in an area of pseudo-boolean constraints optimization like a branch-and-bound [3] and Cutting Planes with the deduction rule [4] can be defined in terms of Resolution proof system that operates with clauses of linear i...

• Type: Conference
• Year: 2007
• Where: SAT
• Authors: Arist Kojevnikov
• Keywords: Lower Bounds, Maximal Absolute Value, Proof Systems, SAT 2007