The Satisfiability Problem: Implementing a Clause-Learning SAT Solver

Rosalind (Rosie) David ’20

Computer Science Major
Faculty Sponsor: Jill Zimmerman

Abstract

I researched the Boolean Satisfiability (SAT) Problem and the algorithm used to solve it. I first implemented a basic SAT Solver and then a more advanced Conflict-Driven Clause-Learning Solver. In this presentation I demonstrate how my solver learns new clauses and compared its performance to the basic version.