[music].
Hi.
I'm Nick Chen, one of the teaching
assistants for Rob Rutenbar's VLSI CAD:
Logic to Layout course.
This is the second tutorial in our series
of video tutorials, introducing you to
several tools that you can use in this
class.
Today we'll be talking about MiniSat.
Minisat, according to its website, is a
minimalistic open source Sat solver
developed to help researchers and
developers alike to get started on Sat.
Minisat is a rather successful Sat solver.
It has already won several competitions.
It's also very fast, as you'll experience
when you try out the tool for yourself.
As usual, this video tutorial has an
accompanying document that will be made
available on the class website.
We expect you to read the document.
And this video just shows how to actually
use the two through the web interface.
The example we're using is from this
Realistic Usage Example section shown on
the right hand side of the screen.
The purpose of the example is actually to
determine whether the network you see here
on the left is equivalent to the network
you see here on the right.
On the following page of the tutorial, we
have already expressed the network as a
set equation.
And here's how you actually express it in
the DIMACS-format input file.
I've actually copied and pasted the
following text, into my text editor.
Here's the text that I've just copied and
pasted from the document.
I'm not going to go through the file
format here, because it's actually
described in great detail in the document
itself.
What I do want to point out is something
that may be a bit unexpected.
You must terminate each of your lines with
the symbol character zero.
This is something that's a bit more
unusual, so I do want to take the time to
point it out.
I'm going to save the file and then we can
upload it to the class website.
Here's our class website.
If you scroll it down and navigate to the
Programming Assignments tab.
Click on it.
You'll see that this is Week 1, so we have
the Computational Boolean Algebra
Programming Assignment out.
I'm just going to do, minimize that.
If you scroll down here, you'll see the
Tools section.
Kbdd was introduced in the previous
tutorial.
What we're interested is actually MiniSat.
Scroll down all the way till you see
MiniSat.
Click on the Submit button.
Choose the text that you just saved as
part output submission.
It's in Desktop.
And hit Submit.
You see that it says, your submission has
been accepted and will be graded shortly.
Go back to the previous page on
Programming Assignments.
Scroll to Tools and view the Feedback.
Here is the feedback for my previous one.
There are three main sections.
First is the Results.
In this case, if you have something that
it can be satisfied, you'll print out SAT
and give you the satisfying equations.
Here in the MiniSAT Standard output
section, you get to see some statistics.
This tells you something like the number
of variables, the number of clauses that
you have and then the time that it takes.
There are more details in the document
accompanying this video tutorial on what
each actually means.
If you still have any questions about
this, feel free to actually post something
on our discussion forums and one of the
staff members will get back to you.
So, that's the output from MiniSAT for
something that can actually be satisfied.
I'm going to give you example for
something that cannot be satisfied.
Here's my text editor again.
And now I have an equation that cannot be
satisfied.
This is taken from this particular
website.
So, if you are interested you can go ahead
and go to there, and download some of the
benchmarks for yourself.
I'm now in the Coursera website again and
I'm going to upload the text file that
I've just saved.
I'm going to scroll down, look for
Programming Assignments.
Click on it.
Scroll all the way to the bottom for
Tools.
Click Submit.
This time, I'm going to choose the
unsatisfiable SAT equation.
Submit.
And it notifies me that my submission has
been accepted.
Go back to Programming Assignments.
Scroll to the bottom.
Open Tools.
When the results are available, I can
click on the view.
And here are the results.
As you can see, this is an unsatisfiable
equation.
So, in MiniSat Results, you see the word
UNSAT.
And if you look at the standard output,
you're going to see the same problem
statistics, except it's going to say
unsatisfiabe here at the bottom.
Again, MiniSat is pretty robust and it
should be able to handle any errors that
you have in your input and tell it may not
be able to pass things.
In the event that you do encounter
something which you can't diagnose, please
let us know what MiniSat reports in the
Standard error and we can take a look for
you.
I also like to point out that MiniSat,
like many of the other tools that you'll
be using for this course, is actually
quite easily installable on your own
machines.
If you want, you can go to the MiniSat
website and just try to install version on
your own machine.
That may make it easier for you to
experiment.
And there you have it, a very short
introduction to using MiniSat through the
course website.
Again, if you have any questions, feel
free to ask on the discussion forums.
Thank you.