On integer closure in a system of unit two variable per inequality constraints
- PDF / 459,240 Bytes
- 18 Pages / 439.642 x 666.49 pts Page_size
- 102 Downloads / 128 Views
On integer closure in a system of unit two variable per inequality constraints K. Subramani1
· P. Wojciechowski1
© Springer Nature Switzerland AG 2020
Abstract In this paper, we study the problem of computing the lattice point closure of a conjunction of Unit Two Variable Per Inequality (UTVPI) constraints. We accomplish this by adapting Johnson’s all pairs shortest path algorithm to UTVPI constraint systems (UCSs). Thus, we obtain a closure algorithm that is efficient for sparse constraint systems. This problem has been extremely well-studied in the literature, since it arises in a number of applications, including but not limited to, program verification and operations research. In UTVPI constraints, linear feasibility does not always imply integer feasibility. Thus, there is a difference between the linear closure of a UCS and the integer closure of that same system. Finding the linear closure requires only a single inference rule called the transitive inference rule. This inference rule corresponds to the addition of constraints and preserves both linear and integer solutions. The problem of finding the integer closure requires the use of the tightening inference rule. Unlike the transitive inference rule, the tightening inference rule does not preserve linear solutions. However, it does preserve integer solutions. The complexity of solving the integer closure problem has steadily improved over the past several decades with the fastest algorithm for this problem running in time O(n3 ) on a UCS with n variables and m constraints. For the same input parameters, we detail an algorithm that runs in time O(m · n + n2 · log n). It is clear that our algorithm is superior to the state of the art when the UCS is sparse (m ∈ o(n2 )), and no worse than the state of the art when the UCS is dense (m ∈ (n2 )). The best known running time for computing the closure of a conjunction of difference constraints (m constraints, n variables) is O(m · n + n2 · log n), and UTVPI constraints subsume difference constraints. Keywords UTVPI constraints · Relaxation · Integer closure · Dijkstra’s algorithm · Shortest paths Mathematics Subject Classification (2010) 90C10 · 90B10 This research was supported in part by the Air-Force Office of Scientific Research through Grant FA9550-19-1-017 and in part by the Air-Force Research Laboratory, Rome through Contract FA8750-17-S-7007. K. Subramani
[email protected]
Extended author information available on the last page of the article.
K. Subramani, P. Wojciechowski
1 Introduction This paper is concerned with the design of a new algorithm for computing the integer closure of a unit two variable per inequality (UTVPI) constraint system (UCS). This is accomplished by adapting Johnson’s all pairs shortest path algorithm to UCSs. UCSs occur in a number of application domains, including but not limited to, constraint solving [10], abstract interpretation [11], spatial databases, and theorem proving. There are two principal problems associated with UCSs i.e., the integer feasibility problem and
Data Loading...
