zbMATH — the first resource for mathematics

A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. (English) Zbl 1360.68889
Summary: In this paper, we discuss a new combinatorial certifying algorithm for the problem of checking linear feasibility in 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. The proposed algorithm runs in \(O(m\cdot n)\) time and \(O(m+n)\) space on a UTVPI system with \(n\) variables and \(m\) constraints. Observe that these resource bounds match the bounds of the fastest strongly polynomial algorithm for difference constraints. Inasmuch as UTVPI constraints subsume difference constraints, it is clear that the resource requirements of our algorithm are optimal. Additionally, our algorithm is certifying, in that it produces a satisfying assignment when presented with a feasible instance, and a refutation, otherwise. At the heart of our algorithm is a new constraint network representation for UTVPI constraints.

68W05 Nonnumerical algorithms
68W40 Analysis of algorithms
Full Text: DOI
[1] Bagnara, R., Hill, P.M., Zaffanella, E.: An improved tight closure algorithm for integer octagonal constraints. In: 9th International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 8-21 (2008) · Zbl 1138.68474
[2] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238-252 (1977) · Zbl 1298.68289
[3] Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001) · Zbl 1047.68161
[4] Chandrasekaran, R; Subramani, K, A combinatorial algorithm for Horn programs, Discret. Optim., 10, 85-101, (2013) · Zbl 1284.90038
[5] Gerber, R; Pugh, W; Saksena, M, Parametric dispatching of hard real-time tasks, IEEE Trans. Comput., 44, 471-479, (1995) · Zbl 1062.68543
[6] Karmarkar, N.K.: A new polynomial-time algorithm for linear programming. In: Proceedings of the 16th Annual ACM Symposium on Theory of Computing, pp. 302-311 (1984) · Zbl 0557.90065
[7] Khachiyan, L.G.: A polynomial algorithm in linear programming. Doklady Akademiia Nauk SSSR 224, 1093-1096 (1979). English Translation: Soviet Mathematics Doklady 20, 1093-1096 · Zbl 0414.90086
[8] 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, September 19-21, Vienna, Austria, pp. 168-183. Springer, New York (2005) · Zbl 1171.68715
[9] McConnell, RM; Mehlhorn, K; Näher, S; Schweitzer, P, Certifying algorithms, Comput. Sci. Rev., 5, 119-161, (2011) · Zbl 1298.68289
[10] Miné, A, The octagon abstract domain, Higher-Order Symb. Comput., 19, 31-100, (2006) · Zbl 1105.68069
[11] Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: 17th International Conference on Computer Aided Verification, pp. 321-334 (2005) · Zbl 1081.68629
[12] Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994) · Zbl 0833.68049
[13] Revesz, P.Z: Tightened transitive closure of integer addition constraints. In: The Eighth Symposium on Abstraction, Reformulation and Approximation (2009)
[14] Rubinfield, R.: A Mathematical Theory of Self-Checking, Self-Testing and Self-Correcting Programs. PhD thesis, Computer Science Division, University of California, Berkeley (1990) · Zbl 1284.90038
[15] Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987) · Zbl 0665.90063
[16] Schutt, A; Stuckey, PJ, Incremental satisfiability and implication for UTVPI constraints, INFORMS J. Comput., 22, 514-527, (2010) · Zbl 1243.90141
[17] Tardos, E, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res., 34, 250-256, (1986) · Zbl 0626.90053
[18] Vaidya, P.M.: An algorithm for linear programming which requires \({O}(((m+n)n^2+(m+n)^{1.5}n){L})\) arithmetic operations. In: Aho, A. (ed.) Proceedings of the 19th Annual ACM Symposium on Theory of Computing, pp. 29-38. ACM Press, New York City (1987) · Zbl 1243.90141
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.