In this assignment you will implement a solver for the Satisfiability (SAT) problem. In particular, you will implement the Davis–Putnam–Logemann–Loveland (DPLL) algorithm. This algorithm takes as input a logical statement in CNF format and outputs a assignment of True or False to each propositional symbol.

Files

Download the code template here. You should write your code between the comments marked "Begin/End your code". You may add extra functions as you like.

Download small instances here and corresponding satisfying assignments here. Note that there may be more than one satisfying for each instance, so if you do not find the same assignment it does not necessarily mean your solution is wrong.

The assignments file has one assignment per line. Each assignment consists of a series of whitespace-separated symbol assignments, where "a" indicates the assignment "a = True" and "-a" indicates "a = False". The instance file is a list of instances, separated by double newlines. Each instance is a list of clauses, separated by newlines. The clause "a -b c" corresponds to the propositional sentence "a OR (not b) OR c". The i-th instance in the input file corresponds to the i-th assignment in the assignment file.

Download big instances here. When you are ready, run your code to generate solutions for these instances. Your code should take less than five minutes to run on this example. Include the output in your submission named big_assignments.txt.

Challenge problem (extra credit, +10 points): Download the bonus instances here (0.2GB gzipped file). Develop the fastest SAT solver you can and run it on these instances. You may use any algorithm, programming language or compute infrastructure that you like. Submit your bonus assignments as a gzipped file called bonus_assignments.txt.gz in your submission directory.

We will give extra credit as follows: +3 points for a new algorithm. Let X be the number of instances solved by my basic DPLL solution; let Y be the maximum number of instances anyone solves, and suppose you solve Z instances. You will get 7 * (Z - X) / (Y - X) extra credit points. (No one should be able to solve all the bonus instances. The sizes grow exponentially, so the best solutions will likely solve only a couple more instances than a basic solution.)

Guidelines

Please use Python 3 for this assignment.

100 points total, worth 10% of the course grade. Turn in on CourSys. Submit a compressed directory (.zip or .tar.gz) with (1) your code in one file name "a2.py" and (2) your solutions to the big instances, named big_assignments.txt.

Grading: Your solution will be evaluated on accuracy and clarity. Solutions that are hard to understand will be given a maximum of 50/100 points. Please use a logical structure, use informative variable names, and document your code thoroughly so that your solution is understandable. You must implement the DPLL algorithm; solutions using other algorithms will be given partial credit, even if they give a correct assignment. (Bonus solution may be any algorithm.)

You are encouraged to work in a group. Feel free to discuss solution strategies and check each other’s work. However, you must write all the text and code you submit on your own. Joint submissions are not allowed, nor is copying someone else's text or code. Plagiarism is not okay, and will be taken very seriously. If you’re not sure whether something is okay, please ask.

If you are having trouble, please take advantage of office hours and the discussion forum. If you see a question from another student on the discussion forum that you think you know the answer to, please respond. (Do your best to lead your fellow student to a solution, rather than simply giving the solution directly.)