SAT Solver

The goal of this assignment is to implement a SAT solver. Your solver should be based on the DPLL algorithm, which was described in class on Monday, Oct 19 (see cs5959_lecture_09.pdf Download cs5959_lecture_09.pdf

The solver takes just one command line argument as input, which is the name of the input file that is is required to solver. The input file contains a propositional logic formula given in the simplified DIMACS formal (see http://www.satcompetition.org/2004/format-solvers2004.html Links to an external site.). Here is the description of the format from that webpage:

The input file format will be in a simplified version of the DIMACS format:

c
c start with comments
c
c 
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

• The file can start with comments, that is lines begining with the character c.
• Right after the comments, there is the line p cnf nbvar nbclauses indicating that the instance is in CNF format; nbvar is an upper bound on the largest index of a variable appearing in the file; nbclauses is the exact number of clauses contained in the file.
• Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line; it cannot contain the opposite literals i and -i simultaneously. Positive numbers denote the corresponding variables. Negative numbers denote the negations of the corresponding variables.

For the purpose of this assignment your SAT solver should check that both nbvar and nbclauses arguments are less than 65536.

Based on the outcome, the following should be printed to standard output and terminated by a newline:

• SATISFIABLE
• UNSATISFIABLE
• UNKNOWN
• ERROR

If the input formula is satisfiable, print SATISFIABLE. If it is unsatisfiable, print UNSATISFIABLE. If you cannot determine one way or the other, print UNKNOWN (note that I suspect that this case will never happen with your implementations). Finally, if the input file does not exist or is not properly formatted, report ERROR. Make sure to always return 0 as your exit code in all the above situations.

Non-functional requirements:

• The solver must be written in C that can be compiled by GCC and Clang on a Linux machine. The test machine is x86-64, but your code should also work when compiled to a 32-bit target, and should in general be as portable as possible.
• It is fine to use external libraries but please email me if you want to use something that is not standard.
• You are required to implement an extensive testing infrastructure for your solver.
• You should write a simple Makefile for building your solver. Remember: do not commit your solver binary to GitHub.
• You should write a README file with instructions on how to compile and run your solver, as well as your test scripts.

Submission:

• Create a GitHub organization based on your team name, and a GitHub repository within that organization. Add your team members to the created organization. Commit everything into the created repository.
• GitHub is regularly used by many companies you will potentially work for one day. Hence, it is great to learn how to use it properly. Leverage GitHub for the following tasks. Communicate but reports among team members (see github issues). Perform code reviews (create branches and pull requests). Make sure to write good commit messages (https://wiki.openstack.org/wiki/GitCommitMessages). Leverage release functionality to create a release.
• Follow some reasonable coding standards. Write a decent README.md file with instructions on how to build and run your solver.
• Include a Makefile so that when someone types "make" in your solver directory, the result is an executable. Name your solver as you wish.
• Do not add your executable to git!
• Try not to make your code or Makefile machine- or OS-specific; ideally it can be compiled on any Linux machine. If you are doing your development on a non-Linux machine, make sure to still build and test your code on a Linux machine.