Abstract
A unit two variable per inequality (UTVPI) constraint is of the form a.x+b.y ≤ d where x and y are integer variables, the coefficients a,b ∈ {–1,0,1} and the bound d is an integer constant. This paper presents an efficient decision procedure for UTVPI constraints. Given m such constraints over n variables, the procedure checks the satisfiability of the constraints in O(n.m) time and O(n+m) space. This improves upon the previously known O(n 2.m) time and O(n 2) space algorithm based on transitive closure. Our decision procedure is also equality generating, proof generating, and model generating.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Software Predicate Abstraction Refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 457–461. Springer, Heidelberg (2004)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI 2001), Snowbird, Utah (June 2001); SIGPLAN Notices, 36(5) (May 2001)
Bellman, R.: On a routing problem. Quarterly of Applied Mathematics 16(1), 87–90 (1958)
Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. In: European Symposium on Algorithms, pp. 349–363 (1996)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.: Theorem Proving usign Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2002), pp. 234–245 (2002)
Ford Jr., L.R., Fulkerson, D.R.: Flows in Networks. Princeton University Press, Princeton (1962)
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 1997), pp. 102–111 (1997)
Hennessy, J.L., Gross, T.R.: Postpass code optimization of pipeline constraints. ACM Trans. Program. Lang. Syst. 5(3), 422–448 (1983)
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 (1994)
Lagarias, J.C.: The computational complexity of simultaneous diophantine approximation problems. SIAM Journal of Computing 14(1), 196–209 (1985)
Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-of-order microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341–354. Springer, Heidelberg (2003)
Lahiri, S.K., Musuvathi, M.: An efficient nelson-oppen decision procedure for difference constraints over rationals. Technical Report MSR-TR-2005-61, Microsoft Research (2005)
Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, October 2001, pp. 310–319. IEEE CS Press, IEEE (2001)
Necula, G.C., Lee, P.: Proof generation in the touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 25–44. Springer, Heidelberg (2000)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS) 2(1), 245–257 (1979)
Pratt, V.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology, Cambridge, Mass. (September 1977)
Seshia, S.A., Bryant, R.E.: Deciding quantifier-free presburger formulas using parameterized solution bounds. In: 19th IEEE Symposium of Logic in Computer Science (LICS 2004), July 2004. IEEE Computer Society, Los Alamitos (2004)
Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM Journal of Computing 1(2), 146–160 (1972)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lahiri, S.K., Musuvathi, M. (2005). An Efficient Decision Procedure for UTVPI Constraints. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_9
Download citation
DOI: https://doi.org/10.1007/11559306_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)