Analyzing Read-Once Cutting Plane Proofs in Horn Systems

In this paper, we investigate variants of cutting plane proof systems for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities \(\mathbf{A \cdot x \ge b}\) is called a Horn constraint system, if each entry in \(\mathbf{A}\) belongs to the set \(\{0,1,-1\}\) and furthermore there is at most one positive entry per row. Our focus is on deriving refutations, i.e., proofs of unsatisfiability of such programs in variants of the cutting plane proof system. Horn systems generalize Horn formulas, i.e., CNF formulas with at most one positive literal per clause. A Horn system which results from rewriting a Horn clausal formula is called a Horn clausal constraint system (HClCS). The cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of the addition rule (ADD) and the division rule (DIV). We show that the cutting plane calculus with the addition rule only (CP-ADD) does not require constraints of the form \(0 \le x_i \le 1\). We also investigate the existence of read-once refutations in Horn clausal constraint systems in the cutting plane proof system. We show that read-once refutations are incomplete. We show that the problem of finding a read-once refutation using only the ADD rule of an HCS is NP-hard even when the right-hand sides of the HCS belong to the set \(\{0,1\}\). Additionally, we show that the problem of finding a read-once refutation using only the ADD rule of an HClCS is NP-hard. We then show that these problems remain hard when we can use both the ADD and DIV rules. We then show that the problem of finding a shortest read-once refutation of an HCS whose right-hand sides belong to the set \(\{0,1\}\) is NPO BP-complete when the refutation can use only the ADD rule or the refutation can use both the ADD and DIV rules. Finally, we provide a parameterized exponential time algorithm for finding a read-once refutation of a system of Horn constraints using only the ADD rule.