Experiment 5.19 - Simulation of solver usage by MUS finders

The experiment was performed using the following selection of 65 unsatisfiable benchmarks from the application benchmarks of the SAT Competition 2011. The 'incremental clause addition' version results were obtained using a modified version of MiniSAT 2.2.0, MiniSAT-jhooker. The 'Clauses with selector variables' version result was obtained by modifying the 65 CNF files into 65 iCNF files, by adding selector variables and an assumptions line using this AWK script. These iCNF files were then solving using MiniSAT-icnf.

The raw results for the experiment can be found in this CSV file. For each version there are three columns in this file corresponding to the CPU time, the real time (i.e. wall clock time) and the solver result. The cactus plot was drawn based on the CPU time column.