WSAT

The GSAT family of algorithms use hill-climbing in order to solve SAT problems. Given a set of propositional clauses, such as (x or y or z), we start by assigning a truth value to every variable. At every iteration we then pick a variable and "flip" its value from true to false or vice versa.

With good heuristics for selecting the variable to be flipped these algorithms work amazingly well (Selman & Kautz, 93), part of the reason for the success being that the simplicity of the algorithm means that we can achieve many flips per second. The sheer speed of the iterations often being sufficient to overcome their lack of deep insight into the problem structure.

WSAT or walksat is a particularly good strategy in the GSAT family. The idea is to do a "random walk on the unsatisfied clauses". For theories with at most 2 literals per clause (2SAT) it is known that simply picking an unsatisfied clause at random, and then flipping a random literal in that clause is sufficient to find a solution (if one exists) in polytime (Papadimitriou, 91).

With the addition of heuristics for selecting the literal to be flipped then the algorithm also does very well for more general SAT theories (Selman, Kautz & Cohen, 94).

CIRL

At CIRL we have implemented a version of Lifted WSAT that allows the input to be in the form of quantified clauses (QPROP).

Older work looked into the effect of restarts on the performance of WSAT, and also how its performance scaled with problem size.

Pointers

Tuning Local Search for Satisfiability Testing
Study of effects of differing frequency of restarts on the performance of WSAT, and the scaling of performance with problem size. AAAI 1996. Postscript.

Parent areas:
Nonsystematic Methods

Applications:
Lifted WSAT

References

C. H. Papadimitriou, "On selecting a satisfying truth assignment." Proceedings of IEEE symposium on Foundations of Computer Science, 1991.

Bart Selman and Henry A. Kautz, "An Empirical Study of Greedy Local Search for Satisfiability Testing" Proc. IJCAI in 1993.

Bart Selman and Henry A. Kautz and Bram Cohen, "Noise Strategies for Improving Local Search", Proc. AAAI in 1994.


Back to the CIRL Overview Page.