The Automated Design of Boolean Satisfiability Problem Solvers Employing Evolutionary Computing

Many important real-world problems, from computer chip layout to cryptography, can be modeled as Boolean Satisfiability Problem (SAT) classes with unique structures. Customizing solver components to target a specific class using evolutionary computing can lead to an improvement in the performance of the solver on the specific class. The goal of this project is to optimize such an automated design system for SAT solvers to satisfy expectations of current SAT solving systems and to possibly improve the quality of produced solvers. In particular, it focuses on (i) selecting new datasets to evaluate the performance of evolved solvers on different SAT problem classes; (ii) adding CPU time to objectives on which the fitness of each solver is based; (iii) changing the main fitness objective for single objective evolutionary algorithm to CPU time; and (iv) changing parent selection to epsilon-lexicase selection