Modified versions of MiniSAT 2.2.0

The original version 2.2.0 of MiniSAT can be downloaded from http://www.minisat.se. Here, we provide only the files that we have modified with respect to version 2.2.0. Only the 'core' version of the solver was used in experiments in the thesis.

MiniSat-log

This version of MiniSAT prints log files for creating clause involvement visualizations. It was used for creating all such visualizations in the thesis, either linked to AIGBMC or linked to the MUS finder.
core/Solver.ccModified version of Solver class implementation for MiniSAT-log.
core/Solver.hModified version of Solver class definition for MiniSAT-log.
core/SolverTypes.hModified version of basic solver datastructures for MiniSAT-log.

MiniSat-icnf

This version of MiniSAT only differs from the original in its file parser, and its main calling routine. The modifications enable it to read iCNF files. It was used in Publication II, and Experiment 4.12.
core/Main.ccModified version of main routine for MiniSAT-icnf.
core/Dimacs.hModified version of file parser for MiniSAT-icnf.

MiniSat-jhooker

This version of MiniSAT only differs from the original in its file parser, and its main calling routine. The modifications will make the solver solve any CNF file by adding one clause at a time to the solver, and running the solver after each clause addition. This type of "incremental solving" was inspired by John Hooker's paper from 1993. It was implemented as part of an argument regarding constructive MUS finding algorithms in Experiment 5.19.
core/Main.ccModified version of main routine for MiniSAT-jhooker.
core/Dimacs.hModified version of file parser for MiniSAT-jhooker.