0:01

So here in Lecture Four we're going to complete

our exploration of Computation Boolean Algebra and

we're going to show you the other great class of methods for

dealing with the Boolean objects as data structures and operators.

In the last lecture, we showed binary decision diagrams as a really powerful

data structure that supports a really nice and useful set of operations.

Now, the thing that's interesting about BDDs is that

they represent the complete Boolean function.

That's great, but there are many engineering examples where all I really

need to know is that there is a way to make a Boolean function make a one

as the output or that that there is no way to have the Boolean function make a one.

And it's surprising that that's enough but in a lot of engineering scenarios, and

we're going to see that in this lecture, that's true.

And so in this lecture,

in Lecture 4.1 were going to introduce this new classic method which are called

Boolean Satisfiability or because satisfiability has lots of syllables.

SAT, S-A-T for short like BDD for short.

So we're going to talk about SAT.

What we're going to talk about in this intro lecture is the representation

scheme called Conjunctive Normal Form that lets us do SAT efficiently.

1:55

And we're going to figure out an assignment of those variables so

that they have values zeros and ones that make the function a 1.

And that's really what satisfy means.

A boolean function is satisfied when it makes a 1.

Now this assignment might not be unique.

There could be lots and lots and lots of satisfying solutions.

We are going to be happy if we can just find one of them, but

if there is no satisfying assignment at all, we expect our technology to prove it,

which is to say to demonstrate conclusively that there is no way to

make this boolean function a one.

There is no way to satisfy it, and to return that information to us.

Now it turns out that there are lots and

lots of things that you can do with BDDs which are good for

basically representing the totality of the structure of a Boolean function.

But you know,

not the most efficient technology if all you want to do is satisfy it.

So it turns out that if you just want to solve it and

decide if it's able to be made one or not, satisfiability technology is easier,

it's faster, it scales to much larger instances of the problem.

And so it's really the preferred solution for solving things.

So SAT scenarios where you just want to find a satisfying assignment or

prove that there isn't one.

3:12

So what's an example of that?

We showed you one of those.

This is the network repair example from the early computational Boolean

algebra lecture.

So suppose that you are able to have some known good version of the logic.

Maybe a boolean equation that does the right thing and

a gate level implementation that's just not working.

That's the picture shown at the top.

And we showed you this very interesting idea where you can replace

a suspect logic gate with in this case a 4:1 multiplexor if it's a two input gate.

With inputs d0 to d3, and we said okay look, take the logic network that's

suspect, take the gate out that is suspect, replace it with a 4:1 mux,

make a bigger function that has these new variables associated with it.

Put that through an exclusive nor gate, which is an equality gate,

a gate that makes a one just if those two blocks of logic for making a one and

make this function that's a function of the original inputs and the new variables

that was specified a multiplexer and then say hey, I'd like this Boolean function to

be one all the time for all possible values of the inputs.

And so universally quantify them away.

We made this function and

what we said was if you could solve it which is to say if you could make it

equal to a one you could affect the bully and network repaired So here it is.

Here's an example of one of these I just want to solve it kinds of scenarios.

Assuming you can build the quantification function for

all a, b, Z, can you go find a SAT assignment to get the d values?

If so, you can repair the network.

Conversely, if the SAT solver comes back and says hey,

no there's no way to solve this quantified Boolean expression.

There is no network repair possible.

So here's a very nice, concrete, engineering-oriented scenario where

solving the Boolean equation is really what I want to do.

Well there's some terminology for these things.

And interestingly enough there is a standard form for these things.

The most convenient form for pursuing this solution.

This is something called Conjunctive Normal Form CNF.

And what's amazing is that you know this you just don't know the name.

This is a product of sums form.

Each of the individual terms in the parentheses is the or

of some variables in truer complemented form, and we and them all together.

Now, I know what you're probably thinking.

You're thinking, wow, I think I learned this when I started college,

when I was learning digital design.

But you know, mostly I remember Mostly I remember sum of products from, right?

Because I'd make a carnal map and I'd circle the ones and I'd get

these friendly terms that look like products with plus signs in between them.

And then I think that they made learn how to circle zeros and

I could also represent the function.

But I representing the zeros and

it was very complicated because I had invert all the variables.

And I just as soon forget it.

Sorry, here we are.

It's back. There's

a reason to learn Product of Sums Form.

And honestly, the reason to learn Products of Sums Form is because it's the right

6:43

Now, one of the things to note here is this sort of the angle bend sign?

This means not, right?

So this is the same as saying, c bar or saying c prime,

this is kind of mathematical logic notation for a negation.

And because this stuff came from the mathematical logic side of the universe,

wow, 50 years ago, The literature is filled with stuff like this, so

I'm just going to keep that, so you have some sense of what it looks like.

Why is the CNF useful?

Hey!

You only need to determine if one clause evaluates to

a zero to know the if whole formula is a zero.

Hey! They're all added together.

You want to make a 1, none of these things had better be a 0.

So it's real easy to tell when they are not satisfiable.

But of course, if you really want to satisfy it, you have to make all

