
"The experimentation web site around the satisfiability problem"
| Preliminary warnings:
Just recall that this site is provided as is, and if I try to check
all results, as they are automatically generated, I currently make no
warranty about them. They are all stemming from my own experience and
running sessions. But, the picture is not so dark, and, as far as I
know, no bugs are around there. Feel free to mail me remarks or suggestions about
results or bugs revealing.
| |
"I want you" for SatEx Operation
|
| 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. |
|
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:
- 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.
Program |
Time Used |
Slow Ratio |
#Solved |
#Tested |
zchaff |
2 days, 22 h. 52 m. 29 s. |
1.00 |
1280 |
1303 |
relsat-200 |
5 days, 19 h. 20 m. 50 s. |
1.97 |
1260 |
1303 |
relsat |
7 days, 9 h. 33 m. 20 s. |
2.51 |
1243 |
1303 |
sato |
8 days, 9 h. 35 m. 12 s. |
2.84 |
1241 |
1303 |
satz-215 |
8 days, 22 h. 48 m. 56 s. |
3.03 |
1237 |
1303 |
eqsatz |
9 days, 0 h. 6 m. 8 s. |
3.05 |
1237 |
1303 |
satz-213 |
9 days, 15 h. 18 m. 16 s. |
3.26 |
1232 |
1303 |
sato-3.2.1 |
10 days, 9 h. 52 m. 52 s. |
3.53 |
1221 |
1303 |
satz |
10 days, 12 h. 59 m. 23 s. |
3.57 |
1211 |
1303 |
modoc |
11 days, 2 h. 27 m. 40 s. |
3.76 |
1217 |
1303 |
Total cpu time in the table: 84 days, 4 h. 55 m. 10 s.
Two very usefull SAT related links
|
- 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.
This main page has been accessed 2408 times since the 31st of March, 2000.
Total number of Hits for the Satex during the same period: 93713
© 2000-2001 Laurent Simon |
Scripts last modified on 01-07-2001 File generated on 6-09-2001 |
  |