Termination Competition 2025 technical details

From Termination-Portal.org
Revision as of 08:16, 11 April 2025 by Ffrohn (talk | contribs) (Created page with "== Execution Environment == Starting from 2025, TermComp runs on the RWTH HPC cluster. Tools must be submitted as Docker images. During the competition, the following two co...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

Execution Environment

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. During the competition, the following two commands will be executed in your Docker container:

  • solver --name
  • solver --timeout=$timeout --category=$category $benchmark

So an executable named "solver" must be available in your container. The former command must print the name of your solver to stdout. The latter must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition. They will essentially be identical to the names of the corresponding TPDB directories.

Registration

To register, you need to create a pull request for this repository. More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt. The content of the line must be the identifier of your Docker image on Docker Hub, so that it can directly be passed to "docker pull".