0:04

In which we are going to design exact algorithms for NP-complete problems.

Â Exact algorithms are also called sometimes intelligent exhaustive search.

Â As opposed to brute force search algorithm.

Â Which to find an optimal solution, just enumerates all

Â possible candidate solutions, and selects the best one.

Â Instead, we are going to find an optimal solution

Â 0:37

The first problem for

Â which we illustrate such an algorithm is 3-satisfiability problem.

Â Recall that the input of this problem consists of a CNF formula, and

Â it is 3-satisfiability each clause contains at most three literals.

Â So this formula is in three conjuctive normal form, in 3-CNF.

Â And our goal is to find out whether it is possible to assign Boolean values

Â to all the variables of this formula so, as to satisfy all the clauses.

Â Let me quickly show you once again, two for example.

Â So the first formula here is satisfiable, because we can set for example,

Â the value 1 to x, y, and z.

Â Or the value 1 to x, and the value 0 to y and z.

Â And the second formula is unsatisfiable.

Â We cannot set the values of the variables x,

Â y, and z to satisfy all these five clauses.

Â And I used brute force search algorithm for

Â these three satisfiability problem, does the following.

Â It just goes through all possible candidate solutions that is through

Â assignments, through all the variables of a formula and

Â checks whether any of them satisfies the input formula.

Â If n is the number of variables of an input formula F, then the running time

Â of this algorithm is proportional to the length of F times 2 to the n.

Â 2:03

Because we have 2 to the n assignments, and for all of them we need this kind of

Â formula to check whether all of the is fired or not.

Â In particular if your formula is unsatisfiable then your algorithm will be

Â forced to check all these assignments.

Â So it's running time will be 2 to the n.

Â So our goal for this module is to avoid going through all possible 2 to the n

Â assignments and still to check whether the input formula is satisfiable or not.

Â The first technique that we are going to use.

Â This is called backtracking.

Â So this is a well known technique which proceeds as follows.

Â You construct your solution piece by piece and

Â then at each step when you realize that your current solution cannot be extended.

Â Your current partial solution cannot be extended to a valid solution

Â you backtrack, you go back.

Â This idea is used in many situations,

Â from many combinatorial optimization problems and for many puzzles, and games.

Â So imagine, for example, that you are playing a game and you are staying in some

Â room, and you are in a maze, and you are looking for an exit from a maze.

Â And in the room that you are currently staying there are three doors leading out

Â of this room.

Â So you use one of these rooms and you enter another room for

Â which you see that there are no other doors.

Â So you are in a deadlock.

Â So you then go back, you backtrack, and you decide to use some other room.

Â So this is way of solving a combinatorial Problem,

Â it is called backtracking once again.

Â We will now show an example as usual how this technique named

Â backtracking is used to check the stability of Boolean formulas.

Â So consider the following formula, we need to find a satisfying assignment and

Â we don't know what to do so let's try to assign zero to h1.

Â What happens in this case is that

Â 4:26

We then proceed as follows.

Â Now let's try to assign the value 0 to x2.

Â What happens is that, well this clause is satisfied, x2 disappears from this

Â clause because it is falsified already from this clause and from this clause.

Â So what we get is x3 or x4, and then the negation of x3, and the negation of x4.

Â Then we try to assign the value 0 to x3.

Â What is left, so this clause disappears, x3 disappears from this clause.

Â So what is left is one clause containing x4, and

Â one clause containing the negation of x4.

Â We then try to assign the value to x4.

Â If we assign the value 0 to x4, then we falsify this clause.

Â So this clause disappears, and this clause becomes empty.

Â Meaning that there is no satisfied literal in this clause,

Â that there is no way to satisfy this clause anymore, right.

Â The same happens if we assign the value 1 to x4.

Â In this case, we satisfy this clause but at the same time, we falsify this clause.

Â Once again, this clause becomes empty,

Â which means that there is not way at this point to satisfy this clause.

Â 5:39

So at this point we backtrack farther.

Â We just realized that it was a wrong move to assign the value 0 to x3.

Â It leads to an unsatisfiable formula.

Â So we now try to assign the value 1 to x3.

Â So now we returned back here, and we are trying to assign the value 1 to x3.

Â But in this case we falsify this clause.

Â This clause becomes 17 which means that the roll this formula is unsatisfiable.

Â Which means that it was a wrong move to assign the value zero to x2, and

Â now we need to try to assign the value 1 to x2.

Â We do this, but we immediately falsify the following clause, right?

Â So in all other clauses we have x2 so all of them are satisfied but

Â what is left is an empty clause which cannot be satisfied.

Â So at this point we backtrack back to the initial formula and at this point we know

Â already that this we must assign the value one if we want to satisfy this formula.

Â So we do this and see again there is an empty clause.

Â So at this point we conclude that the initial formula is unsatisfiable.

Â 7:12

To our four input variables, right?

Â This is how the of the corresponding algorithm looks like.

Â So we first check whether F is empty or not.

Â So if F has no clauses and we have nothing to satisfy,

Â then we just return that the formula is satisfiable.

Â We then check if F is not empty, we check if F is an empty clause.

Â As we've discussed before, an empty clause means a clause which cannot be satisfied.

Â So all the literals in this clause have already been falsified.

Â In this case we return that the formula is unsatisfiable.

Â Otherwise we take some variable which is still present in the formula F.

Â So x is some unassigned variable of F.

Â And then we try two cases.

Â We first try to assign the value 0 to x.

Â So this notation means that we assign the value zero to x.

Â When assigning the value zero to x we remove all the clauses which contain

Â the negation effects.

Â All such clauses already satisfied, and

Â we remove all occurrences of x without negation from all other clauses.

Â Because x is all ready falsified.

Â If the formula turns out to be satisfiable,

Â we return immediately that the real formula is satisfied.

Â 8:31

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.

Â