Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On integer closure in a system of unit two variable per inequality constraints

  • Published:
Annals of Mathematics and Artificial Intelligence Aims and scope Submit manuscript

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\cdot n +n^{2} \cdot \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\cdot n +n^{2} \cdot \log n)\), and UTVPI constraints subsume difference constraints.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness. Formal Methods in System Design (FMSD) 35(3), 279–323 (2009)

    Article  MATH  Google Scholar 

  2. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)

    MATH  Google Scholar 

  3. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Symposium on Principles of Programming Languages (POPL), pp. 238–252 (1977)

  4. Dantzig, G.B., Eaves, B.C.: Fourier-motzkin Elimination and its Dual. Journal of Combinatorial Theory (A) 14, 288–297 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dechter, R.: Constraint Processing. Morgan Kaufmann Publishers Inc., San Francisco (2003)

    MATH  Google Scholar 

  6. Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471–479 (1995)

    Article  MATH  Google Scholar 

  7. Harvey, W., Stuckey, P. J.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proceedings of the 20th Australasian Computer Science Conference (ACSC), pp. 102–111 (1997)

  8. Hochbaum, DS, Naor, JS: Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J. Comput. 23(6), 1179–1192 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  9. Jaffar, J., Maher, M.J., Stuckey, P.J., Yap, H.C.: Beyond finite domains. In: Proceedings of the Second International Workshop on Principles and Practice of Constraint Programming (PPCP) (1994)

  10. Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Proceedings of the 5th International Workshop on the Frontiers of Combining Systems (FroCos) (2005)

  11. Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)

    Article  MATH  Google Scholar 

  12. Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Proceedings of the 11th International Conference on Logic for Programming (LPAR), pp. 36–50 (2004)

  13. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987)

    MATH  Google Scholar 

  14. Schutt, A., Stuckey, PJ.: Incremental satisfiability and implication for utvpi constraints. Informs J. Comput. 22(4), 514–527 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  15. Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Proceedings of the 12th International Workshop on Logic Based Program Synthesis and Tranformation (LOPSTR), pp. 71–89 (2002)

  16. Sitzmann, I., Stuckey, P.J.: O-trees: a constraint-based index structure. In: Proceedings of the 11th Australasian Database Conference (ADC), pp. 127–134 (2000)

  17. Subramani, K.: On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. Math. Log. Q. 50(3), 281–292 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  18. Subramani, K., Wojciechowski, P.J.: A bit-scaling algorithm for integer feasibility in UTVPI constraints. In: Proceedings of the 27th International Workshop on Combinatorial Algorithms (IWOCA), vol. 9843, pp. 321–333 (2016)

  19. Subramani, K., Wojciechowski, P.J.: An optimal algorithm for computing the integer closure of UTVPI constraints. In: Proceedings of the 10th International Workshop on Algorithms and Computation (WALCOM), vol. 9627 of Lecture Notes in Computer Science, pp 154–165. Springer, berlin (2016)

  20. Subramani, K., Wojciechowski, P.J.: Analyzing lattice point feasibility in UTVPI constraints. In: Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP), pp. 615–629 (2017)

  21. Subramani, K., Wojciechowski, P.J.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166–208 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  22. Subramani, K., Wojciechowski, P.J.: A certifying algorithm for lattice point feasibility in a system of UTVPI constraints. J. Comb. Optim. 35(2), 389–408 (2018)

    Article  MathSciNet  MATH  Google Scholar 

  23. Wojciechowski, P.J., Subramani, K., Williamson, M.D.: Optimal length tree-like refutations of linear feasibility in UTVPI constraints. In: Proceedings of the 12th International Workshop on Frontiers in Algorithmics(FAW), vol. 10923, pp. 300–314 (2018)

  24. Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81 (7), 2765–2794 (2019)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LCSEE, West Virginia University, Morgantown, WV, USA

    K. Subramani & P. Wojciechowski

Authors
  1. K. Subramani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. Wojciechowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to K. Subramani.

Additional information

Publisher’s note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

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.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Subramani, K., Wojciechowski, P. On integer closure in a system of unit two variable per inequality constraints. Ann Math Artif Intell 88, 1101–1118 (2020). https://doi.org/10.1007/s10472-020-09703-5

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10472-020-09703-5

Keywords

Mathematics Subject Classification (2010)

Search

Navigation