A Graphical Analysis of Integer Infeasibility in UTVPI Constraints

  • K. SubramaniEmail author
  • Piotr Wojciechowski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11946)


In this paper, we discuss a theorem of the alternative for integer feasibility in a class of constraints called Unit Two Variable Per Inequality (UTVPI) constraints. In general, a theorem of the alternative gives two systems of constraints such that exactly one system is feasible. Theorems of the alternative for linear feasibility have been discussed extensively in the literature. If a theorem of the alternative provides a “succinct” certificate of infeasibility, it is said to be compact. In general, theorems of the alternative for linear feasibility are compact (see Farkas’ lemma for instance). However, compact theorems of the alternative cannot exist for integer feasibility in linear programs unless NP\(\,=\,\)coNP. A second feature of a theorem of the alternative is its form. Typically, theorems of the alternative connect pairs of linear systems. A graphical theorem of the alternative, on the other hand, connects infeasibility in a linear system to the existence of particular paths in an appropriately constructed constraint network. Graphical theorems of the alternative are known to exist for selected classes of linear programs. In this paper, we detail a compact, graphical theorem of the alternative for integer feasibility in UTVPI constraints.



This research was supported in part by the Air-Force Office of Scientific Research through grant FA9550-19-1-017.


  1. 1.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Form. Methods Syst. Des. 35(3), 279–323 (2009)CrossRefGoogle Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Dax, A.: Classroom note: an elementary proof of Farkas’ lemma. SIAM Rev. 39(3), 503–507 (1997)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Farkas, G.: Über die Theorie der Einfachen Ungleichungen. J. für die Reine und Angewandte Mathematik 124(124), 1–27 (1902)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Gale, D.: The Theory of Linear Economic Models. McGraw-Hill, New York (1960)zbMATHGoogle Scholar
  6. 6.
    Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471–479 (1995)CrossRefGoogle Scholar
  7. 7.
    Gordan, P.: Ueber die auflösung linearer gleichungen mit reellen coefficienten. Math. Ann. 6(1), 23–28 (1873)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Hurkens, C.A.J.: On the existence of an integral potential in a weighted bidirected graph. Linear Algebr. Appl. 114–115, 541–553 (1989). Special Issue Dedicated to Alan J. HoffmanMathSciNetCrossRefGoogle Scholar
  9. 9.
    Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 168–183. Springer, Heidelberg (2005). Scholar
  10. 10.
    Lasserre, J.B.: Integer programming, Barvinok’s counting algorithm and Gomory relaxations. Oper. Res. Lett. 32(2), 133–137 (2004)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Marlow, W.H.: Mathematics for Operations Research. Wiley, Hoboken (1978)zbMATHGoogle Scholar
  12. 12.
    Miné, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31–100 (2006)CrossRefGoogle Scholar
  13. 13.
    Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley, New York (1999)zbMATHGoogle Scholar
  14. 14.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987)zbMATHGoogle Scholar
  15. 15.
    Schrijver, A.: Disjoint circuits of prescribed homotopies in a graph on a compact surface. J. Comb. Theory, Ser. B 51(1), 127–159 (1991)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Schutt, A., Stuckey, P.J.: Incremental satisfiability and implication for UTVPI constraints. INFORMS J. Comput. 22(4), 514–527 (2010)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Sitzmann, I., Stuckey, P.J.: O-trees: a constraint-based index structure. In: Australasian Database Conference, pp. 127–134 (2000)Google Scholar
  18. 18.
    Stiemke, E.: Über positive lösungen homogener linearer gleichungen. Math. Ann. 76(2), 340–342 (1915)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Subramani, K.: On deciding the non-emptiness of 2SAT polytopes with respect to first order queries. Math. Log. Q. 50(3), 281–292 (2004)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Subramani, K., Wojciechowski, P.J.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166–208 (2017)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Vohra, R.V.: The ubiquitous Farkas’ lemma. In: Alt, F.B., Fu, M.C., Golden, B.L. (eds.) Perspectives in Operations Research. ORCS, vol. 36, pp. 199–210. Springer, New York (2006). Scholar
  22. 22.
    Williams, H.P.: Model Building in Mathematical Programming, 4th edn. Wiley, Hoboken (1999)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.LDCSEEWest Virginia UniversityMorgantownUSA

Personalised recommendations