Abstract
In this paper, we detail a new algorithm for the problem of checking linear and integer feasibility of a system of Horn constraints. For certain special cases, the new algorithm is faster than the “Lifting Algorithm” described in [1]. Moreover, the new approach is based on different ideas and in fact exploits several properties of Horn constraint systems (HCS) which are not known to be part of the literature. In the case of constraints of bounded width (corresponding to “loosely coupled” systems), our algorithm can be modified to run in \(O(n^3 + m \cdot n + \frac{m\cdot n^2}{\log (\max (m,n))})\) time. Our main result establishes that checking the feasibility of an HCS can be reduced to three subproblems: negative-cost cycle detection in networks (NCCD), matrix-vector multiplication (MV), and the conversion of an HCS to a non-redundant set of difference constraints (H2D). The MV and NCCD problems have been extremely well-studied, and specialized, fast algorithms exist for relevant special cases. We have identified a new problem, H2D, which warrants future research, since improved algorithms for H2D could be implemented in our algorithm to decrease the running time.
This research was supported in part by the National Science Foundation through Award CCF-0827397.
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
Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for horn programs. In: Dong, Y., Du, D.-Z., Ibarra, O. (eds.) ISAAC 2009. LNCS, vol. 5878, pp. 1114–1123. Springer, Heidelberg (2009)
Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. John Wiley & Sons, New York (1999)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)
Lever, J., Wallace, M., Richards, B.: Constraint logic programming for scheduling and planning. British Telecom Technology Journal 13, 73–80 (1995)
Truemper, K.: Personal communication (2003)
Miné, A.: The Octagon Abstract Domain. Higher-Order and Symbolic Computation 19, 31–100 (2006)
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)
Homer, S., Selman, A.L.: Computability and Complexity Theory. Springer, Heidelberg (2001)
de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N.: The ICS decision procedures for embedded deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 218–222. Springer, Heidelberg (2004)
Ford, J., Shankar, N.: Formal verification of a combination decision procedure. In: CADE, pp. 347–362 (2002)
Duterre, B., de Moura, L.: The yices smt solver. Technical report, SRI International (2006)
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)
Lewis, H.R., Papadimitriou, C.H.: Symmetric space-bounded computation. Theor. Comput. Sci. 19, 161–187 (1982)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 84–96. ACM, New York (1978)
Jeavons, P.G., Cooper, M.C.: Tractable constraints on ordered domains. Artif. Intell. 79, 327–339 (1995)
van Maaren, H., Dang, C.: Simplicial pivoting algorithms for a tractable class of integer programs. J. Comb. Optim. 6, 133–142 (2002)
Tardos, E.: A strongly polynomial algorithm to solve combinatorial linear programs. Oper. Res. 34, 250–256 (1986)
Goldberg, A.V.: Scaling algorithms for the shortest paths problem. SIAM Journal on Computing 24, 494–504 (1995)
Liberty, E., Zucker, S.W.: The mailman algorithm: A note on matrix–vector multiplication. Inf. Process. Lett. 109, 179–182 (2009)
Seshia, S.A., Subramani, K., Bryant, R.E.: On solving boolean combinations of UTVPI constraints. Journal on Satisfiability, Boolean Modeling and Computation 3, 67–90 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Subramani, K., Worthington, J. (2011). A New Algorithm for Linear and Integer Feasibility in Horn Constraints. In: Achterberg, T., Beck, J.C. (eds) Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. CPAIOR 2011. Lecture Notes in Computer Science, vol 6697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21311-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-21311-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21310-6
Online ISBN: 978-3-642-21311-3
eBook Packages: Computer ScienceComputer Science (R0)