[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.