Automated Reasoning (AR) emerged as a field in the late 1960s. Its sub-areas cover different aspects of deductive reasoning as practiced in mathematics and formal logic, such as automated theorem proving (ATP) and propositional satisfiability (SAT), among others. Practical and theoretical research enabled ground-breaking success for vast applications of formal methods. At the core of this success are incredibly sophisticated and complex pieces of software, so-called solvers, which tackle specific problems in sub-areas of AR. Recurring solver competitions play a significant role in the practical success. They enable communities to showcase the current state-of-the-art, document practical advancements, identify challenges from research and industry, and push solver developers to not only aim for reliable and robust tools for a wide range of applications, but to improve their tools beyond current limitations. Competitions often set standards when it comes to scientific empirical evaluations, with significant impact on the research community and their empirical methods. Organizing a competition that yields meaningful results both for developers and users of the tools is challenging - a tremendous amount of work. And, since competitions serve as a driving force for new advancements in the area, certain decisions related to competition organization have a significant impact as they often establish standards for formats and experimental evaluations. Thus, competition organizers, competition participants, authors, and reviewers all face similar issues. A central goal of this seminar was to establish a bridge between various competition organizers to enable and activate future collaborations.

Participants

The Dagstuhl Seminar brought together organizers and stakeholders from major AR-related competitions, namely,

• the CADE ATP System Competition (CASC) [26, 25],
• the SAT Competition (SAT) [8, 9],
• the MaxSAT Evaluation [3, 2],
• the Satisfiability Modulo Theories Competition (SMT-COMP) [21, 30],
• the Competition on Software Verification (SV-COMP) [4, 5],
• the MiniZinc Challenge [27, 24, 23],
• the Model Counting Competition [13, 11, 12],
• the Pseudo-Boolean Competition (PB) [22],
• the Hardware Model Checking Competition (HWMCC) [7, 6],
• the Termination Competition (termComp) [15, 17],
• the Reactive Synthesis Competition (SYNTCOMP) [18, 19],
• the Answer Set Programming (ASP) Challenge [16, 10],
• the LP/CP programming contest (Prolog, ASP, SAT, CLP) [1],
• the Competition on Computational Models of Argumentation (ICCMA) [29, 20], and
• the Planning Competition (IPC) [14, 28].

Program, Focus, and Discussions

The program was structured around (i) competition survey talks and challenge collection; (ii) tutorials into benchmark selection, infrastructure, and evaluation; (iii) panels and discussion blocks to surface shared challenges; and (iv) outcomes to define concrete follow-ups. The first two days started with mapping the competition landscape. Numerous short talks presented individual competitions and challenges to establish a shared baseline across solver communities and evaluation traditions. Tutorial talks throughout the week focused on benchmark selection (dataset choice, portfolios, robustness/diversity, anomaly detection) and on evaluation infrastructure, including widely used standardized benchmarking execution and cloud-based benchmarking systems. Evaluation-focused talks presented long-term efforts on benchmark databases, longitudinal benchmark analysis and libraries, cloud infrastructure, and analytical approaches to competition results. A joint session with Research Meeting 25444 on Better Benchmarking Setups for Optimisation: Design, Curation and Long-Term Evolution provided insights into lessons from continuous optimization. Participants collected shared issues and targeted discussions to identify cross-cutting themes, for example, infrastructure, bias, repeatability, ranking methods, and interfaces. A dedicated panel on benchmarks and discussion sessions consolidated perspectives. Numerous discussion slots charted options for the “FLoC Olympics 2026”, participation/collaboration pathways, including spontaneous initiatives for contributing benchmark instances, and discussions on broader planning-competition perspectives.

Outcomes

Participants recognized that there is currently no universal methodology that guarantees robust, fair, and durable methods for competitions, benchmarking, and empirical evaluation in Automated Reasoning. Instead, participants converged on the view that good practice is necessarily context-dependent (competition goals, solver ecosystems, and community norms), requiring proper explanations and clear experimental design, while still benefiting from shared principles, shared resources, and a more precise articulation of trade-offs. Discussions emphasized, for example, the following aspects.

