Reference:

Stefan Kugele. Efficient Solving of Combinatorial Problems using SAT-Solvers. Master's thesis, Technische Universität München, October 2006.

Abstract:

In this thesis we focus on Boolean Satisfiability (Sat), a classical search problem in computer science. Stephen A. Cook and Leonid Levin showed, that this problem is NP-complete, i.e., great many differently structured and at the same time practically relevant search problems can be translated to Sat in a strictly formal sense by so-called reductions.

First, we use a binary search approach and state-of-the-art Sat-solvers as decision procedure to find the chromatic number of hard graph coloring instances. We apply the presented technique successfully and are able to find for formerly unsolved benchmark problems the optimal coloring. The idea of graph coloring is taken as a basis for our second example: Inverse RNA folding denotes the process of obtaining a base assignment—restricted by biological constraints—given a 2-dimensional structure description (Secondary Structure). We introduce a reduction to perform inverse RNA folding very quickly with the help of Sat-solvers. This reduction is enhanced and adopted in a second step. To reduce the number of possible solutions we use a more realstic energy model. More specifically, we use solvers for Pseudo Boolean Optimization (PBO) problems, to optimize the inverse RNA folding process with respect to energy levels.

Finally, we deal with a number theoretical problem, namely the Ramsey numbers . Although this problem seems to be -hard, we will calculate for small inputs . A recursive algorithm to determine bounds for completes this thesis.

Suggested BibTeX entry:

@mastersthesis{kugele:diploma06,
    author = {Stefan Kugele},
    month = {October},
    school = {Technische Universit{\"a}t M{\"u}nchen},
    title = {{E}fficient {S}olving of {C}ombinatorial {P}roblems using {SAT}-{S}olvers},
    year = {2006}
}