The SAT Competition is back

A satellite event of the SAT 2007 conference.

We took a break in 2006, thanks to Carsten Sinz who organized the SAT Race.

But the SAT Competition is coming back! ... soon. That web page will be updated regularly in the next two weeks.

The whole process will be very similar to the SAT 2005 competition.

The IO requirements and input format haven't changed since 2003. If you are a newcomer to the SAT competition, you should check that your solver comply with those simple requirements:

May 31, 2007: In a few hours, the results will be publicly available. Check out the contestants for now. You can also take a look at the presentation done during the conference.

February 15, 2007: A special issue of the JSAT journal will be dedicated to the competitive events related to SAT 2007.

January 19, 2007: Register your solver to the competition.

December 13, 2006: Check out the rules in details!

Important dates

December 31, 2006
Deadline for submitting benchmarks
January 31, 2007
Deadline for submitting solvers
February-March 2007
First stage
end of March 2007
First stage results checking
April 2007
Second stage
May 1-13, 2007
Second stage results checking
May 28-31, 2007
Results disclosed

Special tracks

And-Inverter Graphs input special track

There will be a special track using Armin Biere's And-Inverter Graphs as input format. The deadline for that special track will be in around mid-March 2007. Stay tuned for details.

May 31: The results of the special track are available.

Note that unlike the regular SAT competition, there was no certificates given by the solvers, despite all the machinery to check so-called "witnesses" is available in AIGER. As such, the results are provided "as is", without any warranty. Note also that the solver MiniCirc is reporting a strange answer in a few cases (?(Problem) cells). The solver has been fixed and additional results will be made available by the end of June.

Certified UNSAT special track

Allen Van Gelder made a call for such special track to the SAT 2007 competitors in order to assess his new Reverse Unit Propagation (RUP) proof format. He received 6 solvers this year against two solvers two years ago. The results are summarized in a poster to be presented during the SAT conference.

T-Shirt contest

We are lacking ideas for the T-shirts that will be given to the competitors. Please send us your proposal. We will try to organize a vote.

Organizing Committee

Organizers

Daniel Le Berre and Laurent Simon. Olivier Roussel has joined the team when it was decided to run the competition on his framework.

Judges

Submission/Participation

Benchmarks submission

Send an email to
organizers at satcompetition.org
with the description of the benchmarks an an URL where to download the benchmarks.

Solvers submission

Use that web page to register your SAT solver for the competition. Once registered, please send an email with your submission at
simon at lri.fr
or
leberre at cril.univ-artois.fr
. You might want to use one of our PGP public keys (laurent or daniel) for more security.