Article

Journal of Automated Reasoning

, Volume 51, Issue 1, pp 79-108

Cutting to the Chase

Solving Linear Integer Arithmetic
  • Dejan JovanovićAffiliated withNew York University Email author 
  • , Leonardo de MouraAffiliated withMicrosoft Research

Rent the article at a discount

Rent now

* Final gross prices may vary according to local VAT.

Get Access

Abstract

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.

Keywords

Linear arithmetic SMT SAT DPLL Linear programming Integer arithmetic