The Boolean satisfiability problem (SAT) has many applications in electronic design automation (EDA) as well as theoretical computer science. Most SAT solvers for EDA problems use the DPLL algorithm and conflict analysis dependent decision heuristics. When the search starts, the heuristics have little or no information about the structure of the CNF. In this work, an algorithm for initializing dynamic decision heuristics is evolved using genetic programming. The open-source SAT solver MINISAT v1.12 is used. Using the best algorithm evolved, an advantage was found for solving unsatisfiable EDA SAT problems. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Kibria, R. H., & Li, Y. (2006). Optimizing the initialization of dynamic decision heuristics in DPLL SAT solvers using genetic programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3905 LNCS, pp. 331–340). https://doi.org/10.1007/11729976_30
Mendeley helps you to discover research relevant for your work.