New constraint learning and inprocessing techniques for Integer Linear Programming.
Oriol Brufau Vilaró · RECERCAT (Consorci de Serveis Universitaris de Catalunya) · 2017
The IntSat procedure [Nieuwenhuis 2014] is a complete method for Integer Linear Programming (ILP) based on conflict-driven constraint learning, extending similar ideas used in propositional satisfiability solving (SAT). The aim of this project is, restricted to the Pseudo-Boolean ILP case, to extend this method with new inprocessing techniques, proving the associated correctness and completeness properties, developing data structures and algorithms for their implementation, and providing a careful and extensive experimental assessment for them.