Cutting to the Chase Solving Linear Integer Arithmetic

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.

• Type: Journal
• Year: 2011
• Where: CADE
• Authors: Dejan Jovanovic, Leonardo Mendonça de Moura
• Keywords: CADE 2011, Integer Programming Problems, Linear Integer, Logical Reasoning, Style Search