SAT-based local improvement for the closest string problem

Abstract

Das Closest String Problem (CSP) hat als Eingabe n Strings der Länge m über einem Alphabet A. Das Ziel ist es, einen String gleicher Länge zu finden, die den maximalen Hamming-Abstand d zu allen Eingabe-Strings minimiert. In dieser Masterarbeit fokussieren wir uns auf das CSP mit dem Alphabet A = {A, C, G, T}. Die vier Buchstaben stehen für die vier Basen, die die genetische Information in DNA-Molekülen kodieren: Adenin(A), Cytosin (C), Guanin (G) und Thymin (T). Eine praktische Anwendung besteht darin, neue DNA-Sequenzen zu erstellen, die allen vorgegebenen Eingabesequenzen ähnlich sind. Es wurde gezeigt, dass CSP NP-vollständig ist. Es stellt sich also die Frage, wie dieses Problem effizient gelöst werden kann. Für NP-vollständige Probleme können exakte Algorithmen nicht in polynomieller Zeit laufen. Heuristische Algorithmen haben hingegen den Nachteil, dass sie nicht immer die optimale Lösung liefern. Die SAT-based Local Improvement Method (SLIM) ist ein neuer Ansatz, der exakte und heuristische Methoden kombiniert, um die Vorteile beider Methoden zu nutzen. In früheren Forschungsarbeiten wurde SLIM erfolgreich auf verschiedene Probleme angewandt, wie z.B. treewidth, branchwidth und Graphenfärbung. Es hat also das Potenzial, auch für das CSP geeignet zu sein. Der SLIM-Ansatz besteht aus zwei Schritten: Im initiation step wird eine bestehende Heuristik verwendet, um eine Anfangslösung effizient zu berechnen. Danach wird im local improvement step ein lokaler Teil der bestehenden Lösung ausgewählt und durch einen SAT-Solver verbessert wird. Dieser Schritt kann beliebig oft wiederholt werden. Die Forschungsfrage dieser Arbeit lautet "Können wir SLIM nutzen, um die Lösungen aktueller Heuristiken für CSP zu verbessern?" Die Masterarbeit beschäftigt sich auch damit, was die Leistung von SLIM beeinflusst und welche Parametereinstellungen die besten Ergebnisse liefern. Um die Forschungsfrage zu beantworten, werden wir mehrere Experimente durchführen. Zunächst lassen wir eine bestehende Heuristik so lange laufen, bis sie eine erste Lösung findet. Dann verwenden wir diese Lösung als Ausgangslösung für SLIM und lassen beide Methoden parallellaufen. Nach Ablauf der vorgegebenen Zeit werden die Ergebnisse der beiden Methodenverglichen. Die Ergebnisse zeigen, dass es bereits eine gut funktionierende Heuristik gibt. Dennoch konnte unser SLIM-Ansatz die Lösung für einige der Instanzen verbessern.

The Closest String Problem (CSP) has as input n strings of length m over an alphabet A. The task is to find a string of the same length that minimizes the maximal Hamming distance d to all the input strings. In this thesis, we focus on the CSP with the alphabet A = {A, C, G, T}. The four characters represent the four bases that encode the genetic information in DNA molecules: adenine (A), cytosine (C), guanine (G), and thymine (T). One of its applications is to create new DNA sequences similar to all given input sequences. It was shown that CSP is NP-complete. Thus, the question arises of how this problem can be solved efficiently. For NP-complete problems, exact algorithms cannot run in polynomial time. On the other hand, heuristic algorithms have the downside that they do not consistently deliver the optimal solution. The SAT-based Local Improvement Method (SLIM) is a new approach that combines exact and heuristic methods to use the advantages of both methods. In previous researchSLIM was successfully applied SLIM to dierent problems, like treewidth, branchwidth, and graph coloring. So it also has the potential to be suitable for CSP. The SLIM approach consists of two steps: In the initiation step, we use an existing heuristic to compute an initial solution efficiently. Afterward, we execute the local improvement step, in which a local part of the existing solution is selected and improved by an SAT solver. This step can be executed as often as desired. The research question of this thesis is Can we use SLIM to improve the state of the art in solving the Closest String Problem? The scope of this thesis also includes finding out what influences the performance of SLIM and which parameters and adjustments deliver the best results. To answer the research question, we will conduct multiple experiments. First, we run an existing state-of-the-art heuristic until it finds one solution. Then, we use this solution as the initial solution for SLIM and let both methods run in parallel. After a global timeout, the results of both methods are compared. The results show that there already exists a well working state-of-the-art heuristic. Nevertheless, our SLIM approach could improve the solution for some of the benchmark instances.