SAT Solvers as Smart Search Engines

The bottom right corner is where the solution is found after many-many partial backtracks and associated partial unassignements:

What I want you to take away from this graph is the following: the solver iteratively tries to set a variable a value, calculates forward, and if it doesn’t work, it will partially backtrack, flip its value to its opposite, then descend again. To satisfy requirement (3) one must have a good set of intermediary variables in the CNF so the SAT solver can backtrack partially. If the solver has no intermediary variables to backtrack to, the solver will simply backtrack all the way to the beginning every time, thus becoming a really bad brute-force engine that incidentally tracks a dependency graph and is definitely non-optimised for the task at hand.

Source: www.msoos.org