Input Proofs and Rank One Cutting Planes

Abstract

Input resolution and “unit support” resolution (a generalization of unit resolution) are complete inference methods for Horn clauses in propositional logic. We show that they have a close analog in cutting plane theory. Namely, a logical clause can be deduced using input or unit support resolution if and only if it belongs to the elementary closure of the premises and is therefore a rank one cut in Chvátal's sense. This connection leads to a cutting plane algorithm for solving non-Horn inference problems. INFORMS Journal on Computing, ISSN 1091-9856, was published as ORSA Journal on Computing from 1989 to 1995 under ISSN 0899-1499.