Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning

Robert Nieuwenhuis, Albert Oliveras, Enric Rodriguez-Carbonell

TL;DR

IntSat advances SAT-style conflict-driven learning to Integer Linear Programming by introducing bound propagation, decision handling, and conflict analysis that operate directly on linear constraints. It presents two concrete variants—resolution-based and cut-based—along with extensions for optimisation and practical implementation strategies, including bound-propagation filters, early backjumps, and clause-specific handling. Experimental results on MIPLIB-based benchmarks show that IntSat can outperform or complement mature simplex-based solvers on several feasible and combinatorial instances, particularly when fast first solutions are valuable. The work demonstrates that a CDCL-inspired ILP framework can meaningfully contribute to the ILP toolbox, with clear directions for unboundedness handling, database management, and MILP/binary ILP extensions achieving broader applicability.

Abstract

State-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the so-called Conflict-Driven Clause-Learning (CDCL) scheme, which encompasses a number of techniques that exploit the conflicts that are encountered during the search for a solution. In this article we extend these techniques to Integer Linear Programming (ILP), where variables may take general integer values instead of purely binary ones, constraints are more expressive than just propositional clauses, and there may be an objective function to optimise. We explain how these methods can be implemented efficiently, and discuss possible improvements. Our work is backed with a basic implementation that shows that, even in this far less mature stage, our techniques are already a useful complement to the state of the art in ILP solving.

IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning

TL;DR

IntSat advances SAT-style conflict-driven learning to Integer Linear Programming by introducing bound propagation, decision handling, and conflict analysis that operate directly on linear constraints. It presents two concrete variants—resolution-based and cut-based—along with extensions for optimisation and practical implementation strategies, including bound-propagation filters, early backjumps, and clause-specific handling. Experimental results on MIPLIB-based benchmarks show that IntSat can outperform or complement mature simplex-based solvers on several feasible and combinatorial instances, particularly when fast first solutions are valuable. The work demonstrates that a CDCL-inspired ILP framework can meaningfully contribute to the ILP toolbox, with clear directions for unboundedness handling, database management, and MILP/binary ILP extensions achieving broader applicability.

Abstract

State-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the so-called Conflict-Driven Clause-Learning (CDCL) scheme, which encompasses a number of techniques that exploit the conflicts that are encountered during the search for a solution. In this article we extend these techniques to Integer Linear Programming (ILP), where variables may take general integer values instead of purely binary ones, constraints are more expressive than just propositional clauses, and there may be an objective function to optimise. We explain how these methods can be implemented efficiently, and discuss possible improvements. Our work is backed with a basic implementation that shows that, even in this far less mature stage, our techniques are already a useful complement to the state of the art in ILP solving.
Paper Structure (33 sections, 10 theorems, 49 equations, 1 figure, 4 tables)

This paper contains 33 sections, 10 theorems, 49 equations, 1 figure, 4 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Propositional Satisfiability
  4. Integer Linear Programming
  5. IntSat
  6. The Rounding Problem
  7. Bound Propagation
  8. The Core IntSat Algorithm
  9. Resolution-based IntSat
  10. Hybrid Resolution and Cut-based IntSat
  11. Extensions of IntSat
  12. Implementation
  13. Bound propagation using filters
  14. Early backjumps
  15. Clauses
  16. ...and 18 more sections

Key Result

Lemma 3.4

Let $C$ be a constraint of the form $a_1 x_1 + \ldots + a_nx_n \preceq a_0$ and $A$ be a set of pairwise non-contradictory bounds. The following hold:

Figures (1)

  • Figure 1: Example of bounds vector (left) and stack (right).

Theorems & Definitions (38)

  • Example 2.1
  • Example 2.2
  • Example 3.1
  • Example 3.2
  • Definition 3.3: False constraint, conflict
  • Lemma 3.4
  • proof
  • Lemma 3.5
  • proof
  • Definition 3.6: Bound propagation
  • ...and 28 more