Last update: February, 14 2005.
Please note that some details
might be updated before the competition starts. Changes will be clearly
identified. Please check that web page regularily. Important update
will be announced on SAT Live! Please send your comments to SATCompetition@satlive.org
32 nodes PIII 450MHz, 1GB RAM, 2GB /tmp, 2GB swap 8 nodes Athlon 1800+ (1533MHz), 2GB RAM, 15GB /tmp, 2GB swap 15 nodes Athlon 1800+ (1533MHz), 1GB RAM
For C and C++ source submissions GCC version 3.3.5 will be used for compilation. No other versions are supported. You will need to 'port' your source code to be compilable under version 3.3.5 of GCC prior to submission.
We require that the compilation flag '-static' is used and further recommend '-O3 -fno-strict-aliasing'.
No platform specific options are allowed, such as '-mcpu=i686' or '-march=i686', but we welcome additional options, e.g. '-DNDEBUG', which should precisely be communicated to the organizers or set in the compilation script or Makefile that is included in the sources.
The 2005 edition of the SAT competition will see some changes in the way the competition runs (not in the requirements for the benchmarks or solvers).
The SAT competition is now using some rules that made CASC sucessful.
This year, we will remove holes in variable numbering. As a consequence, the "p cnf nbvar nbclause" line will reflect exactly the number variables in the formula (numbered from 1 to nbvar) and the exact number of clauses.
Note that the order of the variable will not be affected.
Benchmarks submitters are invited to provide a detailed description of the benchmarks, including:
There are two options to participate in the SAT Competition: by participating in the competition itself or by participating in the system demonstration.
In both cases, a 2 page description of the solvers describing the techniques used, technical issues and the expected behavior of the solver (e.g., does it only solve satisfiable formulas) should be submitted together with the solver.
A paper describing the solver might simultaneously be submitted to the SAT 2005 conference, unless a published description already exists. However, submission of a paper is independent of submission of a solver and should follow those guidelines.
Solvers in the competition division will be tested in identical execution environments, rated, and compared with each other. There will be winners in various categories.
To enter the competition division, the SAT solver must be submitted in source and with a build script (normally Makefile) that allows the organizers to easily build the SAT solver from source into a statically linked binary (flag -static). Solvers written in C or C++ will be compiled using the latest version of GCC using UsualOptimisations. Solvers written in Java will run on the latest JVM (1.5) using hotspot server. For solvers written in another language, or if you need a specific compiler, please ContactTheOrganisers.
The authors must allow the SAT competition to release the source code of their solver for research purpose on its web site.
Rationale: Every material submitted to the SAT competition will be available for research purposes after the competition.
The demonstration division is intended to provide greater flexibility for exposure of solvers when the authors cannot or wish not to comply with the requirements for the competition division.
Solvers in the demonstration division might not be tested in identical execution environments; they will not be rated or compared with other solvers. There will not be winners. Their test results simply will be recorded and publicized.
To enter the demonstration division, the SAT solver normally should be submitted either as source, with the same guidelines as the competition division, or as a statically linked binary for linux using UsualOptimisations and flag -static.
The authors normally should allow the SAT competition to release the binary of their solver for research purpose on its web site. If source is also submitted in the demonstration division, it is not released without the authors' explicit permission.
Entries for which the authors do not wish to release either source or binaries for research purposes may be accepted in the demonstration division under special circumstances, at the discretion of the organizers, if it appears that participation will benefit the research community. One possibility is that tests will be run remotely with communication over the internet, at the authors' site. Please ContactTheOrganisers to make special arrangements.
Randomness is not permitted. Each solver should produce repeatable results when run on the same input formula with the same conditions of time and space availability. Pseudorandomness is perfectly acceptable if the program controls it by specifying a random seed whose calculation is repeatable under the same conditions as just mentioned.
-O3 -NDEBUG -static -fno-strict-aliasing
java -server -Xms<SATRAM> -Xmx<SATRAM>
A Competition category is the combination of one Solver category and one Benchmark category.
Solver categories: SAT, UNSAT, SAT+UNSAT, UNSAT+PROOF
Benchmark categories: Industrial, Hand_crafted, Random.
Series fall within Benchmark categories. Problems fall within Series. "Problems" are synonomous with "Formulas".
OPEN PROBLEMS may be accepted as though they are UNSAT at the discretion of the organizers -- primarily, they should have some kind of theoretical interest, not just be difficult. OPEN PROBLEMS might become a Series.
For each Competition category, we award the solvers with the three highest scores (bronze, silver, gold medals).
Each solver's score within its Competition category will be based on the number of problems solved within the time budgets, the amount of time used, and the number of series in which the solver solved at least one problem. The scoring rationale is discussed in the next section.
The precise formula will be publicized after the solvers are submitted (possibly sooner) and before any competition runs begin.
Solvers receive various credits for successes. Credits are computed by dividing purses for various achievements among those solvers that achieved the requirement for the purse. Shares of all purses are computed to sufficient accuracy to break ties correctly. Purses come in three types: solution, speed, and series.
There are no penalties for terminating abnormally, or giving up by answering UNKNOWN. However, an incorrect claim of SAT or UNSAT normally eliminates the solver from the competition and any shares of purses it has won are redistributed.
Tentative scoring plans:
Each problem has a solution purse, which is divided equally among all competition solvers that solve the problem. The standard solution purse is 1000 points. Normally, all problems in a Competition category will have the standard solution purse, but there might be exceptions. If no solver solves a certain problem, its solution purse is not distributed.
Each problem has a speed purse, which is divided unequally among all competition solvers that solve the problem. The speed purse will be a fixed multiple of the solution purse for all problems in the entire competition; it will give a weighting between solving and speed. If no solver solves a certain problem, its speed purse is not distributed.
The formula to divide the speed purse of a problem is the following, where p is problem id and s and i are solver ids and times are in seconds.
speedFactor(p, i) = timeLimit(p) / ( 1 + timeUsed(p, i ) )
where i solved p. It is 0 if i did not solve p.
speedAward(p, s) = speedPurse(p) * speedFactor(p, s) / sum_i ( speedFactor(p, i) )
Thus, the division is pro rata by speedFactor.
Each series has a series purse, which is divided equally among all competition solvers that solve at least one problem in the series. If no solver solves any problem in a certain series, its series purse is not distributed.
Normally, all series in a Competition category will have the same series purse, which will be a fixed multiple of the standard solution purse, for all series in the entire competition, but there might be exceptions. The series purses reward breadth of application.
The coefficients and multiples have not yet been determined.
Each problem (benchmark) has a "prize" for solving it, or a "purse" as they say in horse racing. The standard purse is 1000 points.
If k solvers solve the problem within the time limit, they split the purse k ways.
This provides a natural way to give more credit for solving "hard" problems without introducing arbitrary weights to measure "hardness" -- the winners simply split the purse among themselves.
A state-of-the-art contributor (SOTAC) solver in the CASC
terminology is one that solved some problem that no one else solved.
That is an automatic 1000 and is likely to
be worth more than being great at "stealing candy from babies", i.e.,
knocking off all the easy problems.
If 2 solvers out of 40 are able to solve a problem, that should be more
significant than if 30 / 40 solved it, but for SOTAC there is no