Journal of Combinatorial Optimization

, Volume 35, Issue 2, pp 389–408 | Cite as

A certifying algorithm for lattice point feasibility in a system of UTVPI constraints

Article
  • 14 Downloads

Abstract

This paper is concerned with the design and analysis of a certifying algorithm for checking the lattice point feasibility of a class of constraints called unit two variable per inequality (UTVPI) constraints. A UTVPI constraint has at most two non-zero variables and the coefficients of the non-zero variables belong to the set \(\{+\,1,\ -\,1\}\). These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. As per the literature, the fastest known model generating algorithm for checking lattice point feasibility in UTVPI constraint systems runs in \(O(m \cdot n+n^{2} \cdot \log n)\) time and \(O(n^{2})\) space, where m represents the number of constraints and n represents the number of variables in the constraint system (Lahiri and Musuvathi, in: Proceedings of the 5th  international workshop on the frontiers of combining systems (FroCos), lecture notes in computer science, vol 3717, pp 168–183, 2005). In this paper, we design and analyze a new algorithm for checking the lattice point feasibility of UTVPI constraints. The presented algorithm runs in \(O(m \cdot n)\) time and \(O(m+n)\) space. Additionally it is certifying in that it produces a satisfying assignment in the event that it is presented with feasible instances and refutations in the event that it is presented with infeasible instances. The importance of providing certificates cannot be overemphasized, especially in mission-critical applications. Our approaches for the lattice point feasibility problem in UTVPI constraint systems is fundamentally different from existing approaches for this problem; indeed, it is based on new insights into combining well-known inference rules for these systems.

Keywords

UTVPI constraints Certificates Rounding scheme Difference constraints 

Notes

Acknowledgements

This research was conducted primarily in the School of Computer Science, Carnegie Mellon University, where the first author was an Invited Professor.

References

  1. Bagnara R, Hill P M, Zaffanella E (2008) An improved tight closure algorithm for integer octagonal constraints. In: VMCAI, pp 8–21Google Scholar
  2. Cherkassky BV, Goldberg AV, Radzik T (1996) Shortest paths algorithms: theory and experimental evaluation. Math Program 73:129–174MathSciNetMATHGoogle Scholar
  3. Cormen TH, Leiserson CE, Rivest RL, Stein C (2001) Introduction to algorithms. MIT Press, CambridgeMATHGoogle Scholar
  4. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM symposium on the principles of programming languages (POPL), ACM Press, pp 238–252Google Scholar
  5. Dantzig GB, Eaves BC (1973) Fourier–Motzkin elimination and its dual. J Comb Theory (A) 14:288–297Google Scholar
  6. Fouilhe A, Monniaux D, Périn M (2013). Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Static analysis: 20th international symposium, pp 345–365Google Scholar
  7. Gerber R, Pugh W, Saksena M (1995) Parametric dispatching of hard real-time tasks. IEEE Trans Comput 44(3):471–479CrossRefMATHGoogle Scholar
  8. Haken A (1985) The intractability of resolution. Theor Comput Sci 39(2–3):297–308MathSciNetCrossRefMATHGoogle Scholar
  9. Harvey W, Stuckey PJ (1997). A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proceedings of the 20th Australasian computer science conference, pp 102–111Google Scholar
  10. Hochbaum DS, Naor J (1994) Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J Comput 23(6):1179–1192MathSciNetCrossRefMATHGoogle Scholar
  11. Jaffar J, Maher MJ, Stuckey PJ, Yap HC (1994) Beyond finite domains. In: Proceedings of the second international workshop on principles and practice of constraint programming (PPCP), lecture notes in computer science, vol 874, pp 86–94Google Scholar
  12. Lahiri SK, Musuvathi M (2005) An Efficient decision procedure for UTVPI constraints. In: Proceedings of the \(5{\rm th}\) international workshop on the frontiers of combining systems (FroCos), lecture notes in computer science, vol 3717, pp 168–183Google Scholar
  13. Mehlhorn K, Näher S (1999) The LEDA platform of combinatorial and geometric computing. Cambridge University Press, CambridgeMATHGoogle Scholar
  14. Miné A (2006) The octagon abstract domain. High Order Symb Comput 19(1):31–100CrossRefMATHGoogle Scholar
  15. Nieuwenhuis R, Oliveras A (2005) DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Proceedings of the \(17{\rm th}\) international conference on computer aided verification (CAV), lecture notes in computer science, vol 3576, pp 321–334Google Scholar
  16. Nieuwenhuis R, Oliveras A, Tinelli C (2004) Abstract DPLL and abstract DPLL modulo theories. In: Proceedings of the  \(11{\rm th}\) international conference on logic for programming, artificial intelligence and reasoning (LPAR), lecture notes in computer science, vol 3452, pp 36–50Google Scholar
  17. Revesz PZ (2009) Tightened transitive closure of integer addition constraints. In: Proceedings of the \(8{\rm th}\) symposium on abstraction, reformulation and approximation (SARA), AAAIGoogle Scholar
  18. Schutt A, Stuckey PJ (2010) Incremental satisfiability and implication for UTVPI constraints. INFORMS J Comput 22(4):514–527MathSciNetCrossRefMATHGoogle Scholar
  19. Sitzmann I, Stuckey PJ (2000) O-trees: a constraint-based index structure. In: Australasian database conference, pp 127–134Google Scholar
  20. Subramani K (2004) On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. Math Logic Q 50(3):281–292MathSciNetCrossRefMATHGoogle Scholar
  21. Subramani K, Wojciechowski P (2016) A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica, First online: 28 April 2016Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2017

Authors and Affiliations

  1. 1.LDCSEEWest Virginia UniversityMorgantownUSA

Personalised recommendations