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 (zip archive of 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. Unlike in the previous assignment, instead of using the API to the SAT solver (or BDD package in the previous assignment), 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. (I originally created the assignment this way out of laziness, as it's very easy to program this up without looking up details of the SAT solver. It's also very portable to different solvers. But aside from 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. But if you end up using SAT in your project (or in real life), you'll most likely want to use the proper API.) 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 (zip archive).

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. (BTW, the DIMACS format description I provided is to a copy of the original document and is longer than what you need (and we use only the CNF version of the format). This webpage gives a shorter description (ignore the stuff specific to Varisat). If you're really curious about the history, you can look at the Second DIMACS Implementation Challenge on this page.) Feel free to use or modify as much of my 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.

• Skeleton C program for this project.
• (New this year!) The CaDiCaL SAT Solver. This year, I want to try the CaDiCaL SAT solver. This is a state-of-the-art solver that is actively being used for some very impressive results (including solving open problems in mathematics), but is also designed to be small and easy to understand and modify. You can download or git clone your own copy (it built easily under Linux on my home and departmental machines), if you wish.
• (Optional, Back-Up Solver) Information about the MiniSat SAT solver. In previous years, I've been using MiniSat, which is still quite competitive (and also designed to be simple to understand and modify). If you have problems with CaDiCaL, feel free to use MiniSAT instead.

If you're running on a CS dept Linux machine, you can use my pre-installed version of CaDiCaL or MiniSat at /isd/users/software/cadical/build/cadical and /isd/users/software/minisat-2.2.0/core/minisat_static . I haven't found really good documentation on CaDiCaL, but you can get the basic options by using the -h flag: /isd/users/software/cadical/build/cadical -h .

The usage of CaDiCaL and MiniSat are slightly different. For CaDiCaL, you'll typically be running like this:
cmbcmp-sat circuit1.isc circuit2.isc > foo.cnf
cadical foo.cnf
CaDiCaL prints its output to stdout by default, so you can save the output to a file by redirecting:
cadical foo.cnf > bar.txt
In contrast, MiniSat doesn't tell you what the satisfying assignment is unless you specify an output file. So, you'll typically be running like:
minisat_static foo.cnf bar.txt
(without the redirection). (Aside: If you provide an additional file name to CaDiCaL, it will output a proof of unsatisfiability (if the result is unsatisfiable. I'm not sure what the meaning of the output is if it's satisfiable.) in "DRAT" format, which we'll hopefully talk about later in the course.)

If you're not running on the CS dept machines, your best choice is probably to go to respective solver pages (linked above), and build your own copy. They are small programs, and compile perfectly under Linux. (For MiniSat, 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". Ignore this parenthetical for building CaDiCaL.)