2026-04-13T01:35:12Zhttps://recercat.cat/oai/requestoai:recercat.cat:2117/1005372025-07-17T15:52:40Zcom_2072_1033col_2072_452951
New constraint learning and inprocessing techniques for Integer Linear Programming.
Brufau Vilaró, Oriol
Universitat Politècnica de Catalunya. Departament de Ciències de la Computació
Barcelogic Solutions
Nieuwenhuis, Robert Lukas Mario
Àrees temàtiques de la UPC::Matemàtiques i estadística
Computer science
Satisfiability
0-1 ILP
Pseudo-Boolean
Unit propagation
SAT
Constraint
Informàtica
Classificació AMS::68 Computer science
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.
2017-01
Bachelor thesis
https://hdl.handle.net/2117/100537
FME-1410
eng
Restricted access - author's decision
application/pdf
Universitat Politècnica de Catalunya