0:00

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

10:18

Exclusive OR, XOR you know, we write that as A circle with a plus sign, B.

The output is 1 just if a and b are different.

Okay? Right.

So that's, that's typically this, this gate.

It's kind of an OR gate with another bar on it.

A and B are the inputs. Lets say Y is the output.

This is Y equals a bar b plus A B bar. So this is the gate that makes a 1 when

its input are different. Exclusive NOR I like to write it this way.

I like to write it as an Exclusive OR gate with a bar over it.

Other people like to write it as a, like an AND function with a circle around it.

I'm not, not a, not a big fan of that. It's a, personal taste thing.

It's again a NOR gate, but it has a bubble on it, so that you are reminded that it is

Exclusive NOR. It has two inputs, A and B, and again, an

output Y. And A is I'm sorry Y, the output is a 1,

just if the inputs are the same. Right?

And so, this is Y equals AB Plus A bar, B bar and you can just see from the Boolean

formulas they are that the Exclusive OR is a 1 just if they're different and the

Exclusive NOR is a 1 just if they are the same.

So, just kind of a reminder. Right.

And so, the gate consistency function is the Exclusive NOR of the symbol for the

gate output. Exclusive NOR'd with the Boolean formula

of what the gate does. Now, what does that do?

It is something actually rather nice. The gate consistency function makes a 1

just for combinations of inputs and the output.

There are consistent, with what the gate actually does.

And so, what that means is that, the gate consistency function is an interesting

little object where you can put in an a and you can put in a b and you can put in

a d and the gate consistency function will say, 1, yes, that's what the gate does or

0, no, that's not what the gate does. For example, what if I have a as a 0, b as

a 0 and d as a 1? Well, this is a NAND gate.

So, I put in a 0 here. I put in a 0 here.

0 and 0 is 0. 0 inverted is 1.

Yes, indeed I should make a 1. This is consistent.

12:52

And go ahead. Try it.

What you'll discover is if you do this, phi d is a 1.

Phi d will say yes, a is 0, b is 0, d is 1.

Yes indeed. That's what this gate does.

But what if you did instead, this. What if you put in two 1s.

1 and 1 is 1. 1 inverted is a 0.

Unfortunately, I've just said that I think d one.

This is inconsistent. What will actually happen here, is that

phi d will be a zero. Right?

And so that's what phi d does. Phi d is a function that says hey, is this

what the gate does? It turns out that all you really need to

do to make the satisfiability formula for the entire gate network, is to put

together and together, all of the gate consistency functions because every single

one of those gate consistency functions basically links its inputs to its outputs

and for most of those gates, the output is an input on the next gate.

Right? And so this is the mechanism by which the

clauses get glued together so their values are all overlapping.

So, the only way to make the entire function a 1 is to have everything

consistent all the way through. Its an interesting incredibly practical

concept. So, for your logic network, you now have

to label each wire. Everything, right?

And so here are the inputs of this network and here is the output of this network.

And this is the same logic network before. Gates 1, 2, 3, 4, 5.

1 is a NAND, inputs a b output d. 2 is a NOR, inputs b c output e.

3 is NOT input d output f. 4 is an OR, input d e output g.

5 is an AND, input f g output h. You have to label every single internal

wire with a variable name. Right?

And the reason is that you're going to be writing Boolean equations for every single

gate. So, every input and every output has got

to have a name. So, let us assume that we'd like to do

this for g. All right, and so what I need then is I

need to go look at that gate. Alright.

And so those are internal nodes that need a name.

And that's an internal node that needs a name.

And so this is the gate that's an OR gate. It's got d and e going into it.

And it's got g going out of it. If we were to actually do this, you know,

gate consistency function, phi g is going to be the name of the output, which is g.

And this is going to be Exclusive NOR'd with a Boolean expression for what this

thing does, which is d plus e. If we were to actually grind that out, we

would discover that, that is d bar plus g ANDed with e bar plus g, ANDed with d plus

e plus g bar. And, there we have it.

And, you know, it's you know, it's worth doing this for a few of these others to

just sort of try your hand and kind of convince yourself what's going on here.

So, what do we do next? Well, to get the entire CNF for the entire

net list, what you do is the following. You build this CNF.

Ok, for phi. And it's got two parts.

You actually have to put the output variable there, as one of the clauses.

And then really, you know, there's the output variable.

16:36

And you actually have to put it there and there it is right there.

And the idea is that we are solving for satisfiability for the whole thing.

One of the thing is that it's got to be true is that h is a one.

And the way you make sure that h is a 1 in this clause database is by putting a

clause which has an h in it, which can only be satisfied if h is equal to 1.

Right? And then it's got a product and that

product means a big AND over every gate in the network, and then you put the gate

consistency functions. That's what the phi k's are.

And so, there is a gate consistency function for, for gate 1, and a gate

consistency function for gate 2, and a gate consistency function for gate 3, and

a gate consistency function for a gate 4, and a gate consistency function for gate

5. Right.

So same logic network here, NAND gate 1, NOR gate 2, NOT gate 3, OR gate 4 AND gate

5, exactly the same. And I've got this wonderful big clause CNF

format which I could just literally read off.

Gate 1 makes the gate consistency function.

Bam, put it down. Gate 2 makes the gate consistency

function. Bam, put it down.

Gate 3 makes the gate consistency function.

Put it down. Put down the one for 4.

Put down the one for 5. Remember to put in a single clause which

is the output variable. There you have it.

This is the CNF for your logic network. You can do it from the gates and wires

themselves just walking the network. Yeah, it's going to be pretty big.

