ECE 479: Formal Verification

DPLL

Example Continued

Will take multiple classes to complete.

Clauses POS
$C_1$ $(a'+b+c)$
$C_2$ $(a+c+d)$
$C_3$ $(a+c+d')$
$C_4$ $(a+c'+d)$
$C_5$ $(a+c'+d')$
$C_6$ $(b'+c'+d)$
$C_7$ $(a'+b+c)$
$C_8$ $(a'+b'+c)$

First, we make a decision on one of the varibles (in this case, a) and assign it the value of 0. We then see if that makes any of the clauses true.

In the current case, we see that it makes $C_1$, $C_7$, and $C_8$.

a=0 : $C_1$,$C_7$,$C_8$ $C_1:(a'+b+c)=(0'+b+c)=(1+b+c)=1$

So, now we remember which clauses get satisfied for each decision. The goal is to keep making decisions and then it sees how many clauses are satisfied. If all clauses are satisfied, then the whole function is satisfied.

So now, lets set $b$ to $0$.

a=0,b=0 : $C_1$,$C_6$,$C_7$,$C_8$
This adds $C_6$.

a=0,b=0,c=0 : $C_1$,$C_4$,$C_5$,$C_6$,$C_7$,$C_8$
This adds $C_4$ and $C_5$.

Diagram

To draw this process, follow a tree-like structure

-- Starting Here --

Let's now look at what we have left over:

$C_2 = (a+c+d) = (0+0+d)$

Because this only has one varible left, it is called a unit clause.
Unit clauses usually lead to implications.

What does $d$ need to be to make the function satisfied?
$d = 1$

Now lets look at $C_3$:
$C_3 = (a+c+d') = (0+0+d')$

This is now a unit clause which implies that $d = 0$

Notice how under this branch, $d$ needs to be both $0$ and $1$? This is called a conflict.

This means that one of the other variables needs to be changes. In other words, this branch doesn't lead to satisfiablility, and we can label it so.

Labeled Branch

We now have to backtrack by looking for another branch that can lead to satisfiablility.

Let's make $c = 1$:
a=0,b=0,c=1 : $C_1$,$C_2$,$C_3$,$C_6$,$C_7$,$C_8$
This adds $C_2$ and $C_3$ So do we get any unit clauses?
Yes! $C_4$ and $C_5$

$C_4 = (a+c'+d) = (0+0+d)$ which implies $d = 1$
$C_5 = (a+c'+d') = (0+0+d')$ which implies $d = 0$
These conflict, so we have to backtrack by setting $b = 1$ and $c = 0$.

Notice the process of making decisions and finding unit clauses until there is either a fully satisfiable path or, if all decisions lead to conflicts, it is unsatisfiable.

a=0, b=1 : $C_1$,$C_7$,$C_8$ No additional clauses are satisfied.

a=0, b=1, c=0 : $C_1$,$C_4$,$C_5$,$C_6$,$C_7$,$C_8$ This added $C_4$, $C_5$, and $C_6$. Do we have any unit clauses? Yes! $C_2$ and $C_3$

$C_2 = (a+c+d) = (0+0+d)$ implies $d = 1$ $C_3 = (a+c+d') = (0+0+d')$ implies $d = 0$ These conflict, so we have to backtrack by setting $c = 1$.

a=0, b=1, c=1 : $C_1$,$C_2$,$C_2$,$C_7$,$C_8$ This added $C_2$ and $C_3$. Do we have any unit clauses? Yes! $C_4$ and $C_5$

$C_2 = (a+c'+d) = (0+0+d)$ implies $d = 1$ $C_3 = (a+c'+d') = (0+0+d')$ implies $d = 0$ These conflict, so we have to backtrack by setting $a = 1$, $b = 0$, and $c = 0$.

a=1 : $C_2$, $C_3$, $C_4$, $C_5$
This adds $C_2$, $C_3$, $C_4$, and $C_5$.

a=1, b=0 : $C_2$, $C_3$, $C_4$, $C_5$, $C_6$, $C_8$
This adds $C_6$ and $C_8$.
Do we have any unit clauses? Yes! $C_1$ and $C_7$

$C_1 = (a'+b+c) = (0+0+c)$ implies $c = 1$
$C_7 = (a'+b+c') = (0+0+c')$ implies $c = 0$
These conflict, so we have to backtrack by setting $b = 1$.

a=1, b=1 : $C_1$, $C_2$, $C_3$, $C_4$, $C5$, $C$, $C_7$ This adds $C_1$ and $C_7$. Do we have any unit clauses? Yes $C_6$ and $C_8$.

$C_6 = (b'+c'+d)$
$C_8 = (a'+b'+d) = (0+0+c)$ implies $c = 1$
Now we propagate $c = 1$ into $C_6$.
$C_6 = (b'+c'+d) = (0+0+d)$ implies $d = 1$

Now that we have all clauses satisfied, we can conclude that the function is satisfiable.
Thus, we can conclude the satisfying assignment is a=1, b=1, c=1, d=1.