Parameterized and Exact-Exponential Algorithms for the Read-Once Integer Refutation Problem in UTVPI Constraints

In this paper, we discuss parameterized and exact-exponential algorithms for the read-once integer refutability problem in Unit Two Variable Per Inequality (UTVPI) constraint systems. UTVPI constraint systems (UCSs) arise in a number of domains including operations research, program verification and abstract interpretation. The integer feasibility problem in UCSs is polynomial time solvable and there exist several algorithms for the same. This paper is concerned with refutations of integer feasibility in UCSs. Inasmuch as the integer feasibility problem is in P, there exist polynomial time algorithms to establish unrestricted refutations of integer feasibility. The focus of this paper is on a specific class of refutations called read-once refutations. Previous research has established that the problem of determining the existence of read-once refutations of integer feasibility in UCSs is NP-hard. This paper extends that research by examining the read-once refutability from the parameterized perspective. Using the number of refutation steps in the shortest read-once refutation, we establish fixed-parameter tractability. We also show that no polynomial size kernel exists for this problem. From the exact perspective, we design a non-trivial exponential algorithm.