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