Unit Refutations in Horn Constraint Systems
摘要
This paper is concerned with algorithmic procedures for checking if a Horn Constraint System (HCS) has unit refutations of linear feasibility. A Horn constraint is a linear constraint of the form \(\mathbf{a\cdot x} \ge b\) , where each \(a_{i} \in \{0,1,-1\}\) and at most one of the \(a_{i}\) s is positive. Horn constraints generalize Horn clauses and find applications in a number of practical domains such as program verification and econometrics. Our main contribution is showing that the problem of checking if an infeasible HCS has a unit refutation is in P. To this end, we provide a certifying algorithm which runs in \(O(m\cdot n^{2} \cdot (m+n))\) time, where m and n are the number of constraints and number of variables in the input HCS respectively. Our algorithm is based on a combination of new and existing insights regarding Horn constraints.