The purpose of this assignment is to evaluate experimentally a heuristic algorithm of your invention for solving NP-complete Boolean satisfiability problems.

You should select a state-of-the-art algorithm as a basis for comparison, for example the Walksat method of Selman et al.  Your experiments should compare carefully the performance of your suggested new method, and the basis method.  You should confirm that the performance of the basis method is the same as its performance reported in published papers.

It is recommended that you implement both methods in standard C for efficiency and portability, but you may choose a different programming language.  Performance should be measured in a way that does not depend on the particular compiler or CPU that you use, and also in clock time using the same computing environment for both algorithms.  See the Ten Challenges paper cited below for more guidelines on performance measurement.  Performance includes speed and the percentage of satisfiable instances solved; you may decide that other metrics are important also.

The new algorithm that you design, implement, and test should be well-motivated.  You may choose to modify an existing state-of-the-art method, such as Walksat, or you may invent a more fundamentally new algorithm.  In either case, your algorithm should be motivated by lessons from recent research or ideas that have worked well in analogous fields.  New research should always build on good recent other research in one way or another.  Also, since life is short, you should only do the work of implementing and testing an idea that you have motivated and analyzed as much as possible in advance.  The motivation for the design of your algorithm should be explained clearly, concisely, and concretely in your report.

Pay attention to low-level efficiency in your code, but do not make this a primary focus of the project.  One specific guideline: be sure to use a high-quality but fast pseudo-random number generator, and economize if possible on how often the generator is called.  You should reuse code and test cases from SATLIB.

In general, it is very difficult to show convincingly that one algorithm is systematically faster than another, especially when the algorithms both require exponential time, and running times have very high variance.  Perhaps the most important aspect of the current project is to design, carry out, and report on credible experiments.

The following papers, all co-authored by Bart Selman, will provide inspiration for designing your algorithm and your experiments.

• Evidence for Invariants in Local Search shows how to choose the best version of a randomized algorithm in a principled way.
• Ten Challenges in Propositional Reasoning and Search outlines possible directions for exploration, and suggests which are most important.
• Hard and Easy Distributions of SAT Problems shows that the most difficult 3-SAT problems are ones where the number of clauses is approximately 4.3 times the number of variables.
• Boosting Combinatorial Search Through Randomization shows how to accelerate a deterministic backtracking search algorithm by adding randomization.
• Exploiting Variable Dependency in Local Search shows how to add constraint propagation to a randomized local search method.

All your work should be described in a well-written report that follows all the CSE 250A guidelines.  As an appendix to your report, you should attach a printout of your software, which should be adequately commented and documented.

The authors of one or more of the best reports submitted will be asked to revise their report(s) for distribution to all CSE 250A students.  These authors will receive extra credit of 25% of the total credit available for the project, and they will be encouraged to submit papers to an appropriate workshop or conference.