Programming Assignment 1: Build a SAT Solver

Overview: Implement either DPLL (referred to as “DP” in the textbook) or Walksat. Evaluate its scaling (run time) on randomly generated 3CNF formulas. Due by Blackboard turn-in by 11:59pm Tuesday Oct 26.

New Implement Hints, Posted 10/13

• It is easy to write a basic (but slow) version of either DPLL or Walksat. It is considerably harder to write an efficient version of DPLL than an efficient version of Walksat. You should complete the assignment with a simple implementation before trying to write an efficient implementation, so that you are sure to have something completed on time!
• This paper describes how to write an efficient version of DPLL:
  • Chaff: Engineering an Efficient SAT Solver by M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, 39th Design Automation Conference (DAC 2001), Las Vegas, June 2001.
• The reserved paper "Satisfiability Solvers" by Gomes et al. presents the best version of the Walksat algorithm (page 109). In order to implement it efficiently, your program needs to (1) pick an unsatisfied clause at random and (2) determine how many clauses that are currently satisfied would become unsatisfied if a particular variable were flipped. Here are ways to accomplish this:
  1. Maintain a list U of (pointers to the) clauses that are currently unsatisfied. Initialize this list after the initial random truth assignment is chosen. Choose a random element from the list by choosing a random number i from the range[1 .. length of U], and then returning element U[i].
  2. For each literal (positive and negative), maintain a list of (pointers to) the clauses that contain that literal, and store these lists in an array C indexed by the literal (a proposition or the negation of a proposition). Thus C is an array of lists of clauses, and C[L] is a list of clauses, where L is a literal. (Note that if your programming language does not allow array indexes to be negative numbers, then you will have to fudge the indexes to make them all positive; instead of directly indexing by L, index by L+NumberOfPropositions.) The function Breaks(P), the number of clauses that are currently true that would become false if P were flipped, can then be computed as follows:

     count = 0;
     L = (S[P] > 0) ? P : -P;
     for each clause c in C[L]
         if L is the only true literal in c then
             count ++;
     return count

     If P is indeed chosen to flipped to a new value, then where L is the original value of P, step through the clauses in C[L] and add any that have become false to U, and step through the clauses in C[-L] and remove any that used to be false and after the flip are true from U.
     

Details:

• Work in groups of two. People who do not have a partner by Oct 6 will be matched in class.
• You may use any programming language.
• You may make use of standard libraries for managing data structures.
• You may not copy code from an existing implementation of DPLL or Walksat.
• You may develop your program on any platform (Linux, Windows, or Mac), but it should be possible to execute the final version on Linux.
• Your should be able to invoke your program from the command line as follows.

  dpll LIMIT INFILE OUTFILE

  where

  LIMIT is an integer specifying the maximum number of recursive calls of DPLL that are to be permitted;
  INFILE is a CNF formula in DIMACS format (see below)
  OUTFILE is a satisfying assignment, also in DIMACS format, if one exists

  or

  walksat LIMIT INFILE OUTFILE

  where

  LIMIT is an integer specifying the maximum of number of flips that are to be permitted, and
  INFILE and OUTFILE are as above.

• The DIMACS for problem instances is as follows.
1. Zero or more comment lines, each beginning with the letter c (lowercase).
2. A line in the format:

   p cnf NUMBER_VARIABLE NUMBER_CLAUSES

3. A line for each clause. Literals are represented by integers, which can be thought of as the indexes on a set of propositional letters. Each clause is terminated with a 0 before the end of line. For example, the clause [X3 v ~X5 v X17] would be represented as:

   3 -5 17 0

For example, the formula (~X1 v X3) & (X1 v ~X2) & (X2 v X1) & (~X3 ~X2 v X1) would be:

c This is a test example
p cnf 3 4
-1 3 0
1 -2 0
2 1 0
3 -2 1 0

• A solution file should begin with a line containing the single word SAT, UNSAT, or TIMEOUT (with no spaces on either side). The word TIMEOUT means your program stopped because it reached the limit on the number of recursive calls or flips. If the word is SAT, then a second line specifies a solution in the form of a sequence of positive and negative integers in increasing absolute value order up to the number of variables, followed by a zero. For example, a solution to a 4 variable problem with X1=true, X2=false, X3=true, X4=false would be:

SAT
1 -2 3 -4 0

• If your program is written in an interpreted language such as Python, then your dpll or walksat program should be a shell script that invokes the interpreter on your code. Your code may be in the shell file or in a separate file it loads.
• Your program may print any useful information about its operation to standard out. This should at least include a line that contains the single word SAT, UNSAT, or TIMEOUT (with no spaces on either side).
• You can time how long it takes your program to solve a problem by the Linux “time” command. For example:

  time dpll 100000 f100.cnf f100.sol

• You should test your program on the formulas in the following zip file. The README.txt file describes how the names of the files indicates the problem size (number of Boolean variables), whether the problem is satisfiable or not, and the problem instance index (there are 10 SAT problems and 10 UNSAT problems for each size upto 320 variables, and then satisfiable instances only for larger sizes). You should pick a value of LIMIT large enough so that your program will not time out before at least 5 minutes has elapsed. Start with the smallest problem and run on larger and larger instances until you reach problems that cannot be solved within 5 minutes. If you implement DPLL, compute the average solution time for the 10 SAT instances and the 10 UNSAT instances for each problem size separately. If you implement Walksat, only test your program on the SAT instances. The zip file also contains programs that can be used to verify that your program found a correct solution to the satisfiable problems. Be sure to check that your program is working correctly. Note that you will want to write a bash shell script to run your experiments, otherwise you will be sitting at the terminal for hours!

  SatSolverAssignFiles.tar.gz

• Include in your report a table where each line specifies the problem size, whether the problems are SAT or UNSAT, and the average elapsed real running time in seconds for the 10 instances. Plot the results with the number of variables on the X axis, and the base 10 log of the running time on the Y axis. If you implement DPLL, create separate plots for the SAT and UNSAT instances. For example, your table might look like this:

Variables	Answer	Average Time (Seconds)
10	SAT	0.00001
10	UNSAT	0.00002
20	SAT	0.00002
20	UNSAT	0.00003
...	...	...
80	SAT	250.2400
80	UNSAT	TIMEOUT on instances 3, 6, 9

• Write a report on your work which describes the high level design of your program, the data structures you used, and how your program scales with increasing problem size, as described above. Say kind of scaling is shown by your plots (e.g., linear, quadratic, exponential), and explain how that kind of scaling is revealed by a log-normal plot. Include a discussion of techniques you used (if any) to make your code efficient.
• Grading will be 40% for program correctness, 20% for proper testing, 20% for the report, and 10% for efficiency. Note that you will turn in your work using Blackboard, not by emailing to me.