Sorry. That's just the way it works.

Hand it to the SAT solver. Ask the questions you want to do.

So, you don't read to do any real Boolean algebra simplification other than for each

individual gate level function. And at the network level you AND them all

together. Now, as the result of this, smart people

have written the formulas down, because it's really boring to have to continue to

derive these. And this is a big complicated slide.

So I got this these formulas from pretty famous paper by, from Fadi Aloul, Igor

Markov, and Karem Sakallah. All at the University of Michigan where

they were, you know, just doing some interesting things with SAT.

And here are the formulas. So, there's a formula for interestingly

any, enough, a wire. Because sometimes you just have a wire

where you have sort of the output of one gate is called let's say x and the input

of next gate is called, let's say z. And you have a wire that looks like a

Boolean function, z equals x. You need a Boolean CNF formula for it.

X bar plus z, x plus z bar. And then, you need formulas for NOR gates,

OR gates, NAND gates, AND gates, and inverters.

Inverters are easy. X plus z, x bar plus z bar.

All of the rest of them are kind of complicated.

And they're kind of complicated, but they're also kind of simple.

They've all got exactly three parts. So let's just look for example, at the nor

gate. The first part is a product.

And it's a product over all of the inputs. There are n inputs.

And this particular product is xi bar plus z bar.

So, you've got, if you had a four-input NOR gate, you get four products and they

all look like xi bar plus z bar. And then, that is ANDed with a sum term

that's got two things in it. Right.

So this is a sum, this is you know, an OR. This is an OR of all the inputs.

So, if you had 4 inputs, x1, x2, x3, x4. This is x1 plus x2 plus x3 plus x4.

And then you've got one more term in this sum, which in this case is just the z

term. And if you look at each of these equations

for NOR OR, NAND AND, what you will discover is that they only differ in where

the compliment bar, where the bars are, you know, where the inversions are.

And it's just the way it works out if you do the exclusive nor of the function and

grind out the algebra. This is just the pattern.

And so, you know, just worth remembering them.

Or, you know, write them down on the back of your hand.

I guess that might be a better answer. Now, one other thing that I will, I will

admit, and this is unfortunate, but you know, I have to tell you how EXOR gates

and EXNOR gates work because they also have gate consistency functions.

And the problem is EXOR gates and EXNOR gates are rather unpleasant for SAT

solvers. The, the basic either-or structure makes

for some tough SAT search and they have rather large gate consistency functions

too. So, just the small two input gates creates

a lot of terms. And so here's the, you know, what happens

if z is equal to the Exclusive OR. Of a and b the gate level consistency

function will be z XNOR ax OR b. That's a little bit of unpleasant Boolean

algebra. I'm, I'm just writing it down for you.

I strongly encourage you to go figure out the one for the XNOR.

We don't need to, you could if you want, you could derive the formula for more

inputs. It's just unpleasant.

It's just big and ugly. But now you know, you have the gate level

consistency functions for all the gates worth knowing.

And you could walk the Boolean expression, the Boolean logic network that you had and

you could build a gate level consistency function.

And it's just worth, you know, just really doing one here, just to kind of convince

ourselves we know. So here, here is the general formula for

an n input NAND gate. It's got a product term, and it's got

that's ANDed with a sum term, that has one additional out contribution term, related

to the output. What happens if n is just two?

Right? Well what do you get?

So here's the product term. Right?

Because this product just means AND. And because n is equal to 2.

Right. The product from i equals 1 to 2 of xi

plus z is x1 plus z and x2 plus z. That's all that means.

And then there's a sum term. And again, n is equal to 2.

23:26

So that's it for, for Boolean satisfiability.

It's a wonderful important technology and, together with BDDs, it pretty much

represents the sort of the universe of, of representations and sort of large

computational tools for, for Boolean equations.

I'll note that SAT really has largely displaced binary decision diagrams for

that surprisingly large set of applications where I just need to solve

it. I just have to say, can I find a

satisfying assignment for this big Boolean function, yes or no?

Yes, give me one. No, okay that's what I need to know.

And so there are lots of things that have been transformed into forms that make SAT

the preferred technology but BDDs are still really important and all over the

place. The big reason for SAT is that its more

scalable. You can do gigantic problems, 50,000

variables, 25 million clauses, 50 million, against fifty million clauses.

Right? Sorry.

50 million literals you know, appearances of variables in the clauses.

But, you know, literally,you know, tens of thousands of variables, tens of millions

of clauses. Those are gigantic problems.

You can actually solve those things, you know, kind of remarkably quickly.

Still SAT, like BDDs, not, not, not guaranteed to find a solution in a

reasonable amount of time or space. The idea is, you know, 40 to 50 years old,

depending on which paper you're looking at.

But it's still the big idea. Davisputnamlogemannloveland is the, the

sort of the computational guts of the recursion.

But there have been some amazing engineering advances that make it

stupendously fast. And we're actually going to get to play

with this on some homework assignments. Before I finish this, this lecture riff, I

just wanted to have some acknowledgments to some of my friends.

Karem Sakallah is my buddy from the, the University of Michigan.

I'll admit, I'm a University of Michigan alum.

Like me and Claude Shannon and Karem was very generous with you know time and

inputs in some very early versions of these lecture materials.

And his former PHDA student Joao Marques-Silva, who did some of the

earliest work on conflict learning provided some the samples in some of the

papers that I'm using for this. And he's now at the University College

Dublin. So big thanks to both of those guys for

helping me out on this lecture. And now we're going to move from

representing things to synthesizing things.

So that's our next great set of topics. [music].