El tema d'aquesta tesi és el desenvolupament de tècniques i eines basades en SAT per solucionar problemes combinatoris industrials. Primer, descrivim l'arquitectura dels SAT i SMT Solvers actuals, basats en l'algorisme DPLL. Aquests sistemes es poden usar com a caixes negres per resoldre problemes combinatoris. Malgrat això, sovint podem incrementar la seva eficiència amb petites modificacions de l'algorisme bàsic. Per això, el primer objectiu de la tesi és l'estudi i desenvolupament de tècniques per ajustar els SAT Solvers a problemes combinatoris concrets. Els SAT Solvers només poden tractar lògica proposicional. Per resoldre problemes combinatoris generals, es poden considerar els següents mètodes:¿Reduir els constraints complexos a clàusules proposicionals.¿Enriquir el llenguatge del SAT Solver. El primer mètode correspon a codificar un constraint a SAT. El segon, a usar propagadors, la peça bàsica dels SMT Solvers. Respecte el primer mètode, en aquest document millorem la codificació de dos dels constraints combinatoris més importants: els cardinality i els pseudo-Boolean constraints. Després, presentem un mètode mixt, anomenat "lazy decomposition", que combina els avantatges de propagadors i codificacions.L'altre part de la tesi usa aquestes millores teòriques en problemes combinatoris industrials. Donem un mètode per construir eficientment amb SAT calendaris per algunes lligues esportives professionals. Els resultats són prometedors i mostren que SAT és una eina vàlida per aquests problemes.Malgrat això, el comportament caòtic dels SAT Solvers basats en CDCL, degut a les heurístiques VSIDS, fan difícil que s'obtinguin resultats similars en dos problemes semblants. Això pot ser un inconvenient en problemes del món real, ja que els usuaris esperen obtenir solucions semblants quan es modifica lleugerament l'especificació del problema. Per resoldre aquesta limitació, hem estudiat i resolt el problema de close solution, és a dir, el problema de trobar ràpidament solucions properes quan es consideren problemes similars.
The topic of this thesis is the development of SAT-based techniques and tools for solving industrial combinatorial problems. First, it describes the architecture of state-of-the-art SAT and SMT Solvers based on the classical DPLL procedure. These systems can be used as black boxes for solving combinatorial problems. However, sometimes we can increase their efficiency with slight modifications of the basic algorithm. Therefore, the study and development of techniques for adjusting SAT Solvers to specific combinatorial problems is the first goal of this thesis.
Namely, SAT Solvers can only deal with propositional logic. For solving general combinatorial problems, two different approaches are possible:
- Reducing the complex constraints into propositional clauses.
- Enriching the SAT Solver language.
The first approach corresponds to encoding the constraint into SAT. The second one corresponds to using propagators, the basis for SMT Solvers. Regarding the first approach, in this document we improve the encoding of two of the most important combinatorial constraints: cardinality constraints and pseudo-Boolean constraints. After that, we present a new mixed approach, called lazy decomposition, which combines the advantages of encodings and propagators.
The other part of the thesis uses these theoretical improvements in industrial combinatorial problems. We give a method for efficiently scheduling some professional sport leagues with SAT. The results are promising and show that a SAT approach is valid for these problems.
However, the chaotical behavior of CDCL-based SAT Solvers due to VSIDS heuristics makes it difficult to obtain a similar solution for two similar problems. This may be inconvenient in real-world problems, since a user expects similar solutions when it makes slight modifications to the problem specification. In order to overcome this limitation, we have studied and solved the close solution problem, i.e., the problem of quickly finding a close solution when a similar problem is considered.