Soft Computing Approaches to DPLL SAT Solver Optimization

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

@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",
• address = "Germany",
• month = "23 " # sep,
• keywords = "genetic algorithms, genetic programming, SBSE, Evolution Strategies, Fitness landscape, BCP",
• 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?

  2006 SAT Race benchmark. eg manol-pipe-c6n timeout 120s

  Seven parameters: VARDECAY, CLAUSEDECAY, NOFCONFLICTSINC, NOFCONFLICTSBASE, NOFLEARNTSINC, NOFLEARNTSDIVISOR, RANDOMVARFREQ. Conclusions p184

  p186 'Both the GA and the ES were capable of successfully navigating the search space of the problem and found values of VARDECAY'

  p154 'fitness landscapes are generally extremely noisy and show little structure'

  p189 'the EAs' [ES and GA] are not confused by the highly random effects'

  Also known as \cite{tuprints2759}

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

}

Genetic Programming entries for Raihan H Kibria

Citations