Many tasks in early-stage mission design are still solved manually, as mission profiles tend to be small and subject to numerous constraints. However, the rise of the new space movement has significantly reduced mission costs and increased their frequency, creating a growing demand for automation in early design phases. This shift brings traditional computer science problems into focus, including route planning (e.g., traveling salesperson problems), reliability analysis (e.g., model counting), scheduling (e.g., graph coloring), and facility location (e.g., dominating set problems). As a result, automating mission design requires close collaboration between mission analysts and experts in automated reasoning. Yet, many of the modern tools developed in cost-optimal reasoning (e.g., maximum satisfiability), probabilistic reasoning (e.g., model counting), and constraint reasoning remain largely unfamiliar to the aerospace research community. Historically, this community has focused more on local optimization, e.g., computing optimal trajectories between celestial bodies, rather than on global optimization, like identifying optimal sequences across multiple targets. The goal of this Dagstuhl Seminar 25362 Optimization and Automated Reasoning for Designing Future Space Missions was to establish a bridge between these two communities to enable and activate future collaborations.

Computational Competitions

Early in the seminar, a shared passion quickly emerged as common ground between both communities: computational competitions. These are deeply rooted in the automated reasoning field, with flagship events such as the annual sat competition [10] and the maxsat evaluation [6]. Computer scientists showed strong interest in the efforts of mission analysts to establish similar competitions within the space domain, e.g., the bi-annual Global Trajectory Optimisation Competition (gtoc) [1] and ESA’s Space Optimization Competition (spoc) [8]. Conversely, aerospace researchers were keen to learn from the sat community’s long-standing experience in organizing such events, particularly in the development of standardized interfaces, file formats, validators, and benchmark sets.

Future Space Logistics

The vast majority of hypothetical space missions discussed during the seminar are from the space logistics domain. According to the AIAA Space Logistics Technical Committee, space logistics is “the theory and practice of driving space system design for operability and supportability, and of managing the flow of materiel, services, and information needed throughout a space system lifecycle” [3]. Yuri Shimane provided a detailed tutorial on the topic, highlighting in particular the rise of mega-constellations such as Starlink or OneWeb due to massively reduced launch costs. The design, construction, and maintenance of such structures involves various problems that can naturally be solved with tools from the constraint programming toolbox, which was presented to the participants of the seminar in a tutorial by Laurent Perron.

Routing Problems under Keplerian Dynamics

One of the actively discussed topics during the seminar was a variant of the traveling salesperson problem with moving targets, where the targets follow Keplerian dynamics [2, 4, 12]. This formulation naturally arises in applications such as in-space servicing [7], active debris removal [11], in-orbit refueling [13], and asteroid mining [5]. In contrast to these multi-rendezvous missions (the spacecraft must match position and velocity with the target), some versions only require flybys (matching only the position). A representative example discussed during the seminar was asteroid observation missions, for which Naoya Ozaki presented results on the design of flyby cycler trajectories – a promising approach for repeated asteroid visits. Participants explored how techniques like dynamic discretization discovery and branch-and-price could help to address the time-dependent nature of these problems. Additionally, discussions focused on the potential advantages of leveraging technologies such as max-sat, given the highly dynamic and multi-objective characteristics inherent to these routing problems.

Orbital Facility Location Problems

Another actively discussed topic during the seminar was facility location problems in orbital environments [14]. A classical example involves placing fuel depots in orbit to support sustainable in-orbit refueling missions, where a servicing spacecraft retrieves propellant from a depot and delivers it to a client. Participants explored how such problems can be discretized to make them amenable to automated reasoning techniques. It turned out that in some cases, these problems can be treated as static – for instance, when servicing times significantly exceed orbital periods (e.g., weeks or months versus hours). However, when such assumptions cannot be made, the problem becomes highly dynamic and time-dependent, requiring more sophisticated modeling and solution approaches similar to the routing problems.

Scheduling and Packing Problems

Additional relevant problem domains were proposed during the seminar, including satellite, constellation, and fleet scheduling problems [9], as well as 3D packing problems under physical constraints such as the system’s center of mass (e.g., for cargo vessel loading). While these challenges appear to be natural candidates for techniques from the constraint optimization community, they were not explored within the scope of this seminar due to lack of time.

Artificial Intelligence

The design and operation of in-space infrastructure involves constraints driven by the system’s time-varying properties (e.g., transfer costs), which are often non-linear. Two approaches discussed during the seminar were: (1) full discretization through pre-computation, which is conceptually straightforward but computationally expensive; and (2) the use of surrogate models, typically neural-network-based approximators, which can be integrated into optimization frameworks. In discussions with industry experts such as Robert Luce, participants explored how such integrations could be realized and what kinds of interfaces commercial solvers should support to facilitate this interaction.

Verification and Validation of Neural Networks

Although not a central theme of the seminar, attention was drawn to the stringent safety and reliability standards that neural networks must meet to be certified for on-board use. The automated reasoning community, with its expertise in formal verification, offers promising tools to certify neural network reliability automatically. As a result, future collaborations in this domain were initiated.

Seminar Agenda

Given that this Dagstuhl Seminar brought together two distinct communities, each day began with two tutorial talks: one focused on a computer science topic and the other on a space-related topic. On the first day, Harry Holt presented a tutorial on the fundamental building blocks of (multi-)rendezvous missions, while Matti Järvisalo introduced the concept of maximum satisfiability. The second day featured the tutorials discussed in the previous section, and on the final day, Abdin Adam provided a compelling bridge between optimization techniques and space logistics.

