"The experimentation web site around the satisfiability problem"

The purpose of the competition is to identify new challenging benchmarks and to promote new SAT solvers as well as to compare them with state-of-the-art ones. For more information, please visit the official competition web page, located at www.satlive.org/SATCompetition/2003.

Quick overview

The SAT-Ex site attempts to group experimentations around the fundamental SAT problem. Its aim is to gather experiments, providing executions traces of provers on all benchmarks. It also provides some study on benchmarks and on programs performances. More information about the SatEx can be found here.

Today, the SAT database can be summarized with the following numbers:

• Total CPU time of the SAT executions databases: 529 days, 17 hours, 53 minutes and 20 seconds ( of a PII-400 Under Linux, when counting Resigned executions as 10000s).
• Number of Benchmarks: 1303, grouped in the following families (avg-checker, beijing, bmc, des-encryption, dimacs, formal-verification, miters, morphed, paderborn, quasigroup, ucsc).
• Number of SAT-provers: 23 (asat, calcres, csat, dr, eqsatz, heerhugo, modoc, modoc-2.0, nsat, ntab, ntab_back, ntab_back2, posit, relsat, relsat-200, sat-grasp, sato, sato-3.2.1, satz, satz-213, satz-215, zchaff, zres).
• Number of executions: 32610

• Aims and ideas that justify this site, with some papers dealing with the topic. Why doing such a site?
• Frequently Asked Questions and How-To, thus answering several very natural questions about how to navigate in the site, about its construction, or about the experimental conditions and how to gather some results.
• View synthesis of results of:
  • Any combination of Solver/Benchmark , where you can choose exactly what solvers and what families of benchmarks should appear in the summary.
  • One of the predefined summaries of results, where you choose only a family of solvers and some origins of benchmarks. Summary tables are cached for speed purpose.
• Download all cpu-time results in CSV-format (gzipped, about 125Kb);
• View challenging benchmarks.
• List of reported bugs .
• The History, with the (too long) list of things to do;
• The traditional Links section.

This rank list is established over all benchmarks of SatEx where results are availables, but this ranking should be taken with care. It is only indicative and it can give a bad or a wrong idea of some program performances, especially for those which have been designed for only some specific benchmarks. A special (and much more complete) TOP page is Here.

The SAT Live! web site has a forum dedicated to SatEx. Our aim is to fill-in informations about solvers and benchmarks in SatEx, as well as comments on results. Please visit the Sat Live! forum on SatEx to help us.

Three very usefull SAT related links

• [NEW] The Journal on Satisfiability, Boolean Modeling and Computation. It's a peer reviewed Journal guaranteeing fast publication, and in which I'm involved.
• The SATLIB web site. This site is simply the reference for benchmarks and solver releases.
• The SAT Live! web site. Maintained by Daniel Le Berre, this site is an "Up-to-date database on links for SAT". It contains links to papers (often before conference proceedings), to very recent programs and all other stuff that members can submit. You can also subscribe to a very usefull mailing list about that topic and you are invited to take part of a discussion forum about SAT.

© 2000-2001 Laurent Simon

Scripts last modified on 06-02-2003 File generated on 3-08-2005