Resumen de Sat-based techniques for combinatorial optimization

Roberto Javier Asín Acha

• The topic of this thesis is the development of SATbased techniques and tools for solving combinatorial optimization problems, together with practical experiments from different application domains, with emphasis on the (Curriculumbased) Course Timetabling problem.

  First of all, we present several contributions to the Barcelogic SAT solver. In particular, we describe new, more efficient ways of enhancing solvers like this one in order to extract unsatisfiability proofs and cores. We also show how these unsatisfiability cores are used to implement a MaxSAT solver. Additionally, we show our contributions to finding better ways for encoding very commonlyfound constraints into SAT. That is the case of Cardinality Constraints, for which we present a novel encoding. Finally, we use all these tools to tackle the Curriculumbased Course Timetabling problem using different encodings to SAT and some versions of MaxSAT and present excellent results.

  The main contribution of this thesis is related with efficient ways for tackling Timetabling Problems through SAT technologies. For this, we present novel and efficient SAT and (Weighted) (Partial) MaxSAT encodings, with wich we achieve stateoftheart results for standard 2nd International Timetabling Competition benchmarks.

  As byproducts of the thesis the following ones may be especially interesting:

  i) a new arcconsistent way for encoding cardinality constraints into SAT that needs $n \log^2 k$ clauses and $n \log^2 k$ auxiliar variables;

  ii) a number of improvements for the design, implementation and experimentation with the Barcelogic SAT Solver, that ranked as world's 3rd at the 2008 International SAT Race (Guangzhou, China, see http://baldur.iti.uka.de/satrace2008) iii) implementation and experimental analysis of several algorithms (some of them implemented for the first time) for obtaining unsatisfiability cores from a CDCL SAT solver; and iv) the design and implementation of a novel corebased Partial MaxSAT solver.