[music]. So, here in Lecture 4.3 we're going to

complete our exploration of Computational Boolean Algebra by completing our

discussion of Boolean SAT. And what we've seen so far is at, at a

high level, how to represent a SAT problem in a CNF form and how something like a

Boolean constraint propagation can help us answer the questions about satisfiability

or unsatisfiablity. But what you don't know yet is, how would

I actually take a realistic network of logic gates and turn it into this slightly

strange looking CNF form. And, how would I actually pose an

engineering relevant question like, are these two implementations of this big,

complicated Boolean function as logic gates, are these two things the same or,

or not? What's going on?

Turns out there's a surprisingly simple mechanical procedure for going from real

logic, with gates and wires, into CNF form.

And so we're going to walk through that and complete our discussion of Boolean

satisfiability in this lecture. I, I think it's first good to actually

just take a little bit of a step back, because what we really did this week in

the course is, you know, for the first half of the week we did binary decision

diagrams, and for the second half of the week we did Boolean satisfiability.

It's important to know that they're not, they're not the same.

They're complimentary. So, this is a kind of, of a slide that

says, you know, they're really not equal. You know, they're not, they're not really

exactly the same. And it's important to know both.

That's why we spent this entire week on these two really vital topics.

So look. Bdds often work well for many problems,

and SAT often works well for many problems.

But for both of them there is no guarantee that it will always work.

Sorry. It is just in the nature of solving things

that are exponentially hard, that sometimes your heuristic techniques might

not work. So, for a BDD, basically, what we can do

is we might be able to, we hope, build a BDD to represent the function.

And for the SAT side, we can solve for satisfiability with a yes or no answer on

that function. And those things are really different

things. Okay.

Now lets be all, lets be, lets be clear that sometimes I cannot build the BDD with

reasonable computer resources. And what typically happens is you run out

of memory. You just don't have enough gigabytes to

build the BDD. And on the SAT side, you sometimes cannot

find the SAT solution. You cannot find a satisfying assignment or

prove that one does not exist with reasonable computer resources.

Typically, you run out of time. You know, you just, you're just searching

and searching and searching and searching and you just, you just don't finish.

So, one of the things to be remembering is that, you know, the BDD does in fact build

a full representation of the function. It represents everything there is.

It is, in fact, a canonical representation of the function, that's one of the really

cool things about BDDs. But SAT solvers do not represent the

entire function. Which is to say, they do not represent it

in a way that supports a big, rich, beautiful set of manipulations.

You want to do a sort of an arbitrary kind of a computational thing on a Boolean

function. You probably want to start with a BDD

because you just have this rich pallet of operators.

But, if you just want to solve for the Boolean functions, say, hey, can I make it

0? Yes or no, that's when you want to use

SAT. So, for example, you can build the

functions that represent existential and universal quantifications.

That's, you know, one of the kinds of manipulations you can do in a BDD

universe. In the SAT universe, it turns out that

there are actually different versions of SAT solvers.

Not every SAT solver, but there are versions of SAT solvers.

They are called Quantified SAT solvers, where you can say, okay, look here's the

function and you give it to him in a CNF form.

And then you say, and here are the variables I would like to quantify away

please. And the SAT solver does some interesting

internal magic and then solves for satisfiability on the quantified function.

It's a whole different category of SAT solvers.

But, you cannot do arbitrary Boolean manipulations with SAT solvers.

You can solve for SAT. That's what they do.

If you want to do arbitrary things on a Boolean function, you probably want a BDD.

You can do SAT with a BDD. It's just probably the not, the most

efficient way. Okay?

So important? Maybe a little bit subtle set of

distinctions but, you know, if you sort of get this internalized.

You'll be, you'll be making some real progress toward, you know, toward being,

being a serious[UNKNOWN] person. So you know, what's a typical practical

SAT problem? Hey, I have two logic networks.

And they are both logic networks of exactly the same inputs and I would like

to know if they are the same Boolean function.

I would like to know if F does exactly the same thing as G.

So, I'm just asking the question is F the same thing as G?

