Diese Arbeit befasst sich mit Worst-Case-Algorithmen für das Erfüllbarkeitsproblem boolescher Ausdrücke in konjunktiver Normalform. Im Wesentlichen betrachten wir Laufzeitschranken drei verschiedener Algorithmen, zwei für 3-SAT und einen für Unique-k-SAT. Wir entwickeln einen randomisierten Algorithmus, der eine Lösung eines erfüllbaren 3-KNF-Ausdrucks G mit n Variablen mit einer erwarteten Laufzeit von O(1.32793^n) findet. Der Algorithmus basiert auf der Analyse sogenannter Strings, welche Sequenzen von Klauseln der Länge drei sind. Dabei dürfen einerseits nicht aufeinanderfolgende Klauseln keine Variablen und andererseits aufeinanderfolgende Klauseln ein oder zwei Variablen gemeinsam haben. Gibt es wenige Strings, so treffen wir wahrscheinlich bereits während der String-Suche auf eine Lösung von G. 1999 entwarf Schöning einen Algorithmus mit einer Schranke von O(1.3334^n) für 3-SAT. Viele Strings erlauben es, die Laufzeit dieses Algorithmusses zu verbessern. Weiterhin werden wir den PPSZ-Algorithmus für Unique-k-SAT derandomisieren. Der 1998 von Paturi, Pudlak, Saks und Zane vorgestellte PPSZ-Algorithmus hat die besondere Eigenschaft, dass die Lösung eines eindeutig erfüllbaren 3-KNF-Ausdrucks in höchstens O(1.3071^n) erwarteter Laufzeit gefunden wird. Die derandomisierte Variante des Algorithmusses für Unique-k-SAT hat im Wesentlichen die gleiche Laufzeitschranke. Wir erreichen damit die momentan beste deterministische Worst-Case-Schranke für Unique-k-SAT. Zur Derandomisierung wenden wir die "Methode der kleinen Zufallsräume" an. Schließlich verbessern wir die Schranke für den Algorithmus von Iwama und Tamaki. 2003 kombinierten Iwama und Tamaki den PPSZ-Algorithmus mit Schönigs Algorithmus und konnten eine Schranke von O(1.3238^n) bewiesen. Um seinen Beitrag zum kombinierten Algorithmus zu steigern, justieren wir die Schranke des PPSZ-Algorithmusses. Damit erhalten wir die momentan beste randomisierte Worst-Case-Schranke für das 3-SAT-Problem von O(1.32216^n). / This work deals with worst-case algorithms for the satisfiability problem regarding boolean formulas in conjunctive normal form. The main part of this work consists of the analysis of the running time of three different algorithms, two for 3-SAT and one for Unique-k-SAT. We establish a randomized algorithm that finds a satisfying assignment for a satisfiable 3-CNF formula G on n variables in O(1.32793^n) expected running time. The algorithm is based on the analysis of so-called strings, which are sequences of clauses of size three, whereby non-succeeding clauses do not share a variable, and succeeding clauses share one or two variables. If there are not many strings, it is likely that we already encounter a solution of G while searching for strings. In 1999, Schöning proved a bound of O(1.3334^n) for 3-SAT. If there are many strings, we use them to improve the running time of Schöning''s algorithm. Furthermore, we derandomize the PPSZ algorithm for Unique-k-SAT. The PPSZ algorithm presented by Paturi, Pudlak, Saks, and Zane in 1998 has the feature that the solution of a uniquely satisfiable 3-CNF formula can be found in expected running time at most O(1.3071^n). In general, we will obtain a derandomized version of the algorithm for Unique-k-SAT that has essentially the same bound as the randomized version. This settles the currently best known deterministic worst-case bound for the Unique-k-SAT problem. We apply the `Method of Small Sample Spaces'' in order to derandomize the algorithm. Finally, we improve the bound for the algorithm of Iwama and Tamaki to get the currently best known randomized worst-case bound for the 3-SAT problem of O(1.32216^n). In 2003 Iwama and Tamaki combined Schöning''s and the PPSZ algorithm to yield an O(1.3238^n) bound. We tweak the bound for the PPSZ algorithm to get a slightly better contribution to the combined algorithm.

Today more and more different types of autonomous robots and vehicles are being developed. Most of these rely on the global positioning system and/or communication with other robots and vehicles to determine their global position. However, these are not viable options for the autonomous underwater vehicles (AUVs) of today since radio-waves does not travel well in water. Instead, various techniques for determining the AUVs position are used which comes with a margin of error. This thesis examines the problem of efficiently performing a local search within this margin of error with the objective of finding a docking-station or a bouy.To solve this problem research was made on the subject of search theory and how it previously has been applied in this context. What was found was that classical bayesian search theory had not been used very often in this context since it would require to much processing power to be a viable option in the embedded systems that is AUVs. Instead different heuristics were used to get solutions that still were viable for the situations in which they were used, even though they maybe wasn’t optimal.Based on this the search-strategies Spiral, Greedy, Look-ahead and Quadtree were developed and evaluated in a simulator. Their mean time to detection (MTTD) were compared as well as the average time it took for the strategies to process a search. Look-ahead was the best one of the four different strategies with respect to the MTTD and based on this it is suggested that it should be implemented and evaluated in a real AUV. / Idag utvecklas allt fler olika typer av autonoma robotar och fordon. De flesta av dessa är beroende av det globala positioneringssystemet och/eller kommunikation med andra robotar och fordon för att bestämma deras globala position. Detta är dock inte realistiska alternativ för autonoma undervattensfordon (AUV) idag eftersom radiovågor inte färdas bra i vatten. I stället används olika tekniker för att bestämma AUVens position, tekniker som ofta har en felmarginal. Denna rapport undersöker problemet med att effektivt utföra en lokal sökning inom denna felmarginal med målet att hitta en dockningsstation eller en boj.För att lösa detta problem gjordes en litteraturstudie om ämnet sökteori och hur det tidigare har tillämpats i detta sammanhang. Det som hittades var att den klassiska bayesiska sökteorin inte hade använts mycket ofta i detta sammanhang eftersom det skulle kräva för mycket processorkraft för att det skulle vara ett rimligt alternativ för de inbyggda systemen på en AUV. Istället användes olika heuristiska metoder för att få lösningar som fortfarande var dugliga för de situationer där de användes, även om de kanske inte var optimala.Baserat på detta utvecklades sökstrategierna Spiral, Greedy, Look-ahead och Quad-tree och utvärderades i en simulator. Deras genomsnittliga tid för att upptäcka målet (MTTD) jämfördes liksom den genomsnittliga tiden det tog för strategierna att bearbeta en sökning. Look-ahead var den bästa av de fyra olika strategierna med avseende på MTTD och baserat på detta föreslås det att den ska implementeras och utvärderas i en verklig AUV.