Abstract
This paper is concerned with the design and analysis of a time-optimal and space-optimal, 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. 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 a refutation in the event that it is presented with infeasible instance. Our approach for the lattice point feasibility problem in UTVPI constraint systems is fundamentally different from existing approaches for this problem.
K. Subramani—This work was supported by the Air Force Research Laboratory under US Air Force contract FA8750-16-3-6003. The views expressed are those of the authors and do not reflect the official policy or position of the Department of Defense or the U.S. Government.
P. Wojciechowski—This research was supported in part by the National Science Foundation through Award CCF-1305054.
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 subscriptionsReferences
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Dantzig, G.B., Eaves, B.C.: Fourier-Motzkin elimination and its dual. J. Comb. Theory (A) 14, 288–297 (1973)
Fouilhe, A., Monniaux, D., Périn, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 345–365. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_19
Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471–479 (1995)
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, pp. 102–111 (1997)
Jaffar, J., Maher, M.J., Stuckey, P.J., Yap, R.H.C.: Beyond finite domains. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 86–94. Springer, Heidelberg (1994). doi:10.1007/3-540-58601-6_92
Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Gramlich, B. (ed.) FroCoS 2005. LNCS, vol. 3717, pp. 168–183. Springer, Heidelberg (2005). doi:10.1007/11559306_9
Miné, A.: The octagon abstract domain. Higher-Order Symb. Comput. 19(1), 31–100 (2006)
Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005). doi:10.1007/11513988_33
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2005. LNCS, vol. 3452, pp. 36–50. Springer, Heidelberg (2005). doi:10.1007/978-3-540-32275-7_3
Revesz, P.Z.: Tightened transitive closure of integer addition constraints. In: SARA (2009)
Sitzmann, I., Stuckey, P.J.: O-trees: a constraint-based index structure. In: Australasian Database Conference, pp. 127–134 (2000)
Schutt, A., Stuckey, P.J.: Incremental satisfiability and implication for UTVPI constraints. INFORMS J. Comput. 22(4), 514–527 (2010)
Subramani, K.: On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. Math. Log. Q. 50(3), 281–292 (2004)
Subramani, K., Wojciechowski, P.J.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166–208 (2017)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Subramani, K., Wojciechowski, P. (2017). Analyzing Lattice Point Feasibility in UTVPI Constraints. In: Beck, J. (eds) Principles and Practice of Constraint Programming. CP 2017. Lecture Notes in Computer Science(), vol 10416. Springer, Cham. https://doi.org/10.1007/978-3-319-66158-2_39
Download citation
DOI: https://doi.org/10.1007/978-3-319-66158-2_39
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66157-5
Online ISBN: 978-3-319-66158-2
eBook Packages: Computer ScienceComputer Science (R0)