Department of Computer Science
CPSC 513: Introduction to Formal Verification and Analysis

Assignment 2:

Please email me your completed program (cmbcmp-sat.c only, with any additional files you added, but not the SAT solver, the object files, the benchmarks, etc.) and a brief plain text description of your results on the ISCAS 85 benchmarks. Be sure to start early!

Your task is to write a yet another combinational circuit comparison program, but this time using a SAT solver. I'm too lazy to set this up with the API for the SAT solver we're using, so instead, your program will take the names of two input files containing circuits and will print a SAT instance that is satisfiable iff the circuits are different. (And, aside from my laziness, previous 513 students have said they appreciated having the SAT instances being external text files, to make it easier to inspect the results and test their code.) The SAT solution tells you what input assignment will make the circuits give different results, but it's entirely optional if you want to write a helper program to translate the SAT output back into the names of the inputs to the circuits.

As with the preceding assignment, you'll test your program on the ISCAS 85 benchmarks.

I am providing a SAT solver, as well as skeleton code that reads ISCAS 85 files, builds up a circuit data structure in memory, and generates most of the needed clauses in the DIMACS CNF format that the SAT solver wants. Feel free to use or modify as much of this code as you wish. (The easiest thing to do is just search for "FIX THIS!!!" in the skeleton code and make your changes there.) The assignment took me very little time; I expect it will take you longer, as you'll need to familiarize yourself with my code and the SAT solver.

If you're running on a CS dept Linux machine, you can use my pre-installed version of MiniSat at /isd/users/software/minisat-2.2.0/core/minisat_static . Note that MiniSat doesn't tell you what the satisfying assignment is unless you specify an output file. So, you'll typically be running like:
cmbcmp-sat circuit1.isc circuit2.isc > foo.cnf
minisat_static foo.cnf bar.txt

If you're not running on the CS dept machines, your best choice is probably to go to the MiniSat pages , download, and build your own copy. It's a very small program, and compiles perfectly under Linux. (Read the README file and follow the build instructions there. Note that on my Ubuntu box at home, the GNU make program is just called "make" instead of "gmake", so at home, I followed the same instructions to build as in the README file, except I typed "make rs" instead of "gmake rs".)