Otherwise, we backtrack.

We try to assign the value one to x.

Again, so with F assigns the value one to x,

meaning that we remove all the clauses that contain x from the formula.

And we remove the x, negate it from all other clauses.

If the recursive call returns that the formula is satisfiable we

return that the initial formula is also satisfiable.

In the remaining case we just report that the formula is unsatisfiable.

Because no matter how we assign the value to x the resulting formula is

unsatisfiable.

Meaning that there is no way of assigning

the value to x to get a satisfiable formula.

So as we've seen in our toy example such a strategy arose to

find a satisfying assignment to conclude that the formula is unsatisfiable

without actually checking all possible 2 to the n assignments,

2 to the n candidate solutions.

I'm sorry.

So we do this as follows.

We build each solution piece by piece.

We try to extend each partial solution and

whenever we see that this is a deadend, that the current partial solution

cannot be extended to a valid solution we backtrack immediately.

We cut the correspondent branch of the tree and we do not extend it.

So this is a technique which is used in many, many modern and

state of the art SAT-solvers.

We did not prove any upper bound on the running time of the algorithm.

Well as you expect the running time of the algorithm might be exponential.

Because if we prove that it is polynomial,

we would show that could be solved in polynomial time.

This would resolve the p versus np question.

However, this technique is very useful in practice.

However, in practice SAT-solvers also use complicated heuristics for

simplifying formula and for selecting the next variable for

branching and then in selecting the next value for branching.

So in practice this idea improved by various heuristics

of simplifying a formula chosen as the next variable and chosen as value for

the next variable lead through very efficient algorithms that

are able to solve formulas with thousands of variables.

And other commonly used technique is called local search, and

this is a technique that we will consider in the next part.