TU Darmstadt / ULB / TUbiblio

Soft Computing Approaches to DPLL SAT Solver Optimization

Kibria, Raihan Hassnain (2011)
Soft Computing Approaches to DPLL SAT Solver Optimization.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Digital electronic systems are now so large and complex that ensuring their correct functionality has become the most time-consuming part of their design. Formal verification allows the exhaustive, automatic testing of functional properties of such systems without requiring the designer to create individual test cases manually, which is time-consuming as well as prone to errors and oversights. The properties are first transformed into instances of the Boolean satifiability problem (SAT), which are then solved with SAT solvers. The most efficient SAT solvers for industrial SAT problems are based on enhanced versions of the DPLL algorithm which employs a number of heuristics to guide the search for a solution. Solving times are highly dependent on the choice of the solver's heuristic parameters, and adjusting the heuristics optimally is a complex task in itself. This work presents and tests a new, fully automatic optimization procedure for a SAT solver's heuristic parameters that is based on using local search algorithms which attempt to find optimal parameters for training sets of SAT problems; a result configuration is synthesized from the gathered data. For the optimization two subtypes of Evolutionary Algorithms (local search algorithms that mimic Darwinian evolution), Genetic Algorithms and Evolution Strategies, were tested. The target of optimization was the well known open-source SAT solver MiniSAT. It could be shown that the parameter configurations generated by the automatic procedure are competitive with the default parameters set by human experts.

Typ des Eintrags: Dissertation
Erschienen: 2011
Autor(en): Kibria, Raihan Hassnain
Art des Eintrags: Erstveröffentlichung
Titel: Soft Computing Approaches to DPLL SAT Solver Optimization
Sprache: Englisch
Referenten: Eveking, Dr.-Ing. Hans
Publikationsjahr: 27 September 2011
Datum der mündlichen Prüfung: 23 September 2011
URL / URN: urn:nbn:de:tuda-tuprints-27597
Kurzbeschreibung (Abstract):

Digital electronic systems are now so large and complex that ensuring their correct functionality has become the most time-consuming part of their design. Formal verification allows the exhaustive, automatic testing of functional properties of such systems without requiring the designer to create individual test cases manually, which is time-consuming as well as prone to errors and oversights. The properties are first transformed into instances of the Boolean satifiability problem (SAT), which are then solved with SAT solvers. The most efficient SAT solvers for industrial SAT problems are based on enhanced versions of the DPLL algorithm which employs a number of heuristics to guide the search for a solution. Solving times are highly dependent on the choice of the solver's heuristic parameters, and adjusting the heuristics optimally is a complex task in itself. This work presents and tests a new, fully automatic optimization procedure for a SAT solver's heuristic parameters that is based on using local search algorithms which attempt to find optimal parameters for training sets of SAT problems; a result configuration is synthesized from the gathered data. For the optimization two subtypes of Evolutionary Algorithms (local search algorithms that mimic Darwinian evolution), Genetic Algorithms and Evolution Strategies, were tested. The target of optimization was the well known open-source SAT solver MiniSAT. It could be shown that the parameter configurations generated by the automatic procedure are competitive with the default parameters set by human experts.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

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.

Deutsch
Schlagworte:
Einzelne SchlagworteSprache
DPLL SAT EA ES GA OptimizationEnglisch
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Fachbereich(e)/-gebiet(e): 18 Fachbereich Elektrotechnik und Informationstechnik
20 Fachbereich Informatik
Hinterlegungsdatum: 28 Sep 2011 09:03
Letzte Änderung: 05 Mär 2013 09:54
PPN:
Referenten: Eveking, Dr.-Ing. Hans
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 23 September 2011
Schlagworte:
Einzelne SchlagworteSprache
DPLL SAT EA ES GA OptimizationEnglisch
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen