Glossary
What is WalkSAT?
WalkSAT (Selman, Kautz and Cohen, 1994) looks for a satisfying assignment by wandering: start from a random assignment, pick a clause that is false, and flip one of its variables, sometimes the one that breaks the fewest other clauses and sometimes one at random. Repeat until everything is satisfied or you give up.
Strengths and limits
On large random satisfiable instances it can find a solution far faster than a systematic solver. But it is incomplete: if the formula is unsatisfiable it will just run forever, so it can never prove there is no solution. A CDCL solver can.
Where it is taught
Knuth presents it as Algorithm W in §7.2.2.2 part 3, right after Papadimitriou's simpler random walk, with restarts and the "reluctant doubling" schedule for when to start over.
Questions
What does the noise parameter do?
It is the probability of a random flip instead of a greedy one. Too low and the search gets stuck; too high and it wanders aimlessly.