Title

The Automated Design of Boolean Satisfiability Problem Solvers Employing Evolutionary Computing

Presenter Information

Marketa Illetskova

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

Start Date

4-11-2017 9:00 AM

End Date

4-11-2017 11:45 AM

This document is currently not available here.

Share

COinS
 
Apr 11th, 9:00 AM Apr 11th, 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.