Diese Arbeit untersucht verschiedene Branching-Heuristiken für DPLL basierte SAT-Solver und deren Einfluss auf die Lösungszeit sowie die Suchraumgröße. Dazu wurden die Heuristiken Jeroslow-Wang, 2-Sided Jeroslow-Wang, Maximum Occurences on clauses of Minimum Size und zufälliges Verzweigen implementiert und auf Benchmark-Instanzen getestet. Die Ergebnisse zeigen, dass Maximum Occurences on clauses of Minimum Size bei strukturierten Problemen die besten Laufzeiten erzielt. Eine Optimierung durch Memoization und Formelvorverarbeitung führte zu einer Reduktion der Berechnungszeiten.

This thesis analyses different branching heuristics for DPLL based SAT solvers and their influence on the solution time and the search space size. For this purpose, the heuristics Jeroslow-Wang, 2-Sided Jeroslow-Wang, Maximum Occurences on clauses of Minimum Size and RandomBranching were implemented and tested on benchmark instances. The results show that Maximum Occurences on clauses of Minimum Size achieves the best runtimes for structured problems. Optimisation through memoisation and preprocessing led to a reduction in runtimes.