Soft Computing Approaches to DPLL SAT Solver Optimization

Created by W.Langdon from gp-bibliography.bib Revision:1.3872

@PhdThesis{rkibria-dissertation-final-korrigiert1,
  author =       "Raihan Hassnain Kibria",
  title =        "Soft Computing Approaches to {DPLL SAT} Solver
                 Optimization",
  school =       "TU Darmstadt / Fachgebiet Rechnersysteme",
  year =         "2011",
  month =        "23 " # sep,
  keywords =     "genetic algorithms, genetic programming",
  URL =          "http://tuprints.ulb.tu-darmstadt.de/2759/",
  URL =          "http://tuprints.ulb.tu-darmstadt.de/2759/1/rkibria-dissertation-final-korrigiert1.pdf",
  size =         "235 pages",
  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
                 satisfiability 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
                 optimisation 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 synthesised from the gathered data. For the
                 optimisation 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.",
  german_abstract = "Moderne, digitale Elektronik ist so komplex, dass
                 die Sicherstellung ihrer korrekten Funktion zur Zeit
                 der zeitaufwaendigste Teil der Entwicklung ist. Formale
                 Verifikation ermoeglicht es, funktionale Eigenschaften
                 solcher Systeme automatisch und vollstaendig zu
                 ueberpruefen, ohne dass der Entwickler zeitraubende und
                 fehleranfaellige Tests fuer jeden Einzelfall schreiben
                 muss. Die Eigenschaften werden in Instanzen des
                 Erfuellbarkeitsproblems der Aussagenlogik (SAT, von
                 engl. satisfiability) uebersetzt, die dann mit
                 Erfuellbarkeitspruefer-Software (auch SAT-Solver
                 genannt) geloest werden koennen. Die derzeit besten
                 SAT-Solver fuer industrielle Anwendungen basieren auf
                 verbesserten Versionen des DPLL-Algorithmus. DPLL ist
                 ein Suchalgorithmus, der von einer Vielzahl von
                 Heuristiken gesteuert wird. Die zur Loesung eines
                 SAT-Problems benoetigte Zeit ist stark abhaengig 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 fuer
                 die Heuristikparameter von SAT-Solvern praesentiert und
                 getestet. Das Verfahren basiert auf der Benutzung von
                 Optimierungsalgorithmen, mit denen versucht wird,
                 optimale Parameterkonfigurationen fuer Trainingsmengen
                 von SAT-Problemen anzunaehern. Ein Endergebnis wird
                 dann aus allen gesammelten Daten berechnet. Als
                 Optimierungsalgorithmen wurden zwei Unterarten von
                 Evolutionaeren 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, aehnlich gut sind wie die von Experten
                 ermittelten Standardparameter.",
  notes =        "Almost no mention of GP? Also known as
                 \cite{tuprints2759}

                 Referent: Prof. Dr.-Ing. Hans Eveking Korreferent:
                 Prof. Dr. Christoph Scholl",
}

Genetic Programming entries for Raihan H Kibria

Citations