How do you do that? Well, what you do typically is the

following. For every pair of outputs, and let's just

assume that F1 is supposed to be G1. They're supposed to be doing the same

thing. And F2 is supposed to be G2.

They're supposed to be doing the same thing.

For every pair of outputs, you put an Exclusive OR Gate.

So you put F1 in there and G1 in there. And then over here, you also put another

Exclusive OR Gate and you put F2 over there and G2 over there.

Now, let's think for a minute. What will make the Exclusive OR Gates 1.

And it's the answer if the F and the G inputs disagree.

All right. So, the only way to make a 1 with these

XOR gates is to have F and G not be the same function.

Ok. So, what are we looking for here?

We're looking for a single OR gate. Ok.

Let's call that Z. And what's going to be true?

Well what's going to be true is that Z is going to be 1.

It's going to be satisfiable, right? We shall be able to find a pattern of Xs,

that makes Z make a 1 if and only if F is not equal to G.

Right? That makes sense, right?

And so and if we can find Z satisfiable. Right?

Then we will find an X that has the property.

Right? That, that, you know, something that F

does with X is not equal to something that G does with X.

It's going to be, you know, at least, you know, one of those, one of those sets of

inputs is going to be different. So that's pretty cool, right?

I have two big complicated, you know, pieces of real engineering logic.

And I'd like to say, wow are these two things doing to the same thing?

Exclusively or the associated outputs, or together all of those exclusive ORs ask a

Boolean satisfiability solve it question. Hey, can I make Z equal to a 1?

If I can make Z equal to a 1, the networks are not the same.

This patterns of inputs makes the outputs different.

And not only will I discover that this is the case, but I will get an input X that

actually makes F and G different, that might be helpful as a debugging tool.

And if it unsatisfiable, if Z is always 0, then yes they are in fact the same logic.

They're doing the same thing. So that's pretty cool.

But that raises a whole bunch of questions.

And the first question is how do I start with a gate-level description and get a

CNF? Isn't this hard?

Right. I mean, don't I need Boolean algebra or

BDDs or something complicated? The CNF form was you know, a little weird.

You know, it certainly felt a little awkward.

And you know, if I have some big logic network with 50,000 gates in it, isn't

that just hideous? And the answer is no.

It's actually really, really easy. It's surprisingly easy.

But we have to build up a little bit of technology, a little bit of math to, to

get us there. So let's, let's take a look at that.

So, here's a little logic network. There is a NAND gate numbered 1 with two

inputs, and a NOR gate number 2. And of the three inputs of this circuit,

one of them is shared between gates 1 and 2.

Gate 1 goes to an inverter ,gate 3, and as one input of an OR gate, gate 4.

Nor gate 2 is also the other input to gate 4.

And gate 5 is an AND gate that takes the output of inverter 3 and OR gate 4, and

that's it. So, how do you do this CNF thing?

And the big wonderful simple idea is that you can build up the CNF one gate at a

time. So, we need to introduce a concept here.

And the concept is that there is a gate consistency function, which we will call.

If the whole, let's say the whole function is, is, you know, something called phi.

The gate consistency function is phi sub name of output.

So let's, let's say that we've got this NAND gate here, it has inputs a and b, and

it has an output called d. And so, the gate consistency function is

called phi d. And this is actually equal to d equivalent

to the function of the gate. So let's remember here that, you know,

what this gate is really doing. This gate is an, NAND gate.

So it's ab bar. That's what this gate is doing.

So, this is really nothing more than the symbol that we use for the output of the

gate, Exclusive NORd with the Boolean formula for what this gate is supposed to

be doing, which is ab bar. And if you do just a little Boolean

simplification on this, you will get a plus d, b plus d, a bar plus b bar, plus d

bar, and this is equal to phi sub d. Now, okay.

Why am I doing this? You know, what, what good is this?

This turns out to be a really, a really, you know, magical little, little helpful,

helper function that's going to actually let us get a CNF for the entire network no

matter how complicated it is, one gate at a time.

So first, just a little review, just so everybody's, you know, up on this.