Moderne, digitale Elektronik ist so komplex, dass die Sicherstellung ihrer korrekten Funktion zur Zeit der zeitaufwändigste Teil der Entwicklung ist. Formale Verifikation ermöglicht es, funktionale Eigenschaften solcher Systeme automatisch und vollständig zu überprüfen, ohne dass der Entwickler zeitraubende und fehleranfällige Tests für jeden Einzelfall schreiben muss. Die Eigenschaften werden in Instanzen des Erfüllbarkeitsproblems der Aussagenlogik (SAT, von engl. satisfiability) übersetzt, die dann mit Erfüllbarkeitsprüfer-Software (auch SAT-Solver genannt) gelöst werden können. Die derzeit besten SAT-Solver für industrielle Anwendungen basieren auf verbesserten Versionen des DPLL-Algorithmus. DPLL ist ein Suchalgorithmus, der von einer Vielzahl von Heuristiken gesteuert wird. Die zur Lösung eines SAT-Problems benötigte Zeit ist stark abhängig von der Wahl der Parameter dieser Heuristiken, und die optimale Einstellung der Parameter ist selbst ein schwieriges Problem. In der vorliegenden Arbeit wird ein neues, vollautomatisches Optimierungsverfahren für die Heuristikparameter von SAT-Solvern präsentiert und getestet. Das Verfahren basiert auf der Benutzung von Optimierungsalgorithmen, mit denen versucht wird, optimale Parameterkonfigurationen für Trainingsmengen von SAT-Problemen anzunähern. Ein Endergebnis wird dann aus allen gesammelten Daten berechnet. Als Optimierungsalgorithmen wurden zwei Unterarten von Evolutionären Algorithmen getestet: Genetische Algorithmen und Evolutionsstrategien. Der zu optimierende SAT-Solver war das bekannte Open Source Programm MINISAT. Es konnte gezeigt werden, dass die Parameterkonfigurationen, die mit dem Verfahren erzeugt wurden, ähnlich gut sind wie die von Experten ermittelten Standardparameter.