To foster collaboration and interaction, the seminar contained a problem session on the first day. Zhong Zhang introduced the Global Trajectory Optimization Competition, while Giacomo Acciarini and Manuel López-Ibáñez presented various formulations of the traveling salesperson problem under Keplerian dynamics. Following this session, participants engaged in breakout groups to explore the proposed challenges in more depth. These sessions focused on three main topics: (1) the use of max-sat and dynamic discretization discovery for solving time-dependent routing problems (chaired by Max Bannach), (2) the integration and support of non-linear constraints in modern solvers (chaired by Robert Luce), and (3) the computational aspects of a future mission to the Saturn system, including how a spacecraft might leverage its moons for gravitational braking (chaired by Laurent Beauregard).

Additionally, two sessions of inspiring talks were organized, giving young researchers the opportunity to share ideas from their current work and spark new discussions. Robyn Natherson spoke about challenges in low-thrust trajectory design, Chit Hong Yam addressed issues in sustainable lunar logistics, and Thorsten Ehlers presented on trajectory optimization at DLR. These space-focused insights were complemented by contributions from the computer science community: Anna Latour discussed reasoning under uncertainty, Alexandra Lassota analyzed structural properties of integer programs, and Stefan Szeider explored synergies between language models and constraint reasoning. As is tradition at Dagstuhl, some of the most engaging conversations took place during the Tuesday hike, which provided an informal yet productive setting for deeper interdisciplinary exchanges.

Future Work

As the primary objective of this seminar was to raise awareness of the tools and challenges developed within the computer science and space communities in recent years, much of the time was dedicated to presenting these resources rather than solving specific problems. A natural next step is a more solution-oriented workshop, focused on developing algorithms for concrete applications using techniques from the automated reasoning community. To facilitate this collaboration, participants expressed a clear desire for standardized interfaces, file formats, and benchmark sets.

Moreover, due to the limited duration of the seminar, many important topics could only be touched upon briefly or not at all. These include cargo packing, reliability analysis of constellations under uncertainty, sustainability aspects, applications to planetary defense, and satellite traffic management. These areas present promising directions for future interdisciplinary exploration.

References

1. Global Trajectory Optimisation Competition. https://sophia.estec.esa.int/gtoc_ portal/, 2024. Accessed: 11.04.2024.
2. Adam Abdin. Strategic Management of On-Orbit Servicing: Leveraging Operations Research Methods for Enhanced Mission Planning and Scheduling. In 18th International Conference on Space Operations, 2025.
3. AIAA Space Logistics Technical Committee. Definition of Space Logistics. https://www. aiaa-sltc.org/, 2024. Accessed: 06.09.2025.
4. Max Bannach, Giacomo Acciarini, and Dario Izzo. On the Keplerian TSP and VRP: Benchmarks and Encoding Techniques. In International Astronautical Congress, 2024.
5. A. Bellome, J.P. Sánchez, J.C. García Mateas, L. Felicetti, and S. Kemble. Modified Dynamic Programming for Asteroids Belt Exploration. Acta Astronautica, 215:142–155, 2024.
6. Jeremias Berg, Matti Järvisalo, Ruben Martins, Andreas Niskanen, and Tobias Paxian. MaxSAT Evaluation 2024: Solver and Benchmark Descriptions. 2024.
7. Alec J Cavaciuti, Joseph H Heying, and Joshua Davis. In-space Servicing, Assembly, and Manufacturing for the New Space Economy. Aerospace Center for Space Policy and Strategy, pages 2022–07, 2022.
8. ESA. SpOC. https://www.esa.int/Enabling_Support/Space_Engineering_ Technology/Help_make_an_orbital_megastructure_with_genetic_computation, 2024. Accessed: 08.04.2024.
9. Benedetta Ferrari, Jean-François Cordeau, Maxence Delorme, Manuel Iori, and Roberto Orosei. Satellite Scheduling Problems: A Survey of Applications in Earth and Outer Space Observation. Comput. Oper. Res., 173:106875, 2025.
10. Marijn JH Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Proceedings of SAT Competition 2024: Solver, Benchmark and Proof Checker Descriptions. 2024.
11. Dario Izzo, Ingmar Getzner, Daniel Hennes, and Luís Felismino Simões. Evolving Solutions to TSP Variants for Active Space Debris Removal. In Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2015, Madrid, Spain, July 11-15, 2015, pages 1207–1214, 2015.
12. Manuel López-Ibáñez, Francisco Chicano, and Rodrigo Gil-Merino. The Asteroid Routing Problem: A Benchmark for Expensive Black-Box Permutation Optimization. In International Conference on the Applications of Evolutionary Computation (Part of EvoStar), pages 124– 140. Springer, 2022.
13. Daria Malyh, Sergey Vaulin, Victor Fedorov, Ruslan Peshkov, and Mikhail Shalashov. A Brief Review on in-orbit Refueling Projects and Critical Techniques. Aerospace Systems, 5(2):185–196, 2022.
14. Yuri Shimane, Nicholas Gollins, and Koki Ho. Orbital Facility Location Problem for Satellite Constellation Servicing Depots. Journal of Spacecraft and Rockets, 61(3):808–825, 2024.

Creative Commons BY 4.0

Max Bannach, Johannes Klaus Fichte, Dario Izzo, and Inês Lynce