COMP6902 Spring 2018 project

As you know, 25% of your grade in this course is based on a course project. You are welcome to work in groups of at most three (3) students; if you prefer to work by yourself, this is also fine. The main goal of the project is to get some experience using SAT solvers to solve other problems in NP by reducing them to SAT (SAT solvers are a class of heuristics-based programs for solving SAT; they are widely used in industry). More specifically, you will choose a problem in NP, reduce it to SAT, and see how well SAT solvers can handle it. For the latter, you will generate random instances of your problem of varying sizes, run SAT solvers on these instances, and plot solver's run time as a function of the instance size.

Here are the milestones of the project with more details.

1. Choose your group and your problem. You can pick any problem in NP from the class, from any of the books, from the web (e.g. from this list of NP-complete problems ); the book by Garey and Johnson "Computers and Intractability: A Guide to the Theory of NP-Completeness" has a list with hundreds of problems. As you are going to reduce not from SAT, but to SAT, it is better not to pick a problem about numbers (e.g., HamCycle is OK, but TSP will be a nuisance).
   Submit a text or pdf file with the definition of the problem and a list of your group member (for each person); also, in the comments on submission list the name of your problem and your group members (subsequent submissions will be one per group).
   Due: June 6. Weight: 5%

2. Find in the literature or design yourself a reduction from your problem to SAT (CNF-SAT, to be precise). You might want to do this as you are deciding on the problem. Note: nearly all reductions in the textbooks and papers are going to be from SAT, not to SAT.
   Submit the description of your reduction, referencing a paper in which you found it if you did not do it yourself. In particular, explain how to reconstruct a solution to your problem from a solution to a SAT insance (i.e., from a satisfying assignment).
   Due: June 11. Weight: 15%

3. Install some SAT solver from SAT competition website . Read about the SAT solver's input file format , download a sample test file test.cnf , run the solver on test.cnf to see what it outputs (give it an output file name). See here for an example solver user guide ; yours is likely to be similar, except for the name.
   Submit the name of the solver that you have installed and specs of the system on which it is installed (OS, etc), the formula encoded in test.cnf written as a CNF, and an explanation of the solver's output (was that formula satisfiable, and if so, what satisfying assignment the solver gave you, using names of the variables in the formula you just wrote above).
   Due: June 13. Weight: 10%

4. Describe how you plan to generate random instances of your problem. Say which distribution you will use, what are the parameters, and what is the regime of the parameters for which you are planning to generate instances (with the size of the instance n being a free parameter which you will vary). Try to ensure that your generator can produce both "yes" and "no" instances of your problem reasonably frequently (you can use "planted" method as discussed in June 13 lecture if needed).
   Submit a description of a generator of random instances of your problem.
   Due: Morning of June 20. Weight: 15%

5. Write programs implementing your reduction and your generator Your program REDUCTION should take as an input a name of a file containing an instance of your problem and produce a file with a CNF formula encoding of this instance in .cnf format. You can use any language: Python, Java, Matlab, etc. Check that your program works correctly by handcrafting "yes"- and "no"-instances and confirming that the SAT solver returns the result you expect.
   Your program GENERATOR should generate random instances of your problem using the method you described in the previous submission (for specified input parameters, most importantly size). For example, if you chose 3Col or Clique, this program should output random graphs.
   Submit your programs REDUCTION and GENERATOR, together with a README file explaining how to run your programs (including explanations of their input parameters), as well as a description of the format of the file in which you store your problem's random instances generated by the GENERATOR.
   Due: June 25. Weight: 10% 4

6. Evaluate the performance of the SAT solver on random instances of your problem .
   • First, for 20 (or more) values of n, generate 10 instances each of your problem using your GENERATOR program, run a SAT solver on all of them, and plot the average running time of the SAT solver on these instances as a function of n (the solvers usually output the time). For your specific problem, you will need to determine the range and the increment of n: e.g., it could be n=5 to n=100 in increments of 5, or it could be n=3 to n=23 in increments of 1, depending on how large the resulting CNF formulas are. Aim to have no more than 1000 variables in your largest CNF formula, and no fewer than 10 in the smallest.
   • Now, run additional experiments : e.g., try several different solvers, several heuristics choices for the same solver, etc. Try varying other parameters of your random instances (e.g., density of edges in a random graph or a distribution from which you are sampling), generate new sets of instances and plot the average time the solver takes as a function of that new parameter in addition to n...
   • You can get extra credit (5-10% of the project grade) by coming up with other interesting experiments to do in this project: check with me on our ideas.
     
   Submit a project report (5 pages). This should include the description of your problem, its reduction to SAT, and the random instance generator you submitted before (possibly rewritten), plus the results of your experiments with your analysis of these results (e.g., how did the running time increase with n? Which parameters made a difference, and how? How different solvers/heuristics compare to each other in performance on your instances? Was there a time difference between solving satisfiable vs. unsatisfiable instances? Was there a set of parameters generating hard instances?). Include a link to a repository such as github that has all your materials (except the actual solvers): your generator, reduction program, scripts to run experiments, and, most importantly, all instances used in your experiments (both of the original problem and converted to the solver format(s) ). Typeset your project report in LaTeX, and include a bibliography (I will provide a template).
   Due: July 6. Weight: 45%