Exact and Parameterized Algorithms for Read-Once Refutations in Horn Constraint Systems.

In this paper, we discuss exact and parameterized algorithms for the problem of finding a read-once refutation in an unsatisfiable Horn Constraint System (HCS). Recall that a linear constraint system A · x ≥ b is said to be a Horn constraint system, if each entry in A belongs to the set { 0 , 1 , - 1 } and at most one entry in each row of A is positive. In this paper, we examine the importance of constraints in which more variables have negative coefficients than have positive coefficients. There exist several algorithms for checking whether a Horn constraint system is feasible. To the best of our knowledge, these algorithms are not certifying, i.e., they do not provide a certificate of infeasibility. Our work is concerned with providing a specialized class of certificates called “read-once refutations”. In a read-once refutation, each constraint defining the HCS may be used at most once in the derivation of a refutation. The problem of checking if an HCS has a read-once refutation ( HCS ROR ) has been shown to be NP-hard . We analyze the HCS ROR problem from two different algorithmic perspectives, viz., parameterized algorithms and exact exponential algorithms.