Soft Computing Approaches to DPLL SAT Solver Optimization

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