Journal of Automated Reasoning

, Volume 51, Issue 1, pp 79–108

Cutting to the Chase

Solving Linear Integer Arithmetic

DOI: 10.1007/s10817-013-9281-x

Cite this article as:
Jovanović, D. & de Moura, L. J Autom Reasoning (2013) 51: 79. doi:10.1007/s10817-013-9281-x


We describe a new algorithm for solving linear integer programming problems. The algorithm performs a DPLL style search for a feasible assignment, while using a novel cut procedure to guide the search away from the conflicting states.


Linear arithmetic SMT SAT DPLL Linear programming Integer arithmetic 

Copyright information

© Springer Science+Business Media Dordrecht 2013

Authors and Affiliations

  1. 1.New York UniversityNew YorkUSA
  2. 2.Microsoft ResearchRedmondUSA

Personalised recommendations