On the parametrized complexity of read-once refutations in UTVPI+ constraint systems.

In this paper, we study the problem of finding read-once refutations (ROR) of linear feasibility in a specialized class of constraint systems called UTVPI+ constraint systems (UCS +). The refutations in this paper are analyzed using the ADD inference rule. Recall that a Unit Two Variable Per Inequality (UTVPI) constraint is a constraint of the form a i ⋅ x i + a j ⋅ x j ≤ b , where b ∈ Z , and a i , a j ∈ { 0 , 1 , − 1 }. A conjunction of such constraints is called a UTVPI constraint system (UCS). UCSs find applications in a number of domains such as abstract interpretation and scheduling. We examine a more general form of UCSs that allows for a limited number of non-UTVPI constraints to be added to a UCS. We refer to these more general UCSs as UTVPI+ constraint systems or UCS + s. If a UCS + has only k non-UTVPI constraints, then we refer to it as a UCS k +. Our focus in this paper is on refutations, i.e., proofs of infeasibility in UCS + s. In particular, we study read-once refutations of linear feasibility in UCS + s. Although the problem of finding read-once refutations of UCSs is polynomial time solvable, the presence of non-UTVPI constraints makes the problem NP-hard. However, if the number of non-UTVPI constraints is fixed, then read-once refutations can be found in polynomial time. In fact, in this paper, we show that the ROR problem is fixed-parameter tractable (FPT) for UCS k + s , with respect to k , the number of non-UTVPI constraints in the system. We also provide a lower bound on the efficiency of a class of parameterized algorithms for this problem, based on the Strong Exponential Time Hypothesis. [ABSTRACT FROM AUTHOR]