A solver can be withdrawn from ICCMA 2025 only before the deadline for the submission of the final versions. After this deadline no further changes or withdrawals of the solvers are possible.
The evaluation organizers reserve the right to restrict the number of solver submissions originating from the same author(s) based on computation resource limitations.
A solver will not be immediately disqualified if it displays a wrong solution during the execution of the evaluation. The organizers will aim to provide all participants a fair chance of submitting bug fixes to their solvers in a timely manner based on feedback on wrong results. However, the organizers reserve the right to limit the number of resubmissions of a buggy solver based on resource limitations.
If the solver's bug cannot be resolved, the submitters will still have the option of having the solver's correct results tabulated and reported in the table of results. However, the results will be marked to indicate that the solver also generated some incorrect results.
In all tracks except for the No-Limits Track, solvers must use only a single core of the processor on the computing node it is run on, and solvers making use of multiple cores will be disqualified. This limitation does not concern the No-Limits Track, where parallel computations are allowed.
Portfolio solvers, which combine several existing argumentation solvers are not allowed to participate in the competition. This limitation does not concern the No-Limits Track, where portfolios are allowed.
The organizers may move a solver from the Main Track to the No-Limits Track if the solver is deemed to violate these conditions.
If a solver takes part in the Fixed-SAT-Solver comparison, the solver must implement the IPASIR interface with incremental SAT solvers. The compilation must be described sufficiently so that the organizers can compile the solver with a specific SAT solver implementing the IPASIR interface. For instance, when using makefiles, a clear and dedicated must be present for exchanging the IPASIR SAT solver. For examples, we provide a simple example, and also see the IPASIR repository. The solver will then interact with a SAT solver with the IPASIR interface and be compiled with a specific SAT solver for ICCMA 2025. Taking part in the Fixed-SAT-Solver comparison excludes then use of any other search engine similar to SAT solvers (like answer set programming). Usage of a SAT solver is limited to usage of the IPASIR interface (i.e., the solver may only use the interface to delegate computationally intenstive computations). The organizers reserve the right to remove submissions to the Fixed-SAT-Solver comparison based on a case-by-case analysis.
For all tracks apart from No-Limits, solver source code originating from the authors (including modifications to third-party source code such as SAT solvers as part of a solver) must be submitted together with a corresponding solver binary. The source code package of each participating solver will be made available at the time when the results of ICCMA 2025 are presented. We plan to present the results at the KR 2025 conference. In case bug fixes are submitted during the evaluation (i.e., if requested by the evaluation organizers), the bug-fixed source package must also be submitted together with a bug-fixed solver binary. A solver is allowed to use external binaries or unmodified third-party libraries. However, if the library is non-standard (i.e., not STL, Boost, etc.) its identity and usage in the solver should be clearly specified in the solver description.
Each entrant to ICCMA 2025 must include a short (at least 1, at most 2 pages) description of the system. This should include a list of all authors of the system and their present institutional affiliations. It should also provide details of any non-standard algorithmic techniques (e.g., heuristics, simplification/learning techniques, etc.) and data structures, as well as references to relevant literature (be they by the authors themselves or by others). The system description must be formatted in a style that will be announced at a later stage, and submitted as PDF. The system descriptions will be posted on the ICCMA 2025 website. Furthermore, given that the quality and number of system descriptions is high enough, the organizers are considering publishing the collection of system descriptions as a report.
The organizers are allowed to enter their own solvers into the evaluation. To avoid providing them with advantage over other participants, details of the benchmark selection process will be made public after the submission deadline and it will ensured that no individual organizers nor subsets of the organizers can impose that a specific seed is used for the randomized process applied for benchmark selection. Furthermore, any solver originating from the authors will be published online in open source at the submission deadline.
Building. The submitted source code of the solver must include a README with detailed instructions on how to compile and invoke the solver. For the Dynamic Track, the README must include instructions on building the solver in order to be called via the generic Python API (e.g., how to build a dynamic library beforehand). All builds must be successful on a standard Linux distribution with x86-64 processors. Note that if the solver makes use of non-standard libraries or external binaries, they must be included within the submission.
Input format. In the Main Track, the No-Limits Track, the Dynamic Track, and the Heuristics Track, the following AF input file format is used. The arguments of an AF with n arguments are indexed consecutively with positive integers from 1 to n. The first line of the input file is the unique "p-line" of the form
p af <n>where <n> is the number of arguments n, ending with the newline character. An attack a → b, where a has index i and b has index j, is expressed as the line
i jending with the newline character. In addition to the p-line and lines expressing attacks, lines starting with the '#' character are allowed. These lines are interpreted as comment lines unrelated to the syntax of the input AF, and end with the newline character. No other lines are allowed.
Example. The AF with five arguments a,b,c,d,e and attacks a → b, b → d, d → e, e → d, e → e is specified as follows, assuming the indexing a=1, b=2, c=3, d=4, e=5.
p af 5 # this is a comment 1 2 2 4 4 5 5 4 5 5
In the Assumption-Based Argumentation track, the following ABA input file format is used. The atoms of an ABA framework with n atoms are indexed consecutively with positive integers from 1 to n. The first line of the input file is of a the unique "p-line" of the form
p aba <n>where <n> is the number of atoms n, ending with the newline character. Assumptions, rules and contraries are specified on individual lines. A line starting with 'a', followed by an index between 1 and n, specifies that the atom with the index is an assumption. A line starting with 'c', followed by two space-separated indices between 1 and n, specified that the atom corresponding to the second index is a contrary of the atom corresponding to the first index. A line starting with 'r' followed by a space-separated list of indices between 1 and n specify a rule whose head is the atom corresponding to the first index in the list and whose body consists of the atoms corresponding to the subsequent indices in the list. Each line starting with 'a', 'c' or 'r' ends with the newline character. In addition to the p-line and lines starting with 'a', 'c' or 'r', lines starting with the '#' character are allowed. These lines are interpreted as comment lines unrelated to the syntax of the input ABA framework, and end with the newline character. No other lines are allowed.
Example. The ABA framework with rules (p ← q,a), (q ←), (r ← b,c), assumptions a,b,c, and contraries a̅ = r, b̅ = s, c̅ = t is specified as follows, assuming the atom-indexing a=1, b=2, c=3, p=4, q=5, r=6, s=7, t=8.
p aba 8 # this is a comment a 1 a 2 a 3 c 1 6 c 2 7 c 3 8 r 4 5 1 r 5 r 6 2 3
Output format. In all tracks except for the Dynamic Track, the solvers must print the result into standard output exactly in the format specified below.
YES w 1 2 5Otherwise, the solver output must be:
NO
YESOtherwise, the solver output must be:
NO
Update: for the specific case of preferred semantics, the witness can also consist of an admissible set attacking the queried argument.
For example, if the solver finds the σ-extension 1,4 not containing the query argument 2, the solver output must be the following:NO w 1 4Otherwise, the solver output must be:
YES
YESOtherwise, the solver output must be:
NO
w 3 7Otherwise, the solver output must be:
NO
Note that in the Dynamic Track, where the solver is invoked via an API, the solver may not print anything to standard output. The benchmark application calling the solver will perform the necessary printing.
Usage. In all tracks except for the Dynamic Track, the solvers must be executable from a command line with the following behavior.
user$ solver MySolver v1.0 John Doe, john.doe@example.com
user$ solver --problems [DC-CO,DS-CO,SE-CO,DS-PR,SE-PR]
solver -p <task> -f <file> [-a <query>]The arguments -p <task> and -f <file> are mandatory for all tasks. Here <task> is a computational problem supported by the solver, and <file> is a valid file as described above. The -a <query> argument is mandatory only for the DC and DS tasks. Here <query> is a positive integer less than or equal to <n> (i.e., the number of arguments in the AF tracks and the number of atoms in the ABA tracks) as specified in the p-line. Example (Main or No-Limits Track):
user$ solver -p DC-CO -f instance_file -a 2 YES w 2 3Example (Heuristics and ABA Tracks):
user$ solver -p DC-CO -f instance_file -a 2 YES
Note that in the Dynamic Track, the solver is invoked via IPAFAIR, an incremental API for AF solvers. The API contains the specifications for the input arguments and return values of all functions.