Titelaufnahme

Titel
Max 3-SAT - Modelle, Heuristiken und Implementationen / Christian Kofler
Verfasser/ VerfasserinKofler, Christian
Begutachter / BegutachterinGreistorfer Peter
Erschienen2013
UmfangV, 82 Bl. : 2 Zsfassungen
HochschulschriftGraz, Univ., Masterarb., 2013
Anmerkung
Zsfassung in dt. und engl. Sprache
SpracheDeutsch
DokumenttypMasterarbeit
Schlagwörter (GND)Erfüllbarkeitsproblem / Algorithmus / Programm / Erfüllbarkeitsproblem / Algorithmus / Programm / Online-Publikation
URNurn:nbn:at:at-ubg:1-51805 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Max 3-SAT - Modelle, Heuristiken und Implementationen [1.02 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Seit mittlerweile über 40 Jahren ist das SAT Problem, auf Deutsch das Erfüllbarkeitsproblem, eine der zentralen Fragestellungen in der Entscheidungstheorie. Nachdem festgestellt wurde, dass es sich hierbei um ein NP-vollständiges Problem handelt, ist die Wissenschaft auf der Suche nach effizienten Heuristiken. Es begann auf der ganzen Welt ein regelrechter Wettbewerb, da das SAT Problem eine wichtige Rolle bei der Entwicklung von Computersystemen einnimmt. Das 3-SAT Problem besitzt in diesem Forschungsbereich eine Vorreiterstellung. Diese Masterarbeit ist Teil einer Forschungsgemeinschaft von Amerikanischen Universitäten und der Grazer Universität zur Entwicklung zweier Algorithmen zur Berechnung von solchen 3-SAT Problemen. Das Hauptaugenmerk dieser Arbeit liegt in der programmiertechnischen Umsetzung der Algorithmen und der Auswertung und Beurteilung erster Ergebnisse. In einem ersten Abschnitt wird die Konstruktion der Zielfunktion für beide Computerprogramme beschrieben. Dabei werden die Clauses in ein diskretes Entscheidungsproblem ohne Nebenbedingungen umgewandelt. Dieser Vorgang geschieht mit Hilfe sogenannter Penaltyfunktionen. Bei dem ersten Computerprogramm zur Lösung der Zielfunktion handelt es sich um die xQx-Methode. Diese Methode lässt jedoch nur lineare und quadratische Terme in der Zielfunktion zu. Aus diesem Grund wird in einem ersten Schritt mittels einer Heuristik die Funktion dritter Ordnung durch Einführung zusätzlicher Variablen reduziert. Anschließend wird das Gleichungssystem der Form xQx mit Hilfe des LocalSolvers gelöst. Die zweite Berechnungsmethode ist eine Ausprägung der Simple One-Pass Heuristik. Bei diesem Algorithmus handelt es sich um ein Gewichtungsverfahren, wo schrittweise die Lösung der Variablen bestimmt wird. Der Vorteil gegenüber der xQx-Methode liegt darin, dass keine neuen Variablen eingefügt werden müssen. Aus diesem Grund sind die Berechnungszeiten bei diesem Verfahren auch wesentlich geringer.

Zusammenfassung (Englisch)

For more than 40 years, the satisfiability problem (SAT) has been one of the central issues in the theory of computation. Since it was determined that it is a NP-complete problem, scientists are looking for efficient heuristics. Because of the fact that the SAT problem plays an important role in the development of efficient computer systems, a real competition to find heuristics started all over the world. 3-SAT has a pioneering role in this research. This thesis is part of the work of a research community of American universities and the University of Graz. It?s goal is the development of two algorithms for the computation of such 3-SAT problems. The main focus of this work lies on the implementation of the algorithms. Furthermore, a first analysis and evaluation of the results should be performed. In the first part of the paper, the construction of the objective function for both computer programs is described. In this context, the clauses are converted into a discrete decision problem without constraints. This process is done with the help of penalty functions. The first computer program used in order to solve the objective function is the xQx-method. This approach allows only linear and quadratic terms in the objective function. For this reason, in a first step, the cubic terms have to be eliminated. This happens by implementing additional variables and penalty functions. Finally, the system of equations is solved with the use of a program called LocalSolver. The second method is a type of Simple One-Pass heuristic. This algorithm is basically a weighting method that determines the solution of the decision variables step by step. The advantage of this in comparison to the xQx-method is that no new variables need to be introduced. Therefore, the time of the calculation is significantly lower.