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!
- 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
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 contestWe 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.
OrganizersDaniel Le Berre and Laurent Simon. Olivier Roussel has joined the team when it was decided to run the competition on his framework.
Benchmarks submissionSend an email to
organizers at satcompetition.orgwith the description of the benchmarks an an URL where to download the benchmarks.
Solvers submissionUse that web page to register your SAT solver for the competition. Once registered, please send an email with your submission at
simon at lri.fror
leberre at cril.univ-artois.fr. You might want to use one of our PGP public keys (laurent or daniel) for more security.