.--. .--. .--. .--. .---. .--. ,-. .-. : .--': .--': .--': .--' `--. :: ,. :.' : .'.' : : `. `. `. `. : : ,',': :: : `: :.'.'_ : :__ _`, : _`, :: :__ .'.'_ : :; : : ::_ ` : `.__.'`.__.'`.__.'`.__.' :____;`.__.' :_; :_: This is a test environment for preparing an entry to the Configurable SAT Solver Competition, CSSC 2014. The folder structure is identical to what we'll use in the competition. Your submission will go into a subdirectory of solvers/ and you should not have to change any of the other files. In fact, any changes you make outside that folder won't be part of your submission, so if you believe something outside that folder needs to be changed please email us at cssc.organizers@gmail.com. We provided a few examples of parameterized solvers as subdirectories of the solvers/ directory. Each of these subdirectories would constitute a valid submission, so if you use one of them as an example everything should work. In order to use this test environment, you'll need Linux (sorry Mac users, the runsolver tool won't work for you) with Python2.7 and Java6 installed. Please check whether the following binaries are executable: * configurators/smac-v2.06.00-master-615/smac * scripts/runsolver * scripts/SAT Especially, the last two tools have to be recompiled on 32bit systems. The source can be found in scripts/sources/ ========================== Components of a submission ========================== (1) Source code or binary for your solver. (2) Parameter configuration space (.pcs) specification file (3) A short script translating a partial parameter instantiation to a command line call to your solver, setting those parameters. Some information about each of these components: (1) We use exactly the same input/output format as the 2014 SAT competition (and in fact the same scripts to verify correctness). Only submissions with source code are eligible for medals. (2) This file specifies your solver's parameters and their domains, as well as dependencies between parameters. Please see pcs-format.pdf for the details and the .pcs files of the provided solvers for examples. We encourage you to include two versions of this file: one that natively handles numerical parameters, and one that uses your domain knowledge to pick some interesting values for them and treats them as categorical. There are two reasons for this: (a) ParamILS can only handle categorical parameters and it might be the best configurator for your solver. (b) In some cases, we have noticed that the domain knowledge going into the discretization can result in *better* performance than when searching the "proper" range of the numerical parameter. See solvers/spear/spear-params.pcs for an example of a discretized version of the mixed continuous/discrete file spear-params-mixed.pcs. (3) We require your solver directory to contain a Python script called Wrapper.py that implements one methods, i.e., get_command_line_cmd() (Note to last year's submitters: no worries, you can reuse your scripts; see the section below.) Please have a look at the docstring for the documentation. The output of the method is an executable command line callstring to your solver, to run on the provided instance, with the provided seed (if you support that, not crucial), and with the provided parameter values. Using the provided example solvers for reference, it should not be hard to fill in this function; it typically has about 5 lines. However, if you don't want to touch any Python code you don't have to; instead, you can provide a script (written in your programming language of choice) that reads the inputs (instance file, seed, configuration) from a file, creates the command line call using them and outputs the call to stdout. You would then copy minisatWrapper.py from the example solver directory minisat_with_ruby_wrapper, which writes a file with the inputs, calls your script and reads its output to get the command line call. You have to add "--ext-callstring \"\"" to the "--algo" definition in the SMAC call. ===================================== Using the ruby wrapper from CSSC 2013 ===================================== If you already participated in the CSSC last year, you can easily use your Ruby wrapper from last year. Your Ruby function from last year's callstring_generator.rb is extended by some code we provide and is called via the new Python wrapper. An example is given in the example solver directory minisat_with_ruby_wrapper. You can simply use your callstring_generator.rb script from last year and add the last part of file solvers/minisat_with_ruby_wrapper/callstring_generator.rb (starting with the comment "The code below stays the same for every Ruby wrapper; simply replace the function above."). You can then call SMAC as in Example 4 below. ======================= Testing your submission ======================= Various things can go wrong when you first parameterize your solver: - Path issues: this is one of the common problems when wrapping a solver for configuration. Here, we minimized the risk for this problem by defining the directory structure we will use. Everything should work if you put the files for (2) and (3) above in the root of your solver subdirectory, and make sure that the command line call generated with the script in (3) is executable from the root of the cssc directory (e.g., put a binary of your solver in our solver subdirectory and use 'solvers/minisat/minisat-static'). If you don't change the remaining files there shouldn't be any path issues when we wrap your solver call with runsolver, solution checking, etc. - Input parsing bugs: make sure that your solver actually uses the parameter values defined in your command line call. We simply execute that call and cannot check the solver's internals. - Bugs with certain parameter values: non-default solver options are tested less frequently than the defaults, so it is likely that there are some bugs. The SMAC configurator, which is part of this download, can be used as a rudimentary fuzz testing tool. When called with the option "--executionMode ROAR" as below, it generates random instantiations of parameters, runs your solver with them on some instances and checks its result. When called without that option, it performs a targeted search for good configurations. In either case, when you use the flag "--abortOnCrash true" it terminates whenever a solver run crashes. ======================= What exactly to submit: ======================= To submit, simply zip up your subdirectory of the solvers/ directory and send it to us (cssc.organizers@gmail.com). If you want to be eligible for medals also include source and information on how to build the binary from it. Before you submit, please ensure that an example configuration run using SMAC goes through without errors. We give examples and hints on debugging your submission below. Please also add include the following information in your email: * name(s) of author(s) * contact email address * name of your solver * literature reference as bibtex entry (if possible) ======================================================================= Examples: some calls of SMAC for our example solvers and instance sets. ======================================================================= We strongly suggest that before you run SMAC on your own solver, you make sure everything is set up correctly by running it on one of the example solvers we provide. Below you can find several example calls to execute. Note that each of these calls will run SMAC for up to 4000 seconds, generating lots of (somewhat cryptic) output. You don't need to run SMAC to completion for every example (Control-C will terminate it, with a "friendly" exception); you can also control SMAC's budget with the wallClockLimit parameter. The important thing is that SMAC doesn't crash and stop; if it crashes for one of the provided examples something bad and unexpected happened - please email us in that case. The syntax for calling SMAC and its random sampling variant ROAR is as follows: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --wallClockLimit 4000 --executionMode ROAR --scenarioFile --algo "python scripts/SATCSSCWrapper.py --script ./solvers//.py" --paramfile solvers// Example 1: MiniSAT on a regressiontest benchmark suite, trying random parameter configurations: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --executionMode ROAR --scenarioFile ./scenarios/regressiontests-5s-1h.txt --algo "python scripts/SATCSSCWrapper.py --script ./solvers/minisat/minisatWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt" --paramfile solvers/minisat/minisat-params.pcs Example 2: MiniSAT on a regressiontest benchmark suite, actual search for good parameter configurations: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --scenarioFile ./scenarios/regressiontests-5s-1h.txt --algo "python scripts/SATCSSCWrapper.py --script ./solvers/minisat/minisatWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt" --paramfile solvers/minisat/minisat-params.pcs Example 3: MiniSAT on SWV: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --scenarioFile ./scenarios/CSSC-SWV-GZIP-5s-1h.txt --algo "python scripts/SATCSSCWrapper.py --script ./solvers/minisat/minisatWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt" --paramfile solvers/minisat/minisat-params.pcs Example 4: MiniSAT (with Ruby wrapper) on SWV: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --executionMode ROAR --scenarioFile ./scenarios/CSSC-SWV-GZIP-5s-1h.txt --algo "python scripts/SATCSSCWrapper.py --script None --ext-callstring \"ruby solvers/minisat_with_ruby_wrapper/callstring_generator.rb\"" --paramfile solvers/minisat/minisat-params.pcs Example 5: MiniSAT on 3-SAT: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --scenarioFile ./scenarios/CSSC-uf250-5s-1h.txt --algo "python scripts/SATCSSCWrapper.py --script ./solvers/minisat/minisatWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt" --paramfile solvers/minisat/minisat-params.pcs Example 6: SPEAR on SWV with logging of runs: ./configurators/smac-v2.06.00-master-615/smac --numRun 0 --wallClockLimit 4000 --doValidation false --abortOnCrash true --executionMode ROAR --scenarioFile ./scenarios/CSSC-SWV-GZIP-5s-1h.txt --algo "python scripts/SATCSSCWrapper.py --log True --sat-checker scripts/SAT --sol-file ./instances/true_solubility.txt --script ./solvers/spear/spearCSSCWrapper.py" --paramfile solvers/spear/spear-params.pcs ========================= Debugging your submission ========================= Once SMAC works on the above examples you can try it for your own solver. Simply take one of the callstrings above and replace the solver directory and the parameter file with yours. If SMAC works on the solver examples we provided but crashes for your own solver, then there is a problem with either your parameter file, your command line generation method, or your solver. You would get one of the following problems: Problems locating the parameter file yield an exception like the following: Error occured running SMAC ( ParameterException : Could not find a valid PCS file named in any of the following locations : ([...]) please check the file exists or for a previous error) Syntactical problems with the parameter file yield an exception like the following: Error occured parsing: [ERROR] StackTrace:java.lang.IllegalArgumentException: Cannot parse the following line: Any other errors related to your wrapper function or your solver that lead to a crash of SMAC will cause SMAC to output a line like the following as part of its error message: [INFO ] Failed Run Detected Call: cd "/home/lindauer/git/cssc/." ; python scripts/SATCSSCWrapper.py --script ./solvers/minisat/minisatWrapper.py instances/Sat_Data/test/reg_test_48d.cnf SATISFIABLE 1.0104007351875306 2147483647 8433049 -phase-saving '1' -var-decay '0.5' -ccmin-mode '1' -rnd-init '0' -rnd-freq '0' -rfirst '10' -luby '1' -rinc '4' -gc-frac '1' -cla-decay '0.999' You can debug all of these latter errors by simply copy-pasting the above command line call (include the cd statement) and manually executing it on the command line. These problems can range anywhere from a syntax error in your wrapper function, a problem locating your solver binary, a problem in the generated command line, a segmentation fault in the solver when run with a certain parameter configuration, or a bug in the solver (e.g. yielding an incorrect solution for a certain instance when run with a certain parameter configuration). Once you fixed the cause of the problem simply run SMAC again and iterate until no problems remain. To debug your algorithms, you can add "--log" as an argument to the python wrapper (see Example 6) to log all runs of your solver in a csv file named target_algo_runs.csv. With "grep CRASHED target_algo_runs.csv", you find all crashed runs the output of your algorithm and runsolver for these runs. If the wrapper option "--sat-checker scripts/SAT" is used, SAT modells are also verified with "SAT" tool. This option will be used in the CSSC. With "grep "SOLVER BUG" target_algo_runs.csv", you find all runs that returned wrong solutions - probably due to a solver bug. To test your submission under a variety of conditions, you should try all the following 3 scenarios before submitting: ./scenarios/regressiontests-5s-1h.txt (heterogeneous, thus not too interesting for configuration, but a good scenario for debugging) ./scenarios/CSSC-SWV-GZIP-5s-1h.txt (software verification instances generated with the static checker Calysto on gzip) ./scenarios/CSSC-uf250-5s-1h.txt (satisfiable uniform random 3-SAT with 250 variables at the phase transition) In all these simple scenarios, each solver run is capped at 5 seconds (as opposed to 300 seconds in the competition), and the budget for configuration is 1h as opposed to 2 days in the competition. Once everything goes through for these 3 cases, you're ready to submit :-) ===================== Questions & Feedback: ===================== Please send us email at cssc.organizers@gmail.com