Thrashing in Davis Putnam
Davis Putnam is liable to thrashing
- exploring exponentially too many branches
Look at this part of a clause set
Suppose we set variables in order a b c d Ö w x y z
When we set w either way, unit clauses force failure
But we will backtrack useless to x, then w, Ö
- taking 224 branches until we get back to a