A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints

Abstract

In this paper, we discuss a new model-generating algorithm for integer feasibility in a system of Unit Two Variable Per Inequality (UTVPI) constraints (IF). Recall that a UTVPI constraint is a linear constraint of the form: $a\cdot x+b \cdot y \le c$, where $a, b \in \{0,1,-1\}$ and $c \in \mathbb {Z}$. These constraints arise in a number of application domains including but not limited to program verification (array bounds checking and abstract interpretation), operations research (packing and covering) and logic programming. Over the years, several algorithms have been proposed for the IF problem. Most of these algorithms are based on two inference rules, viz. the transitive rule and the tightening rule. None of these algorithms are bit-scaling, i.e., the running times of these algorithms are parameterized only by the number of variables and the number of constraints in the UTVPI system. We introduce a novel algorithm for the IF problem, which is based on a collection of new insights. These insights areused to design a new bit-scaling algorithm for IF that runs in $O(\sqrt{n}\cdot m \cdot \log C)$ time, where n denotes the number of variables, m denotes the number of constraints and C denotes the largest absolute values of all the constants defining the system.

K. Subramani—This work was supported by the Air Force Research Laboratory under US Air Force contract FA8750-16-3-6003. The views expressed are those of the authors and do not reflect the official policy or position of the Department of Defense or the U.S. Government.

P. Wojciechowski—This research was supported in part by the National Science Foundation through Award CCF-1305054.