MAX-SAT Project On the Relative Merits of Simple Local Search Methods This page is devoted to a MAX-SAT project, in which we evaluate the performance of conceptually simple algorithmic techniques for solving the MAX-SAT problem. All the techniques under consideration are based on local search (LS), and include oblivious and non-oblivious local search, tabu search, simulated annealing, their combinations, and maxwalksat.

Source for LS Algorithms

For this project, we developed a library of local search algorithms that can be found here: Source code distribution (Compiles under Mac OS X with g++ 4.0.1).

Feel free to download, copy, modify, and redistribute the code at your own will. The code does not come with any guarantees. Use it at your own risk.

If you find a bug, or if you find the code useful, I would love to hear from you (my contact information).

Source for Formula Generator

We used the following code to generate weighted k-CNF formulas with the number of clauses around the conjenctured phase transition threshold: Source code distribution (Compiles under Mac OS X with gcc 4.0.1)

Experiments

We performed many experiments; however, not all of them made it to the final version of a companion paper, because of space limitations.

Rough overview of additional experiments can be found here.

SAT 2010 Conference

Presentation (2.8 mb)

People Involved

Denis Pankratov, University of Chicago

Allan Borodin, University of Toronto