The Automated Design of Boolean Satisfiability Problem Solvers Employing Evolutionary Computing
Department
Computer Science
Major
Computer Science
Research Advisor
Tauritz, Daniel R.
Advisor's Department
Computer Science
Funding Source
Missouri S&T Opportunities for Undergraduate Research Experiences (OURE)
Abstract
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.
Biography
Marketa Illetskova is a senior in Computer Science at Missouri University of Science and Technology and plans to complete her B.S. in Computer Science by May of 2017. She is an Undergraduate Research Assistant in S&T’s Natural Computation Laboratory. Furthermore, she is on the Missouri S&T Women’s Volleyball Team and the Love Your Melon Campus Crew.
Research Category
Sciences
Presentation Type
Poster Presentation
Document Type
Poster
Location
Upper Atrium/Hall
Presentation Date
11 Apr 2017, 9:00 am - 11:45 am
The Automated Design of Boolean Satisfiability Problem Solvers Employing Evolutionary Computing
Upper Atrium/Hall
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.
