1 00:00:00,002 --> 00:00:02,545 [music]. Hi. 2 00:00:02,545 --> 00:00:09,551 I'm Nick Chen, one of the teaching assistants for Rob Rutenbar's VLSI CAD: 3 00:00:09,551 --> 00:00:13,652 Logic to Layout course. This is the second tutorial in our series 4 00:00:13,652 --> 00:00:17,044 of video tutorials, introducing you to several tools that you can use in this 5 00:00:17,044 --> 00:00:19,673 class. Today we'll be talking about MiniSat. 6 00:00:19,673 --> 00:00:24,684 Minisat, according to its website, is a minimalistic open source Sat solver 7 00:00:24,684 --> 00:00:29,626 developed to help researchers and developers alike to get started on Sat. 8 00:00:29,626 --> 00:00:34,250 Minisat is a rather successful Sat solver. It has already won several competitions. 9 00:00:34,250 --> 00:00:38,099 It's also very fast, as you'll experience when you try out the tool for yourself. 10 00:00:39,530 --> 00:00:43,242 As usual, this video tutorial has an accompanying document that will be made 11 00:00:43,242 --> 00:00:47,110 available on the class website. We expect you to read the document. 12 00:00:47,110 --> 00:00:51,338 And this video just shows how to actually use the two through the web interface. 13 00:00:51,339 --> 00:00:56,150 The example we're using is from this Realistic Usage Example section shown on 14 00:00:56,150 --> 00:01:01,892 the right hand side of the screen. The purpose of the example is actually to 15 00:01:01,892 --> 00:01:07,274 determine whether the network you see here on the left is equivalent to the network 16 00:01:07,274 --> 00:01:11,706 you see here on the right. On the following page of the tutorial, we 17 00:01:11,706 --> 00:01:15,440 have already expressed the network as a set equation. 18 00:01:15,440 --> 00:01:19,019 And here's how you actually express it in the DIMACS-format input file. 19 00:01:20,240 --> 00:01:26,827 I've actually copied and pasted the following text, into my text editor. 20 00:01:26,828 --> 00:01:29,815 Here's the text that I've just copied and pasted from the document. 21 00:01:29,815 --> 00:01:33,808 I'm not going to go through the file format here, because it's actually 22 00:01:33,808 --> 00:01:36,804 described in great detail in the document itself. 23 00:01:36,804 --> 00:01:39,744 What I do want to point out is something that may be a bit unexpected. 24 00:01:39,745 --> 00:01:44,529 You must terminate each of your lines with the symbol character zero. 25 00:01:44,529 --> 00:01:49,653 This is something that's a bit more unusual, so I do want to take the time to 26 00:01:49,653 --> 00:01:53,332 point it out. I'm going to save the file and then we can 27 00:01:53,332 --> 00:01:57,885 upload it to the class website. Here's our class website. 28 00:01:57,885 --> 00:02:03,868 If you scroll it down and navigate to the Programming Assignments tab. 29 00:02:03,868 --> 00:02:07,381 Click on it. You'll see that this is Week 1, so we have 30 00:02:07,381 --> 00:02:11,515 the Computational Boolean Algebra Programming Assignment out. 31 00:02:11,515 --> 00:02:15,872 I'm just going to do, minimize that. If you scroll down here, you'll see the 32 00:02:15,872 --> 00:02:18,913 Tools section. Kbdd was introduced in the previous 33 00:02:18,913 --> 00:02:22,619 tutorial. What we're interested is actually MiniSat. 34 00:02:22,619 --> 00:02:26,942 Scroll down all the way till you see MiniSat. 35 00:02:26,942 --> 00:02:32,620 Click on the Submit button. Choose the text that you just saved as 36 00:02:32,620 --> 00:02:37,821 part output submission. It's in Desktop. 37 00:02:40,090 --> 00:02:48,185 And hit Submit. You see that it says, your submission has 38 00:02:48,185 --> 00:02:54,330 been accepted and will be graded shortly. Go back to the previous page on 39 00:02:54,330 --> 00:03:02,379 Programming Assignments. Scroll to Tools and view the Feedback. 40 00:03:02,380 --> 00:03:12,674 Here is the feedback for my previous one. There are three main sections. 41 00:03:12,675 --> 00:03:16,687 First is the Results. In this case, if you have something that 42 00:03:16,687 --> 00:03:22,007 it can be satisfied, you'll print out SAT and give you the satisfying equations. 43 00:03:22,008 --> 00:03:28,857 Here in the MiniSAT Standard output section, you get to see some statistics. 44 00:03:28,858 --> 00:03:32,514 This tells you something like the number of variables, the number of clauses that 45 00:03:32,514 --> 00:03:36,639 you have and then the time that it takes. There are more details in the document 46 00:03:36,639 --> 00:03:40,565 accompanying this video tutorial on what each actually means. 47 00:03:40,566 --> 00:03:45,591 If you still have any questions about this, feel free to actually post something 48 00:03:45,591 --> 00:03:50,445 on our discussion forums and one of the staff members will get back to you. 49 00:03:50,445 --> 00:03:55,571 So, that's the output from MiniSAT for something that can actually be satisfied. 50 00:03:55,571 --> 00:03:59,475 I'm going to give you example for something that cannot be satisfied. 51 00:03:59,475 --> 00:04:06,058 Here's my text editor again. And now I have an equation that cannot be 52 00:04:06,058 --> 00:04:08,468 satisfied. This is taken from this particular 53 00:04:08,468 --> 00:04:10,824 website. So, if you are interested you can go ahead 54 00:04:10,824 --> 00:04:13,952 and go to there, and download some of the benchmarks for yourself. 55 00:04:13,952 --> 00:04:19,310 I'm now in the Coursera website again and I'm going to upload the text file that 56 00:04:19,310 --> 00:04:23,958 I've just saved. I'm going to scroll down, look for 57 00:04:23,958 --> 00:04:28,372 Programming Assignments. Click on it. 58 00:04:28,372 --> 00:04:33,836 Scroll all the way to the bottom for Tools. 59 00:04:33,836 --> 00:04:39,010 Click Submit. This time, I'm going to choose the 60 00:04:39,010 --> 00:04:43,736 unsatisfiable SAT equation. Submit. 61 00:04:43,736 --> 00:04:50,120 And it notifies me that my submission has been accepted. 62 00:04:50,120 --> 00:04:55,479 Go back to Programming Assignments. Scroll to the bottom. 63 00:04:55,480 --> 00:05:00,707 Open Tools. When the results are available, I can 64 00:05:00,707 --> 00:05:04,876 click on the view. And here are the results. 65 00:05:04,876 --> 00:05:09,980 As you can see, this is an unsatisfiable equation. 66 00:05:09,980 --> 00:05:13,457 So, in MiniSat Results, you see the word UNSAT. 67 00:05:13,458 --> 00:05:18,290 And if you look at the standard output, you're going to see the same problem 68 00:05:18,290 --> 00:05:22,854 statistics, except it's going to say unsatisfiabe here at the bottom. 69 00:05:22,854 --> 00:05:27,404 Again, MiniSat is pretty robust and it should be able to handle any errors that 70 00:05:27,404 --> 00:05:31,134 you have in your input and tell it may not be able to pass things. 71 00:05:31,134 --> 00:05:36,204 In the event that you do encounter something which you can't diagnose, please 72 00:05:36,204 --> 00:05:41,274 let us know what MiniSat reports in the Standard error and we can take a look for 73 00:05:41,274 --> 00:05:43,829 you. I also like to point out that MiniSat, 74 00:05:43,829 --> 00:05:48,245 like many of the other tools that you'll be using for this course, is actually 75 00:05:48,245 --> 00:05:51,106 quite easily installable on your own machines. 76 00:05:51,107 --> 00:05:55,657 If you want, you can go to the MiniSat website and just try to install version on 77 00:05:55,657 --> 00:05:58,569 your own machine. That may make it easier for you to 78 00:05:58,569 --> 00:06:01,561 experiment. And there you have it, a very short 79 00:06:01,561 --> 00:06:05,575 introduction to using MiniSat through the course website. 80 00:06:05,576 --> 00:06:09,180 Again, if you have any questions, feel free to ask on the discussion forums. 81 00:06:09,180 --> 00:06:11,303 Thank you.