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• x + b•y ≤ c, where a,b ∈ {0,1,-1} and c ∈ 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(n~(1/2)• m•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.
展开▼