the clauses identically 1, and that's maybe the hard part.

7:39

One more bit of terminology, an assignment.

An assignment gives values to some, but not necessarily all, of your variables.

And other terminology's pretty straightforward here.

A complete assignment assigns values to all the variables,

a partial assignment assigns values to some of the variables.

An assignment means we can evaluate the status of the clauses, and

the clauses can be in different kinds of states.

So, let's just make an arbitrary decision, A is zero, B is one, but

C and D are unassigned.

And ask some questions, and look at a bit of terminology.

So if a is a 0 and b is 1, then in the first clause, a plus not b,

that's going to be a 0, that's also going to turn into a 0.

And this whole clause, evaluates to a 0, and

the term for this is that this clause is conflicting.

8:27

Why is it conflicting?

It conflicts with our goal of satisfying the boolean equation.

We're kind of, sort of, hoping that we can find a way to make this fee function a 1.

If a clause evaluates to a 0 it is in conflict with that goal, and

we say it is conflicting.

Now what about the next clause not a + b + not c?

Well the a is going to turn into a 1 and the b is going to turn into a 0 and

I don't need to know anymore this clause actually is 1.

And this clause is said to be satisfied, no big surprise.

This clause is satisfied because it's a 1.

What about the next cross, a + c + d, well, the a is a 0 and

I don't know anything more.

And so, all we can frankly say about this clause is that it is unresolved.

I don't know enough to know if it's going to be a 0 and be a conflict, and

I don't know enough to make it a 1 and say it's satisfied.

So, I just don't know.

It's unresolved.

And for the last one, not a is going to be a 1,

not b is going to be a 0, and this clause is also satisfied.

So, those are the things that we can say about a clause.

It's conflicting with our goal of satisfying the boolean equation.

It's satisfied because it's a 1 or, hey, I don't know.

It's unresolved.

9:46

This is going to be a pattern we see over and over again in the VLSI CAD universe.

You've got some really gigantic complicated problem and

you don't know how to solve it, maybe you can break up into smaller pieces,

solve the pieces, and put the answers back together again.

So I'm going to show you a little bit of how the recursion works in the next slide.

But the recursion has two big ideas.

The first one is decision, and what decision means is,

look Sometimes you just gotta select a variable, assign it a value.

It is kind of arbitrary, but the goal is that if you assign

a value to a variable, you can simplify the CNF formula and

maybe you'll be able to learn something, maybe it satisfies.

Maybe it's a conflict and you know that's a bad idea, and you have to undo it.

So the basic idea is you decide something, rather arbitrarily, and then you pursue,

in the CNF form, how it simplifies and whether you can solve it or not.

The more interesting bit, honestly, is the deduction part.

And in deduction, you look at the newly simplified clauses, and

you continue to simplify iteratively.

Based on the structure of the clauses,

you can deduce that other values must be assigned to other variables.

And this is sort of the cool part.

Of boolean satisfiability.

Even though you've arbitrarily decided maybe only a few variables,

a whole bunch of other variables might need to have certain values,

because otherwise satisfiability is just impossible.

And that turns out to be really the heart of boolean satisfiability.

And so you keep doing this until nothing simplifies, and

then either you can satisfy it or not.

And, if not, then you have to go back up and

decide some more, and you keep pursuing this.

What does this look like?

Well, just the decision part here, here's a Boolean equation,

x + y + z, not x y (Not y + z) (not x + not y + not z).

Let's try to make some progress here.

And so we shall decide that x is a 1.

Well then, in the left-hand box I get (1) for

the first clause, (y) for the second clause, (not y + z) for the third clause,

(not y + not z) And that's still too complicated for me to do anything.

So let's just decide that y is 1 and see what happens.

And then I still get something with a little bit of complexity, 1z z bar.

Now at this point you might be thinking, hey Didn't we just spend like

a whole half of a week learning about binary decision diagrams?

You know it's not like Z Z bar is a really complicated function.

Couldn't I just represent that and figure out that's a zero?

And the answer is, well yeah conceptually yes, but in practice no.

Because this kinds of boolean SAT formulas we're trying to solve are so

gigantically large that you just don't have time to build a BDD for

every one of these search nodes.

You actually have to have a Different very,

very light weight kind of technology to go ask the question and answer it.

So for us you still can't answer this question is this a one yes or no.

No, I can't answer it and so I have to go further and assign z equal zero then you

know I can actually tell that this thing is unsatisfiable and

so I'll go back over and I'll say well let’s try making z the other value.

And I'll discover it's still unsatisfiable.

And I'll go back up and I'll undo y = 1, and I'll make y = 0, and

I'll discover again, it's unsatisfiable.

Go back up, undo the x=1 decision, decide x = 0, and gosh, that's complicated.

Can't do anything there, and so I'll decide to set z = 1, and hey!

I satisfied it.

And so I am done, and you'll note that I don't have to search for

the rest of the tree.

Boolean satisfiability works like this.

Go find me a satisfying assignment.

Once you've found it, give it to me.

I'm a happy guy.