Benchmark sets should preferably be neutral, since this cannot always be guaranteed. Clearly highlighted pros and cons can be more valuable. Too much emphasis on the “best” result may limit development to what “progress” should look like, obstructing long-term research possibilities. Participants emphasized that a competition should include a wellargued benchmark selection, reduce overfitting to benchmark sets, enable representativeness beyond annual competition cycles (by reusing settings in paper submissions), facilitate new trends, and explore new applications.

Participants agreed that competitions are not purely technical; they serve as a tool for building communities. A joint infrastructure that simplifies coordination, research efforts, and stable evaluation would be highly appreciated. Participants argued that longterm discussions on standards for empirical methodology would be beneficial. Moreover, competition organizers should actively balance between a narrow leaderboard focusing on winners and detailed scientific reporting, including clear documentation of configurations, available resources, and constraints, different (possibly opposing) measures, and ranking approaches that reflect different needs. Participants favored explicit decisions that are transparent and understandable.

Moreover, practical considerations to simplify competition organization and enable easy, replicable evaluations, such as shared tooling, access to compute infrastructure (public HPC clusters and cloud resources), replication and artifact evaluation, and software quality, were discussed. What comes to infrastructure, developers and competition organizers often maintain their own infrastructure, as modern HPC research environments currently do not provide stable, reliable, and replicable execution for evaluating AR solvers. Therefore, the need to engage with HPC operators to establish a standard setup and run configurations on HPC environments was identified. In this context, the seminar discussed the future of StarExec, including perspectives on StarExec in the Cloud and the sustainability challenges of centralized evaluation platforms (governance, funding, maintenance, and risk mitigation).

Several coordination endeavors and community resources emerged spontaneously during the week. These included:

• an initiative on contributing benchmark instances (mysolvertimesout.org) aiming at lowering submission barriers and improving crediting practices (Daniel Le Berre);
• joining competitions focusing on onboarding and participation pathways (Laurent Simon);
• controversial evaluation statements and benchmarking (Ciran McCreesh)
• discussion of collaboration models to foster cross-competition exchange of tooling, benchmarks, and evaluation know-how (Marie Anastacio);
• distribution and dissemination of competition reports (Sophie Tourret);
• designing variable but meaningful complementing rankings (Oliver Roussel);
• a joint website on AR competitions as a centralized entry point for competition information, best-practice guidance, and shared resources (Geoff Sutcliffe); and
• an imitative on requirements to establish a European competition infrastructure (Ciran McCreesh).

The participants agreed during the closing session to follow-up in particular on

• mechanisms for benchmark distribution and crediting;
• exploring publication venues and journal tracks for durable competition and evaluation outputs
• pursuing funding and coordination initiatives to support shared infrastructure;
• and planning future workshops, FLoC-related events, and an ERC Cost Action to maintain momentum and enable frequent meetings; and
• comprehensive survey paper synthesizing methodological lessons across competition ecosystems.

References

