WalkSAT

In computer science, GSAT and WalkSAT are local search algorithms to solve Boolean satisfiability problems. In computer science, GSAT and WalkSAT are local search algorithms to solve Boolean satisfiability problems. Both algorithms work on formulae in Boolean logic that are in, or have been converted into, conjunctive normal form. They start by assigning a random value to each variable in the formula. If the assignment satisfies all clauses, the algorithm terminates, returning the assignment. Otherwise, a variable is flipped and the above is then repeated until all the clauses are satisfied. WalkSAT and GSAT differ in the methods used to select which variable to flip.