Lesson 1

Despite the hardness of the satisfiability problem, modern SAT solvers are very efficient in practice: they solve many formulas even with millions of variables. They are based on heuristic methods — methods that work well in practice but have no proven guarantees. The two main heuristics of most modern SAT solvers are:

• Backtracking.  We construct a satisfying assignment step by step: fix the value of a variable and continue recursively; if no solution is found, backtrack and fix the opposite value.


• Local search.  Start from some assignment and try to improve it locally to make it satisfying.