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 a random value to each variable. If the assignment satisfies all clauses, the algorithm terminates, returning the assignment. Otherwise, the value of exactly one variable is changed, and the process is repeated. WalkSAT and GSAT differ in the methods used to select this one variable.

GSAT makes the change which minimizes the number of unsatisfied clauses in the new assignment. If no satisfying assignment has been found after a fixed number of iterations, the algorithm restarts with a new random assignment. The algorithm terminates either when a satisfying assignment has been found, or when the number of restarts exceeds some fixed maximum.

WalkSAT adds random noise to the GSAT method, potentially helping it to avoid becoming "trapped" in assignments that are local maxima with respect to the number of satisfied clauses. Specifically, instead of consistently choosing the minimizing assignment, WalkSAT occasionally alters a randomly-chosen variable.

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 converts 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—one 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.

[edit] External links