Overview / Usage

The boolean satisfiability problem (SAT) is the first problem to be proven NP-complete. In the last decade, the usefulness of SAT has increased so much that much effort has been put into improving technology that can find solutions to these satisfiability problems (SAT solvers). SAT solvers can be split into two main categories: Complete and incomplete. Complete SAT solvers are guaranteed to find a satisfying assignment if one exists (Given enough time) while incomplete solvers are not. Many different kinds of problems can be encoded as a propositional logic formula and then fed into a SAT solver to find a solution to the problem. The areas of application include, but are not limited to, formal software verification, scheduling tasks, automated mathematical proofs and hardware and software design.

This project is aimed at making progress in the development of an incomplete SAT solver that makes use of concepts from artificial intelligence and certain heuristics to improve solving time. Some solvers of interest are WalkSAT, GSAT and FlipGA. Research on improving FlipGA and developing crossover operators that work better in the context of SAT has been done by Lardeux et al. and the GASAT algorithm was born. This algorithm makes use of a genetic algorithm and three proposed crossover operators. Furthermore, a local search algorithm, specifically tabu search, is used to guide the search. This project includes implementing the GASAT algorithm and running experiments with several different configurations. This is done via a randomized grid search to optimise the parameters for specific problems and then trying to find a general trend. We hope to make a breakthrough in applying evolutionary algorithms to SAT and contribute to the scientific community.

We are a team of 5 undergraduate students at the University of Pretoria and are doing this project as part of our final year project for an undergraduate computer science degree. Our leaders in the project are two post-doctoral researchers in the field of formal software verification and who wish to use this project to further their research in bounded model checking.