#SpySMAC SpySMAC is an algorithm configuration tool based on SMAC for SAT solvers

#LICENSE 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.

#OVERVIEW 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.

#REQUIREMENTS

• Python 2.7 (or 3.4 soon)
• numpy (during the analysis, not for the configuration phase)
• matplotlib (during the analysis, not for the configuration phase)

#INSTALLATION 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

#PACKAGE CONTENTS 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

#USAGE See:

$ python SpySMAC_run.py -h

#Mini Example with MiniSAT

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.

#RECOMMENDATIONS

We recommend the following things to improve the results of SpySMAC:

• use at least 200 SAT formulas as instances (the more the better)
• use a homogeneous instance set (i.e., all instances from one application); on heterogeneous instance sets, configuration gets a lot harder
• the default configuration of your solver should solve at least 50% with the given runtime cutoff
• as configuration budget, you should be at least 200 times the runtime cutoff (more is better)
• since SMAC is a stochastic process and the configuration space has many local minima, several indepent runs of SMAC will improve also the result (use option -r); we recommend at leat 10 SMAC runs

#Examples

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.

###minisat-HACK-999ED-CSSC

• CSSC-K3-300s-2day
• CSSC-CircuitFuzz-300s-2day
• CSSC-3cnf-v350-300s-2day
• CSSC-Queens-300s-2day
• CSSC-unsat-unif-k5-300s-2day
• CSSC-GI-300s-2day
• CSSC-LABS-300s-2day
• CSSC-IBM-300s-2day
• CSSC-BMC08-300s-2day

###probSAT

• CSSC-3SAT1k-sat-300s-2day
• CSSC-5SAT500-sat-300s-2day
• CSSC-7SAT90-sat-300s-2day

###Riss-4.27

• CSSC-GI-300s-2day
• CSSC-BMC08-300s-2day
• CSSC-K3-300s-2day
• CSSC-Queens-300s-2day
• CSSC-CircuitFuzz-300s-2day
• CSSC-3cnf-v350-300s-2day
• CSSC-LABS-300s-2day

###YalSAT

• CSSC-3SAT1k-sat-300s-2day
• CSSC-LABS-300s-2day
• CSSC-5SAT500-sat-300s-2day
• CSSC-GI-300s-2day
• CSSC-7SAT90-sat-300s-2day

###clasp-3.0.4-p8

• CSSC-Queens-300s-2day
• CSSC-GI-300s-2day
• CSSC-BMC08-300s-2day
• CSSC-3cnf-v350-300s-2day
• CSSC-CircuitFuzz-300s-2day
• CSSC-K3-300s-2day

###cryptominisat

• CSSC-GI-300s-2day
• CSSC-CircuitFuzz-300s-2day
• CSSC-LABS-300s-2day
• CSSC-IBM-300s-2day
• CSSC-Queens-300s-2day
• CSSC-BMC08-300s-2day

###CSCCSat2014

• CSSC-5SAT500-sat-300s-2day
• CSSC-7SAT90-sat-300s-2day
• CSSC-3SAT1k-sat-300s-2day

###DCCASat+march-rw

• CSSC-K3-300s-2day
• CSSC-3cnf-v350-300s-2day
• CSSC-unsat-unif-k5-300s-2day

###lingeling

• CSSC-Queens-300s-2day
• CSSC-GI-300s-2day
• CSSC-LABS-300s-2day
• CSSC-CircuitFuzz-300s-2day

###SparrowToRiss

• CSSC-3cnf-v350-300s-2day
• CSSC-IBM-300s-2day
• CSSC-GI-300s-2day
• CSSC-3SAT1k-sat-300s-2day
• CSSC-CircuitFuzz-300s-2day
• CSSC-Queens-300s-2day
• CSSC-LABS-300s-2day
• CSSC-K3-300s-2day
• CSSC-BMC08-300s-2day
• CSSC-5SAT500-sat-300s-2day
• CSSC-7SAT90-sat-300s-2day

#CONTACT

Stefan Falkner
Marius Lindauer
Frank Hutter
University of Freiburg
{sfalkner,lindauer,fh}@cs.uni-freiburg.de