Provides API for high-performance SAT solver written in pure Python. Implementation of simple Davis-Putnam-Logemann-Loveland algorithm with intuitive search heuristics for the resolution steps - making it much faster than traditional DPLL.
This project was assigned by Dr. Licato as part of a class on Automated Reasoning (CIS 6930) at University of South Florida in Fall 2020. The class taught me about state-of-the-art SAT solvers, formulating other problems in SAT and 3SAT, and working in higher order logics (e.g., FOL). Practically, I learned methods used to parse, convert to CNF and evaluate complex boolean formulae. We were tasked to implement a DP-based SAT solver with optimizations made to improve over basic DP. In my approach, I implemented the popular DPLL, but, as just resorting to DPLL was considered too 'simple' of a solution, I further optimized the DPLL algorithm by computing metrics to select the 'best' literal for resolution. Other optimizations could be made that improve the selection of the branching literal (for DPLL step), like CDCL, but I found that merely adding strong heuristics to the resolution step drastically improved performance, with relative ease to implement.
Ultimately, we held a competition in the class to determine which group implemented the most efficient SAT solver. Groups were limited to 3 undergrads or 2 grads, with there being a good mix of groups and solo students -- I decided to complete the project on my own. Amazingly, my code turned out to be the fastest and the only one able to solve some problems with a large number of variables. For this, I was awarded extra credit points and some pride :). However, there were some edge cases, like where the input was supplied in DNF format with a large number of variables. In that case, my code would spend an endless amount of time converting to CNF. This can be alleviated by performing a Tseytin transformation (which a couple groups actually did).
The parsing and conversion code was completed through incremental assignments leading up to the project. Parsing is performed on boolean statements formatted like S-expressions. So, if you wish to use this code, you will have to pass your inputs in that format (shown in the P1_grader.py script provided by Dr. Licato). The DPLL code itself represents the expression as a list of sets of integers, where every set is a clause in the CNF formula. This makes it very easy to implement the rules using Python set functionality and itertools for high performance.