SAT Competition 2020
The Main Track (as well as the Glucose Hack Subtrack) will be run on the StarExec-cluster.
The solvers will be executed with a time limit of 5000 seconds and memory limit of
The StarExec system will be also used for submitting the solvers.
Usage of StarExec
Getting an acount
- Register for an account in the SAT community (unless you are already registered).
- Wait until one of the SAT community leaders (Marijn Heule and Tomas Balyo) approves your request (should not take more than 24h).
- If you register late
in the season, it may also be necessary to add your new user account to the respective spaces mentioned below. Please send an email to the organiziers if you do not seem to be able to find the necessary spaces on StarExec. (Also note that you might need to log out of StarExec and then log in again to see such changes taking effect.)
Uploading a solver for testing
- The solver is submitted by uploading its source code and a build script. The solvers are then compiled by StarExec.
- The uploaded file must have a special format (see the StarExec User Guide for details, here is an example with minisat). Please follow the required directory structure precisely otherwise StarExec will not be able to compile and run your solver.
- Login to StarExec and click Spaces->Explore (on the top) then on the left open root->SAT->Sat2020Testing
- At the bottom of page click "upload solver" to open the upload dialog.
- Click "Browse" and select the zip file with your solvers code, enter the solver name, change downloadable to "no" (otherwise everyone can see you source code) and click "upload".
Testing your solver
We put a few testing instances in the Sat2020Testing space which you can use if you uploaded your solver to this space. To run a test:
- Go to the root->SAT->Sat2020Testing space.
- Click "create job" on the bottom of the page. This opens a page where you don't need to change anything so just click "next". (Update: currently the testing problems in Sat2020Testing are compressed using bz2. If your solver does not support native uncompression, just additionally choose "unpact bz (272)" as a preprocessor here.)
- On the next page select the "choose" option and then "all in Sat2020Testing"
- A page with all solvers (and their configurations) comes up, select the solver you want to run and click "submit" at the bottom of the page.
- You can check out the status and results of your test job by clicking on Jobs on the top and selecting your job.
Outputing proofs in the Main Track
The proof for UNSAT instances must be written in a file called proof.out and placed in the folder which your start script gets as the second parameter ($2). Thefore your starexec_run_default should contain something like
#!/bin/bash ./solver $1 --proof-file=$2/proof.out
Note, that the answer line ("s SATISFIABLE" and "s UNSATISFIABLE") and the solution in case of a satisfiable instance (lines starting with "v") must still go to stdout (not into "proof.out").
Testing proof output validation
To test that your proofs are correctly validated by the version of drat-trim installed on StarExec, it is easiest to download this job xml description, unzip it, replace (while keeping the quotes) "YOUR-SOLVER-CONFIGURAION-ID-GOES-HERE" in the xml file there with your solver's configuration id as found on StarExec (example here), zipping again and uploading the result to the testing space Sat2020Testing using Jobs/"upload job xml" button. This will run your solver on the five testing benchmarks out of which three are unsatisfiable. If your solver solves at least one of them under 300s, drat-trim will be subsequently run on the produced proofs. When inspecting the finished job, do not forget to check both "job information" and (the more detailed) "job output".
Uploading the final version of your solver
The submission of the final version of a solver is essentially the same as uploading the solver for testing (see above). To submit the final version of your solver upload it to the space root->SAT->SatComp20->[track], where [track] is one of Main, Planning and NoLimits, depending on the track you want to participate in (Glucose hacks should be uploaded to the Main Track space) . If you want to participate in several tracks upload your solver to each one of them separately.
Don't forget to select "downloadable:no" when uploading your solver to prevent other participants from seeing your source code before the start of the competition. After the solver submission deadline we will ask all the participants to update the downloadable option to "downloadable:yes". This will make the source code visible to the organizers and all the participants. The participants must comply with this request in order to participate in the competition (except for the No Limits Track).
For the Parallel Track and the Incremental Library Track the source codes are submitted by email to the organizers.
Emailing your System Description Document and Benchmarks to the organizers
After you have submitted the final version of your solver send an email to the organizers (firstname.lastname@example.org) containing your system description document and 20 benchmark problems (see General Rules for more information).