Algorithms for the satisfiability problem [Elektronische Ressource] / von Daniel Rolf

Algorithms for theSatisfiability ProblemDISSERTATIONzur Erlangung des akademischen Gradesdoctor rerum naturalium(Dr. rer. nat.)im Fach Informatikeingereicht an derMathematisch-Naturwissenschaftlichen Fakultät IIHumboldt-Universität zu BerlinvonHerrn Dipl.-Inf. Daniel Rolfgeboren am 5.1.1979 in NeuruppinPräsident der Humboldt-Universität zu Berlin:Prof. Dr. Christoph MarkschiesDekan der Mathematisch-Naturwissenschaftlichen Fakultät II:Prof. Dr. Wolfgang CoyGutachter:1. Prof. Dr. Martin Grohe2. Prof. Dr. Stephan Kreutzer3. Prof. Dr. Walter Kerneingereicht am: 30. Mai 2006Tag der mündlichen Prüfung: 17. November 2006AbstractThis work deals with worst-case algorithms for the satisfiability problem regardingboolean formulas in conjunctive normal form. The main part of this work consistsof the analysis of the running time of three different algorithms, two for 3-SATand one for Unique-k-SAT.Research on the satisfiability problem has made reasonable progress during thelast years. After the introduction in Chapter 1, we will study some interestingalgorithms and their running time bounds in Chapter 2.In Chapter 3, we establish a randomized algorithm that finds a satisfying as-nsignmentforasatisfiable3-CNFformulaGonnvariablesinO(1.32793 )expectedrunning time.