SpySMAC is an algorithm configuration tool based on SMAC for SAT solvers
It is distributed under the GNU Public License. See COPYING for details regarding the license. Please note that SMAC (shipped with SpySMAC) is released under a different license. For non-commercial and academic use, it is free to use. Please contact Frank Hutter to discuss obtaining a license for commercial purposes.
SpySMAC is an algorithm configuration and analyzing tool. It is written in Python and uses SMAC (Java). It combines the configuration quality of SMAC and extensive analysis providing insights into the optimized parameter settings.
As the computations are potentially executed on a cluster, SpySMAC is not installed via pip. Just clone the repository including all the submodules via
$ git clone https://github.com/sfalkner/SpySMAC.git && cd SpySMAC/
$ git submodule init
$ git submodule update --checkout --recursive
examples - directory containing a small set of instances and miniSAT
cmd_building_scripts - directory with example script how to write your own command line builder
fanova - powerful parameter importance evaluation package
pysmac - a package providing the python inteface to SMAC
SpySMAC - directory containing the python scripts
COPYING - GNU Public License
CHANGELOG - Major changes between versions
README.md - This file
SpySMAC_run.py - script to run the configuration
SpySMAC_analyze.py - script to analyze the confiuration runs
latex_tools - directory with files to automatically generate a paper via SpySMAC_analyze.py script
See:
$ python SpySMAC_run.py -h
Here is a small example for the well known SAT solver MiniSAT. First, let us have look at the input:
$ cd examples/ && ls -l .
minisat/
swv-inst/
In "swv-inst", you will find the some compressed software verification instances. Please extract them with:
$ cd swv-inst
$ tar xvfz SWV-GZIP.tar.gz
Now, we have to compile minisat:
$ cd ../minisat/
$ export MROOT=`pwd`
$ cd core && make
Last but not least, we can start SpySMAC on minisat and the SWV instances:
cd ../../..
python SpySMAC_run.py -i ./examples/swv-inst/SWV-GZIP/ -b ./examples/minisat/core/minisat -p ./examples/minisat/pcs.txt --prefix "-" -o ./spysmac_logs/ -B 60 -c 2 -r 2 -n 2
Here is a break down of the arguments:
'-i ./examples/swv-inst/SWV-GZIP/' : SWV instances
'-b ./examples/minisat/core/minisat' : MiniSAT binary
'-p ./exapmles/minisat/pcs.txt' : PCS file of MiniSAT
'--prefix "-"' : Prefix of parameters
'-o ./spysmac_logs/' : Output directory of log files
'-B 60' : configuration budget in sec
'-c 2' : runtime cutoff of an individual algorithm run
'-r 2' : perform 2 independent SMAC runs
'-n 2' : execute 2 runs in parallel
'-s 1' : use seed=1 (any positive integer would do here)
After approx. 1 minute, you will find all generated data during configuration in "./spysmac_logs/". To compare against the default configuration of MiniSAT, we have also to evaluate the default configuration, which is done by running SpySMAC with seed 0:
python SpySMAC_run.py -i ./examples/swv-inst/SWV-GZIP/ -b ./examples/minisat/core/minisat -p ./examples/minisat/pcs.txt --prefix "-" -o ./spysmac_logs/ -c 2 --seed 0
If you run now the analyzing script, a report of the configuration run will generated:
python SpySMAC_analyze.py -i spysmac_logs/ -o spysmac_report/
You can see the report by opening "spysmac_report/index.html" in the web browser of your choice. And you can see the generated paper in the "spysmac_report" folder together with the tex files.
To use for example the ijcai13 template you have to write in your terminal:
python SpySMAC_analyze.py -i spysmac_logs/ -o spysmac_report/ -t ijcai13
And for help type
python SpySMAC_analyze.py -h
Please note that the configuration run was very short and SMAC could not collect a lot of data. Therefore, we don't expect a large improvement on this mini example and also the parameter importance results may be very vague.
We recommend the following things to improve the results of SpySMAC:
To give you an idea of how these reports could look like, we used a subset of the data generated in the CSSC2014 and applied our analysis to it.
Stefan Falkner
Marius Lindauer
Frank Hutter
University of Freiburg
{sfalkner,lindauer,fh}@cs.uni-freiburg.de