Modified AIGBMC

The data for several figures presented in the thesis was generated using a modified version of AIGBMC, which was linked to MiniSAT-log.

AIGBMC from the AIGER 1.9.4 toolset was modified to use MiniSAT instead of PicoSAT. The complete modified sources can be found here. To compile this version of AIGBMC, make sure that the MROOT environment variable is set to the root directory of the MiniSAT version you would like to use. To generate clause involvement visualizations from AIGBMC one should link it to MiniSAT-log. The modifications adds two command line parameters to AIGBMC:
-c
Continue upto the specified maximum bound even if a counterexample is found.
-j
Solve ONLY the encoding of the specified maximum bound (no incremental solver usage).

The following AIGER benchmarks were used for clause involvement visualizations in the thesis:
bc57sensorsp2neg.aigHWMCC'07 benchmark l2s/bc57sensorsp2neg.
eijk.S1238.S.aigHWMCC'07 benchmark tip/eijk.S1238.S.
pdtvisgigamax2.aigHWMCC'11 benchmark pdtvisgigamax2.
example_n3.aigSee Example 4.10 / Appendix A.

The data for several of the clause involvement visualizations in the thesis can be obtained by running the following commands:

./aigbmc -m -c bc57sensorsp2neg.aig 110 2>hwmcc07-aigbmc-bc57sensorsp2neg
./aigbmc -m eijk.S1238.S.aig 50 2>hwmcc07-aigbmc-eijkS1238
./aigbmc -m pdtvisgigamax2 150 2>hwmcc11-aigbmc-pdtvisgigamax2
./aigbmc example_n3.aig 30 2>example-inductive-n3