SMT-Exec: Results Help

General help: Rows in tables are clickable to navigate between different views of the results; hover the cursor over the row to get a description of the view you'll be taken to. Most column headings are clickable to change sort order. Informational notices and links to other result views are available toward the top of many pages.

Jobs: This system is job-driven; the competition run is merely one job. Multiple jobs can be selected for focus at the top right of results pages; doing so merges the results of the selected jobs.

Legend for this page:

job complete

job incomplete

results

no results yet

refreshed with new results

currently running

running hors concours

Results Help

The results system for SMT-Exec is intended to be highly dynamic and answer many questions about solver performance.

Feedback

Please give us feedback on this system's design and implementation! We hope it will be useful to the SMT community, and we appreciate hearing your ideas for improving both the back-end infrastructure and the front-end results views.

Infrastructure

SMT-Exec is run on a cluster of nine execution hosts (specifications here). At the start of the competition, benchmark scripts are queued for execution. Each script runs a single benchmark on all competing solvers. This has the consequence that a single execution host runs every solver on a benchmark, and does so as a single block. This is intended to ensure that benchmark results are fair; if a particular execution host is relatively slower on average, for any reason, each solver shares the same hardship and the results are still comparable.

The solvers on a particular benchmark are run in pseudorandom order. The divisions are run in order; only when all remaining jobs of a particular division are executing will the next division start (on another host, of course).

Legend

A color-coding legend is available at the bottom left corner of most results pages (the blue question mark box). Clicking it reveals the legend.

Navigating

Clicking rows of a result table takes you to another, related view. Hover the mouse over a row to see a description of the linked view.

Sorting Results

Results tables can be sorted on any column (with the exception of the summary view). Click the column header to sort by that column. Click it again to sort in the opposite direction.

Searching Results

In the solver results view (listing benchmarks), you can search for a specific benchmark or family of benchmarks by clicking the [Search] button, typing a search term into the text box, and pressing ENTER. To reset the view and see all results again, click [Reset].

Job Model

This view is subject to the job model, as other results pages are. Ensure that the SMT-Exec job “smtcomp2007” is the sole job selected (at the top right of each page) if you want to view competition results. If you want to compare two jobs (for example, to see improvement of solvers over last year's solvers), select a second job to view in conjuction with the SMT-Exec results.

Refreshing the View

At the bottom of many results pages is found a refresh control panel. Click a refresh time and the results will be refreshed at that interval. If the server cannot be reached, the attempt is repeated every minute.

Setting a Time Zone Preference

Your time zone preference can be changed by clicking on the current time zone setting at the top left of most pages. All result time stamps are converted to this time zone for your convenience; the time displayed at the bottom of every page is the page service time stamp, and is displayed in the server's time zone (currently Central Daylight Time in the US).

Web Standards

We attempt to adhere closely to web standards in the results system. In a few cases we tailor content for web browsers that don't support web standards. This site is best viewed with recent versions of Konqueror, Firefox, Opera, or Internet Explorer.