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 (so as a plain text file (that is with extension .txt)) of your results on the ISCAS 85 benchmarks. Be sure to start early!
Your task is to write a combinational circuit comparison program. The program will take the names of two input files containing circuits and will print whether or not the circuits are functionally equivalent. If they are not, the program should print an input vector that distinguishes the two circuits.
To give you interesting data to work with, I'm providing a copy of the ISCAS 85 benchmarks. This is an industry-standard set of combinational benchmarks. (I realize this benchmark set is older than many of you are, but it's still used in some papers even now.) The benchmarks have names like "c1908". You are to use your program to compare the version of the circuit in the DATA subdirectory (e.g. "c1908.isc") with a logic-optimized version of the same circuit in the NONREDUN subdirectory (e.g. "c1908nr.isc"). These circuits are supposed to be the same. Note, however, that in the past there were bugs in the benchmark set -- circuits that were supposed to be the same were actually different. You can see if your program can catch these mistakes by comparing against the old versions in the NONREDUN subdirectory (e.g. "c1908nr_old.isc").
Your task is to write a combinational circuit comparison program using a SAT solver. 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. 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. You'll test your program on the ISCAS 85 benchmarks.
You need a SAT solver to complete this assignment. Here are three links to popular solvers. They all should read CNF or DIMACS files:
Note that this assignment is a slight adaptation of the assignments proposed by Alan Hu. Here is his course webpage. Thanks Alan!