IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916136139882496 |
|---|---|
| author | Nieuwenhuis, Robert Oliveras, Albert Rodriguez-Carbonell, Enric |
| author_facet | Nieuwenhuis, Robert Oliveras, Albert Rodriguez-Carbonell, Enric |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2402_15522 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning Nieuwenhuis, Robert Oliveras, Albert Rodriguez-Carbonell, Enric Artificial Intelligence I.2.8; F.4.1 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. |
| title | IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning |
| topic | Artificial Intelligence I.2.8; F.4.1 |
| url | https://arxiv.org/abs/2402.15522 |