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.