MUS Finder

A simple selector variable based MUS finder was implemented. It was used only for Figures 5.4 and 5.5 in the thesis, but it also implements the autarky based redudancy check of Definition 5.27, and several other experimental features which have not been seriously tested and which are thus not recommended.

The source code is available here. Before compiling, make sure that the environment variable MROOT is set to the root directory of the desired MiniSAT version. For the Figures 5.4 and 5.5 this MUS Finder was linked to MiniSAT-log.

The data for the times clause involvement visualizations Figures 5.4 and 5.5 can be obtained by running the MUS finder as follows on benchmark barrel5.dimacs:

./mus -cref barrel5.dimacs 2>musfinder-barrel5
./mus -cref -rotate barrel5.dimacs 2>musfinder-barrel5-rotate