WalkSAT

From Wikipedia, the free encyclopedia

GSAT and WalkSat are local search algorithms to solve boolean satisfiability problems.

Both algorithms work on formulae that are in (or have been converted into) conjunctive normal form. They start by assigning random values to all the variables. If the assignment satisfies all clauses, the algorithm stops and returns the assignment. Otherwise, the value of a variable is changed, and the process is repeated. The variable to change is the one that minimizes the number of unsatisfied clauses in the new assignment in GSAT. If no assignment satisfying all clauses has been found after a fixed number of iterations, the algorithm starts again with a new random assignment. The algorithm terminates either when a model of the formula has been found or when the number of restarts exceeds a fixed number (for example, ten).

WalkSAT differs from GSAT for the addition of random noise. In order to avoid being entraped into assignments that are local maxima with respect to the number of satisfied clauses, the move from one model to another is sometimes done randomly rather than choosing the literal that maximizes the number of satisfied clauses.

Many versions of GSAT and WalkSat exist. WalkSAT has been proven particularly useful in solving satisfiability problems produced by conversion from automated planning problems (the approach to planning that consists in converting planning problems into Boolean satisfiability problems is called satplan.)

MaxWalkSat is a variant of WalkSat designed to solve the weighted satisfiability problem, in which each clause has associated with a weight, and the goal is to find an assignment - which may or may not satisfy the entire formula - that maximizes the total weight of the clauses satisfied by that assignment.

[edit] References

Bart Selman, Henry Kautz, and Bram Cohen. "Local Search Strategies for Satisfiability Testing." Final version appears in Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, October 11-13, 1993. David S. Johnson and Michael A. Trick, ed. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, AMS, 1996.

H. A. Kautz and B. Selman (1996). Pushing the envelope: planning, propositional logic, and stochastic search. In Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI'96), pages 1194-1201.

B. Selman and H. A. Kautz (1993). Domain-Independent Extension to GSAT: Solving Large Structured Satisfiability Problems. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI'93), pages 290-295.

B. Selman, H. Levesque, and D. Mitchell (1992). A new method for solving hard satisfiability problems. In Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI'92), pages 440-446.