|
Abstract:
|
Many real-world problems can be modeled as constraint satisfaction
problems (CSPs) and then solved by one of many available techniques for solving
these problems. One of the techniques is reduction to SAT, i.e. Boolean Satisfiability
Problem. Variables and constraints of CSP are translated (encoded) to SAT
instance, that is then solved by state-of-the-art SAT solvers and solution, if exists,
is translated to the solution of the original CSP. The main aim of this thesis is to
improve CSP solving techniques that are using reduction to SAT.
Two new hybrid encodings of CSPs to SAT are presented and they combine good
sides of the existing encodings. We give the proof of correctness of one encoding
that did not exist in literature. We developed system meSAT that enables reduction
of CSPs to SAT by using 4 basic and 2 hybrid encodings. The system also enables
solving of CSPs by reduction to two problems related to SAT, SMT and PB.
We developed a portfolio for automated selection of encoding/solver to be used
on some new instance that needs to be solved. The developed portfolio is comparable
with the state-of-the-art portfolios. We developed a hybrid approach based on short
solving timeouts with the aim of significantly reducing the preparation time of a
portfolio. By using this approach, we got results comparable to the ones obtained
by using preparation time of usual length. We made comparison between several
machine learning techniques with the aim to find out which one is the best suited
for the short training approach.
The problem of assigning air traffic controllers to shifts is described and three
models of this problem are presented. We used a large number of different solving
methods and a diverse set of solvers for solving this problem. We developed optimization
techniques that aim to find optimal solutions of the problem. A hybrid
technique combining reduction to SAT and local search is shown to be the most
efficient one.
We also considered sudoku puzzles and the existing techniques of solving the
puzzles of greater size than 9 9. Amongst the used techniques, the existing reduction
to SAT is the most efficient in solving these puzzles. We improved the existing
algorithm for generating large sudoku puzzles. It is shown that simple preprocessing
rules additionally improve speed of generating large sudokus. |