1. Mario Alviano. Lp/cp programming contest. https://lpcp-contest.github.io/, 2025.
2. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian. MaxSAT evaluation 2024 : Solver and benchmark descriptions. Technical report, Helsinki University Library, 2024.
3. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian. Maxsat evaluations: Evaluating the state of the art in maximum satisfiability solver technology. https://maxsat-evaluations.github.io/, 2025.
4. Dirk Beyer. Competition on software verification (sv-comp). https://sv-comp.sosy-lab. org/, 2025.
5. Dirk Beyer and Jan Strejček. Improvements in software verification and witness validation: SV-COMP 2025. In Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’25), pages 151–186, Hamilton, ON, Canada, 2025. Springer-Verlag.
6. Armin Biere, Nils Froleyks, and Mathias Preiner. Hardware model checking competition 2024. In Proceedings of the 2024 Formal Methods in Computer-Aided Design (FMCAD’24), pages 1–1, 2024.
7. Armin Biere, Nils Froleyks, and Mathias Preiner. Hardware model checking competition. https://hwmcc.github.io/, 2025.
8. Cayden Codel, Katalin Fazekas, Marijn Heule, and Ashlin Iser. SAT competition 2025. https://satcompetition.github.io/2025/index.html, 2025.
9. Cayden Codel, Katalin Fazekas, Marijn J. H. Heule, and Markus Iser. Proceedings of sat competition 2025 : Solver and benchmark descriptions. Technical report, TU Wien, 2025.
10. Carmine Dodaro, Christoph Redl, and Peter Schüller. The answer set programming challenge 2019. https://sites.google.com/view/aspcomp2019/, 2019.
11. Johannes K. Fichte and Markus Hecher. The model counting competitions 2021-2023. https://arxiv.org/abs/2504.13842, 2025.
12. Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. ACM J. Exp. Algorithmics, 26, oct 2021.
13. Johannes K. Fichte, Markus Hecher, and Arijit Shaw. Model counting competition. https: //mccompetition.org/, 2025.
14. Daniel Fišer, Florian Pommerening, Jendrik Seipp, Javier Segovia-Aguas, Ayal Taitler, Scott Sanner, Joan Espasa Arxer, Enrico Scala, Ron Alford, Dominik Schreiber, and Gregor Behnke. International planning competition 2023. https://ipc2023.github.io/, 2023.
15. Florian Frohn, Jürgen Giesl, Georg Moser, Étienne Payet, Akihisa Yamada, and Dieter Hofbauer. Termination competition. https://termination-portal.org/wiki/Termination_ Competition, 2025.
16. Martin Gebser, Marco Maratea, and Francesco Ricca. The seventh answer set programming competition: Design and results. Theory and Practice of Logic Programming, 20(2):176–204, 2020.
17. Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. The termination and complexity competition. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 156–166, Cham, 2019. Springer International Publishing.
18. Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, and Adam Walker. The reactive synthesis competition (SYNTCOMP): 2018-2021. https://arxiv.org/abs/2206.00251, 2024.
19. Swen Jacobs, Guillermo A. Pérez, and Philipp Schlehuber-Caissier. The reactive synthesis competition. https://www.syntcomp.org/, 2024.
20. Matti Järvisalo, Tuomo Lehtonen, and Andreas Niskanen. ICCMA 2023: 5th international competition on computational models of argumentation. Artificial Intelligence, 342:104311, 2025.
21. Martin Jonáš, François Bobot, David Déharbe, and Dominik Winterer. SMT-COMP 2025. https://smt-comp.github.io/2025/, 2025.
22. Olivier Roussel. Pseudo-Boolean competition 2025. https://www.cril.univ-artois.fr/ PB25/, 2025.
23. Peter J. Stuckey, Ralph Becket, and Julien Fischer. Philosophy of the minizinc challenge. Constraints, 15(3):307–316, July 2010.
24. Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. The MiniZinc challenge 2008–2013. AI Magazine, 35(2):55–60, Jun. 2014.
25. G. Sutcliffe. The 12th IJCAR Automated Theorem Proving System Competition - CASC-J12. AI Communications, 38(1):3–20, 2025.
26. Geoff Sutcliffe. The CADE ATP system competition. https://tptp.org/CASC/, 2025.
27. Guido Tack, Peter J. Stuckey, Jason Nguyen, Jip J. Dekker, Kevin Leo, and Maria Garcia de la Banda. The MiniZinc challenge. https://www.minizinc.org/challenge/, 2025.
28. Ayal Taitler, Ron Alford, Joan Espasa, Gregor Behnke, Daniel Fišer, Michael Gimelfarb, Florian Pommerening, Scott Sanner, Enrico Scala, Dominik Schreiber, Javier Segovia- Aguas, and Jendrik Seipp. The 2023 International Planning Competition. AI Magazine, 45(2):280–296, 2024.
29. Matthias Thimm, Johannes P. Wallner, Iosif Apostolakis, and Andrei Popescu. Iccma international competition on computational models of argumentation. https: //argumentationcompetition.org/, 2025.
30. Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, and Giles Reger. The SMT competition 2015-2018. J. Satisf. Boolean Model. Comput., 11(1):221– 259, 2019.

Creative Commons BY 4.0

Johannes Klaus Fichte, Matti Järvisalo, Aina Niemetz, and Guido Tack