Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications

  • D. Chubarov
  • A. Voronkov
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3618)


We define a basis of solutions of a system of linear inequalities and present a general algorithm for finding such a basis. Our algorithm relies on an algorithm for finding a Hilbert basis for the set of nonnegative solutions of a system of linear inequalities and can be used in conjunction with any such algorithm.


Model Check Linear Inequality Nonnegative Solution Integral Vector Full Column Rank 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aardal, K., Weismantel, R., Wolsey, L.A.: Non-standard approaches to integer programming. Discrete Applied Mathematics 123(1-3), 5–74 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Ajili, F., Contejean, E.: Avoiding slack variables in the solving of linear Diophantine equations and inequations. Theoret. Comput. Sci. 173, 183–208 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Bockmayr, A., Weispfenning, V.: Solving numerical constraints. In: Robinson, A., Voronkov, A. (eds.) Hanbook of Automated Reasoning, ch. 12, vol. I, pp. 751–842. Elsevier Science, Amsterdam (2001)CrossRefGoogle Scholar
  4. 4.
    Bruns, W., Gubeladze, J., Henk, M., Martin, A., Weismantel, R.: A counterexample to an integer analogue of Carathéodory’s theorem. J. Reine Angew. Math. 510, 179–185 (1999)zbMATHMathSciNetCrossRefGoogle Scholar
  5. 5.
    Domenjoud, E.: Solving systems of linear Diophantine equations: An algebraic approach. In: Tarlecki, A. (ed.) MFCS 1991. LNCS, vol. 520, pp. 141–150. Springer, Heidelberg (1991)Google Scholar
  6. 6.
    Durand, A., Hermann, M., Juban, L.: On the complexity of recognizing the hilbert basis of a linear diophantine system. In: Kutylowski, M., Pacholski, L., Wierzbicki, T. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 92–102. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Filgueiras, M., Tomás, A.P.: A fast method for finding the basis of nonnegative solutions to a linear Diophantine equation. J. Symbolic Comput. 19, 507–526 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Filgueiras, M., Tomás, A.P.: Solving linear Diophantine equations using the geometric structure of the solution space. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 269–283. Springer, Heidelberg (1997)Google Scholar
  9. 9.
    Giles, R., Pulleyblank, W.R.: Total dual integrality and integer polyhedra. Linear Algebra and Appl. 25, 191–196 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Gordan, P.: Über die auflösung linearer gleichungen mit reellen coefficienten. Math. Ann. 6, 23–28 (1873)CrossRefMathSciNetGoogle Scholar
  11. 11.
    Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 333–346. Springer, Heidelberg (1993)Google Scholar
  12. 12.
    Hemmecke, R.: On the computation of Hilbert bases and extreme rays of cones. E-print arXiv:math.CO/0203105 (March 2002)Google Scholar
  13. 13.
    Henk, M., Weismantel, R.: On minimal solutions of linear diophantine equations. Contrib. Algebra and Geometry 41(1), 49–55 (2000)zbMATHMathSciNetGoogle Scholar
  14. 14.
    Henzinger, T., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 460–463. Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Hermann, M., Juban, L., Kolaitis, P.G.: On the complexity of counting the hilbert basis of a linear diophnatine system. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, pp. 13–32. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Hilbert, D.: Über die endlichkeit des invariantensystems für binäre grundformen. Math. Ann. 33, 223–226 (1888) (In German)CrossRefMathSciNetGoogle Scholar
  17. 17.
    Huet, G.P.: An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations. Inform. Process. Lett. 7, 144–147 (1978)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Lambert, J.: Une borne pour générateurs des solutions entière positives d’une équation diophantienne linéaire (A bound for the minimal positive integer solutions of a linear diophantine equation) (in French). C. R. Acad. Sci. Paris Sér. I Math. 305, 39–40 (1987)zbMATHGoogle Scholar
  19. 19.
    Mayr, E.W.: Some complexity results for polynomial ideals. J. Complexity 13(3), 303–325 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Micciancio, D., Warinschi, B.: A linear space algorithm for computing the Hermite normal form. In: proceedings ISAAC 2001, pp. 231–236. ACM, New York (2001)Google Scholar
  21. 21.
    Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Pasechnik, D.V.: On computing Hilbert bases via the Elliot–MacMahon algorithm. Theoret. Comput. Sci. 263, 37–46 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Pottier, L.: Minimal solutions of linear diophantine systems: Bounds and algorithms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 162–173. Springer, Heidelberg (1991)Google Scholar
  24. 24.
    Rybina, T., Voronkov, A.: Using canonical representations of solutions to speed up infinite-state model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 386–400. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  25. 25.
    Rybina, T., Voronkov, A.: Fast infinite-state model checking in integer-based systems. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 546–573. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  26. 26.
    Schrijver, A.: Theory of Linear and Integer Programming. John Wiley, Chichester (1998)zbMATHGoogle Scholar
  27. 27.
    Schulz, A., Weismantel, R.: An oracle-polynomial time augmentation algorithm for integer programming. In: proceedings ACM–SIAM SODA 1999, pp. 967–968 (1999)Google Scholar
  28. 28.
    Sebő, A.: Hilbert bases, Caratheodory’s theorem and combinatorial optimization. In: Kannan, R., Pulleyblank, W.R. (eds.) Proceedings IPCO 1990, pp. 431–455. University of Waterloo Press (1990)Google Scholar
  29. 29.
    Stickel, M.E.: A unification algorithm for associative-commutative functions. J. ACM 28, 423–434 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  30. 30.
    van der Corput, J.G.: Über systeme von linear-homogenen Gleichungen und Ungleichungen. Proc. Roy. Acad. Amsterdam 34, 368–371 (1931) (in German)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • D. Chubarov
    • 1
  • A. Voronkov
    • 1
  1. 1.The University of Manchester 

Personalised recommendations