Solving hard industrial combinatorial problems with SAT
Visualitza/Obre
10.5821/dissertation-2117-94935
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/94935
Tutor / directorNieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric
Càtedra / Departament / Institut
Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics
Tipus de documentTesi
Data de defensa2013-05-15
EditorUniversitat Politècnica de Catalunya
Condicions d'accésAccés obert
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement 3.0 Espanya
Abstract
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.
CitacióAbío Roig, I. Solving hard industrial combinatorial problems with SAT. Tesi doctoral, UPC, Departament de Llenguatges i Sistemes Informàtics, 2013. DOI 10.5821/dissertation-2117-94935. Disponible a: <http://hdl.handle.net/2117/94935>
Dipòsit legalB. 19941-2013
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
TIAR1de1.pdf | 1,107Mb | Visualitza/Obre |