# What is WalkSAT?

> WalkSAT is a randomized local search for satisfiability: start anywhere and flip variables in unsatisfied clauses. When it beats CDCL and when it cannot.

**WalkSAT**: WalkSAT is a randomized local search algorithm for satisfiability that repeatedly picks an unsatisfied clause and flips one of its variables, mixing greedy and random choices.

**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](https://cracked.guide/glossary/cdcl) solver can.

## Where it is taught

Knuth presents it as Algorithm W in [§7.2.2.2 part 3](https://cracked.guide/guide/knuth-w124-0), 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.

---

Source: https://cracked.guide/glossary/walksat
cracked.guide: A free, dated 145-week path to getting genuinely cracked at programming.