[music] So here we are in Lecture 4.2. We're going to continue working on
computational boolean algebra, and we're going to continue our discussion of
boolean satisfiability, or SAT. In the last lecture, we introduced
Conjunctive Normal Form, CNF as a, as a representation scheme.
And now we're going to show how does one actually start with a set of clauses in a
CNF style and answer the question as to whether it's satisfiable or not.
And it turns out, we shouldn't be surprised.
It's another recursive sort of computation.
But more importantly, there's a very powerful and important iterative sort of
computation that says, more or less, let's just assume that a particular variable has
a value, and let's just see what happens. When you have a boolean equation with
many, many variables and many, many, many clauses, it turns out you can get most of
the work done with this simple procedure. And this is called the boolean constraint
propagation, or BCP. And what we're going to talk about next is
how BCP works. So in the last lecture, we said that
boolean satisfiability had two big parts. It had a decision part where we more or
less arbitrarily decide to set some values to variables.
And we go simplify the CNF form and we see what happens.
Can we satisfy it or are we conflicted or what happens?
The problem is that's only going to go so far.
And it turns out that, because some variables have values, you can deduce that
other variables must have values. And it turns out that in a really, really
big instance of a CNF for a really big boolean function, there is an enormous
amount of this deduction that is possible. In fact, this is where really all of the
deep work happens in boolean satisfiability.
And this means stuff has a name. It's called boolean constraint
propagation. So, given a set of fixed variable
assignments, what else can you deduce about the necessary assignments to other
variables? Well, you can do that by propagating
constraints. Now, there is a very famous strategy for
this, called the Unit Clause Rule, and gosh, this is like 50 years old.
A clause is said to be unit if it has exactly one unassigned literal, right?
And so a unit clause has exactly one way that you can satisfy it and so what that
means is that, you have to pick the polarity that makes the clause 1.
You don't have a choice, you don't get to arbitrarily pick the polarity of that
literal and that choice is called an implication.
So here is a little boolean function phi, a plus c, b plus c, not a plus not b plus
not c and let us assume that we have decided to make these choices.
So a is a 1 and b is a 1. So what do we know?
In the first clause, a is 1 and so that clause is satisfied.
I can stop worrying about it. And in the second clause, b is 1.
That clause is satisfied, I can also stop worrying about it.
But in the third clause, the a term becomes a 0.
The b term becomes a 0. And oh look.
What has happened? This clause has become unit.
And it's unit, because there's exactly one unassigned literal, which in this case is
c bar. So what do I know, I know that c must be
0. It has to be a zero, because the only way
that I can satisfy this clause is if c is a 0.
And then that clause becomes a 1. If I really want to satisfy this boolean
function, because of the decisions I have made for a and b, I am, I have deduced
that c, by implication, must be a 0. It turns out that in gigantic CNFs for
real industrial circuits, you get to deduce a zillion of these unit clauses.
You get to deduce a zillion variable values, its really what drives the sat
process forward in any real SAT engine. Let's go take a look at sort of how that
might work. So I have got a little example here, and
this is an example from this paper which is worth checking out by my friends John
Marques-Silva and Karen Sakallah. Done when they were both at the University
of Michigan. Marques is now in Dublin.
So, phi, my little boolean function has 9 clauses.
Omega 1, omega 2, 3, 4, 5, 6, 7, 8, 9. 9 clauses.
And omega 1, not x1 plus x2. Omega 2, not x1 plus x3 plus x9.
Omega 3, not x2 plus not x3 plus x4, omega 4, not x4 plus x5 plus x10, omega 5, not
x4 plus x6 plus x11, omega 6, not x5 plus not x6, omega 7, x1 plus x7 plus not x12,
omega 8, x1 plus x8. Omega 9 not x7 plus not x8 plus not x13.
Gosh. It's not easy to tell if these things are
satisfiable, is it? And imagine if it's hard for a, a function
that has 13 variables imagine what it's like for a function with 13,000 variables.
This is why we need an algorithmic, a computational approach to asking and
solving these problems. So how do you start?
Let's start by just, somewhat arbitrarily, doing a partial assignment x9, 10, 11 and
x12 and 13 are signed values shown here, x9, 10, 11 are 0, x12 and 1 are 13.
We're going to go look at the clauses in the function, and we're going to just
simplify them by inserting those values. And so here we go.
I've inserted values for 9, 10, 11, 12 and 13.
Okay, so what happens and the answer is that, not much happens.
I cannot satisfy any of these clauses, there are conflict in these clauses.
There are, you know, basically there's no unit clauses here which is sort of the
interesting part of this exercise. I can't really do anything so pretty much
I can say now what, and the answer is, I guess I'm going to have to go decide
arbitrarily to set some more variable values because nothing interesting
happened here. I've really haven't you know, haven't I
haven't been able to conclude anything. Alright so, What are we going to do next?
We're going to choose to assign a variable to a value and we're just going to choose
to assign x1 to be a 1. So, I'm going to go back to my boolean
equation here and I've, I've got all the previous assignments from the last round
greyed out and I'm going to assign these values.
And what happens is, in clause omega 1 and omega 2, the x1 term becomes a 0.
And in clause omega 7 and omega 8, the x1 term becomes a 1.
Oh, this is good, actually. This is helpful, because, in these first
two clauses, and I'm going to circle this here, in these first two clauses things
have become unit in clause omega 1 x2 stands alone, its the only variable
without a value. I know what it has to be, its got to be 1
and in x3, I'm sorry in omega 2, x3 is the only variable without a value everything
else this is 0 and so I know x3 is got to be a 1.
So, my unit clause rule tells me, hey I have figured something out.
X2s gotta be a 1 and x3s gotta be a 1 or I can't make any further progress.
And similarly, I've gotta couple of clauses x x1 in omega 7 and x1 in omega 8.
Hey, those two clauses are satisfied. I can stop worrying about them.
That's great. So hey, I feel like I actually made some
progress. Two of my clauses fell off my list of
things I have to worry about. Omega 7 and omega 8.
Two more of my clauses fell off my list because they were unit.
I know what happens to them. X2 and x1 are, or x2 and x3, sorry, are a
1. Let's go forward and see what happens.
So here we are. I have again grayed out all of the
assignments that we got up to this point, and I am about to actually set x2 to 1 and
x3 to 1. So, let's see what happens.
And this is what happens, you know, in clause 1 and clause 2, x2 and x3
respectively become 1 and, you know, it's satisfied, no surprise.
But in clause omega 3, x2 and x3 now take the value 0 and x4 has been exposed as a
unit literal. This clause says, unit, I don't have a
choice. I now know exactly what has to happen to
x4, x4 has to be a 1. This is just an example of this fact that
the, just the fact that I assigned a few values to variables means that a whole lot
of other variables must take values if we are to proceed toward a satisfiable
solution. And in these gigantic industrial scale SAT
problems, the BCP just goes on and on and on and on, it's really the, the, the deep
algorithmic heart of these, of these techniques.
So x4 is a 1 we have discovered the clause omega 3 is unit.
That's great. That tells us something.
We can go forward and we can simplify. So, let's see what happens.
So we're about to set x4 to be equal to 1 and again I have grayed out all of the
previous assignments. And so if I go in and I set x4 to 1, well
clause omega 3 is satisfied, no surprise clause omega 4 is now unit because x4 is a
0. X5 is exposed as, something that must have
a value. And in clause omega 5, x4 is also a 0.
Literal x6 is exposed as a value that I now know.
So I have now discovered, that x5 and x6, we can deduce that they must, by
implication, have values. They have to be 1 and 1 respectively.
X5 has gotta be a 1, and x6 has gotta be a 1.
Great, I feel like I'm making progress, you know?
I continue to uncover clauses that are a unit.
I make the assignment that makes that clause satisfied and I uncover other
clauses that are a unit and it just keeps going.
It's like, wow, this thing is simplifying itself.
So let's go make that assignment. Omega 4 and omega 5 are now unit clauses.
We know what x5 and x6 have to be. Let's go do it.
So, moving forward, we are about to assign x5 and x6 to both values 1, respectively.
And let's see what happens. Well, in clause omega 4, x5 is a 1.
Omega 4 is satisfied. In clause omega 5, x5 is 1.
It's satisfied. And something bad happened.
Oh, look at what happened in clause omega 6.
Not x5 is a 0. Not x6 is a 0.
That's not happy. All right?
Clause omega 6 has now become unsatisfied. Right?
Clause omega 6 is a conflict, because of all of the implications to get to this
point of the other clauses that had to have values of certain variables, in order
for them to be satisfied, clause omega 6 is necessarily conflicted.
Oops. Sorry.
This is the way this works. This is why this sort of problem is
recursive. You go until either, something happy
happens like, you find an assignment that satisfies it or you go until something
unhappy happens like, oops, I got a conflict.
I guess I'm going to have to undo some decision very early on to make some
forward progress. So pretty much, you know, when you run a
SAT solver when BCP in the heart of the SAT engine finishes a pass, there are
really three things that can happen. I could have found a SAT assignment of all
the clauses I was working on so I could return a 1.