Optimization and Automated Reasoning for Designing Future Space Missions

In this talk I will show some optimization problems that were solved in the institute for air transport at DLR. While the main focus of our institute is on the aerospace side, it is highly relevant for us to use the right optimization algorithms, e.g. in evaluating operational concepts for new aircraft.

The objective of this talk was to introduce the field of multi-rendezvous/encounter missions in astrodynamics to a non-expert audience. After covering some of the building blocks in orbital mechanics, such as propagation, orbital elements and reference frames, we discussed the constraints imposed by different encounters and propulsion systems. Lambert’s problem was introduced for solving two-impulse transfers, and direct encodings were presented for deep-space manoeuvres, multi-impulse trajectories, low-thrust trajectories, and gravity assists. Finally, space-specific methods for solving the outer combinatorial part were presented, including pruning approaches and approximating the cost function.

We provide a high-level overview of maximum satisfiability (MaxSAT), covering basics on encoding problems as MaxSAT, the algorithmic approaches implemented in modern MaxSAT solvers, and pointers to further recent developments in MaxSAT solving.

This talk will give you a little snippet on the TCS side of integer programs: What are some of us actually doing? What are our challenges? What are our accomplishments?

Real-world problems typically contain a lot of structure that we can exploit to solve them fast in practice. For example: in many problems that reason about uncertainty, we can capture the problem in a decision diagram, and use that DD’s structure to not only prune the search space of strategies, but also efficiently integrate over scenarios to evaluate the quality of a strategy.

For a satellite constellation for Earth observation design problem, we recently showed that we can improve upon the state of the art by framing the original problem as a computationally harder problem, but with an exponentially smaller encoding. Thanks to the speed of solvers for high-complexity problems in practice, we can make orders of magnitude improvement in the size of the problems that we can solve. This is all thanks to smartly leveraging the structure of the problem. We are currently working on how to apply this trick to different (and in some cases more realistic) variants of the problem.

The next step is to increase our capabilities of optimisation under uncertainty by applying structure-based approaches to sensitivity analysis. The classical approach to identifying how sensitive your decisions are to the exact value of certain input parameters relies on simulations. These are computationally expensive, might miss important sensitivities due to their probabilistic nature (and hence provide statistical guarantees at best), and can typically only handle one parameter at a time.

I propose a new method that is based on the logical structure of the problem, instead. Advantages include that you get the interaction of variables for free and that you get access to formal verification technology.

Many real-world scenarios involve solving bi-level optimization problems in which there is an outer discrete optimization problem, and an inner problem involving expensive or black-box computation. This arises in space-time dependent variants of the Traveling Salesman Problem, such as when planning space missions that visit multiple astronomical objects. Planning these missions presents significant challenges due to the constant relative motion of the objects involved. There is an outer combinatorial problem of finding the optimal order to visit the objects and an inner optimization problem that requires finding the optimal departure time and trajectory to travel between each pair of objects. The constant motion of the objects complicates the inner problem, making it computationally expensive. This paper introduces a novel framework utilizing decision diagrams (DDs) and a DD-based branch-and-bound technique, Peel-and-Bound, to achieve exact solutions for such bi-level optimization problems, assuming sufficient inner problem optimizer quality. The framework leverages problem-specific knowledge to expedite search processes and minimize the number of expensive evaluations required. As a case study, we apply this framework to the Asteroid Routing Problem (ARP), a benchmark problem in global trajectory optimization. Experimental results demonstrate the framework’s scalability and ability to generate robust heuristic solutions for ARP instances. Many of these solutions are exact, contingent on the assumed quality of the inner problem’s optimizer.

Inspired by the recent 11th Global Trajectory Optimisation Competition, this paper presents the asteroid routing problem (ARP) as a realistic benchmark of algorithms for expensive bound-constrained black-box optimization in permutation space. Given a set of asteroids’ orbits and a departure epoch, the goal of the ARP is to find the optimal sequence for visiting the asteroids, starting from Earth’s orbit, in order to minimize both the cost, measured as the sum of the magnitude of velocity changes required to complete the trip, and the time, measured as the time elapsed from the departure epoch until visiting the last asteroid. We provide open-source code for generating instances of arbitrary sizes and evaluating solutions to the problem. As a preliminary analysis, we compare the results of two methods for expensive black-box optimization in permutation spaces, namely, Combinatorial Efficient Global Optimization (CEGO), a Bayesian optimizer based on Gaussian processes, and Unbalanced Mallows Model (UMM), an estimation-of-distribution algorithm based on probabilistic Mallows models. We investigate the best permutation representation for each algorithm, either rank-based or order-based. Moreover, we analyze the effect of providing a good initial solution, generated by a greedy nearest neighbor heuristic, on the performance of the algorithms. The results suggest directions for improvements in the algorithms being compared.

Low-thrust propulsion enables deep space exploration at a fraction of the fuel cost. However, these systems require significantly longer thrust arcs compared to those with conventional chemical propulsion systems. Burn durations can span days, weeks, or even months. The extended thrusting periods of low-thrust systems increase the likelihood that a spacecraft anomaly will overlap with a planned burn, causing the spacecraft to deviate from its nominal trajectory. This is referred to as the missed thrust problem. Without robust trajectory design, losses from missed thrust jeopardize mission objectives, especially when flight paths include encounters with celestial bodies.

My doctoral research focuses on how to leverage reachability results to design robust transfers accounting for missed thrust. Reachability results can be formulated in two ways, forwards and backwards. My work specifically utilizes backwards reachable sets, or controllable sets. Controllable sets characterize the region of full-state initial conditions which can reach a target within a finite time. Typically, designing for missed thrust involves an iterative process where candidate transfers are tested for robustness and updated until design constraints are satisfied. However, applying reachability theory to study the missed thrust problem would allow the entire solution space to be studied at once, avoiding this tedious process. I will discuss the use of a reachability framework to compute a robustness metric, the missed thrust recovery margin (MTRM). The MTRM is the amount of time a spacecraft can coast away from a nominal trajectory before the target becomes inaccessible. By sampling points on a controllable set, we map the robustness of regions in phase-space visualized with a heatmap. The goal is to leverage this reachability information to design flight paths through regions that have inherently high MTRM.

Challenges associated with this research include:

• $\mathrm{■}$

  Reachability computation – efficiency, accuracy, and sampling of full-state sets

• $\mathrm{■}$

  Representing reachability point-cloud data in a usable form – especially for non-convex reachability results

• $\mathrm{■}$

  Testing inside/outside of a controllable or reachable set

• $\mathrm{■}$

  Visualization of 4D or 6D full-state reachability data

Due to the missed thrust problem, robust design strategies are integral for promoting mission assurance for flight projects employing low-thrust systems. Our novel reachability-informed trajectory design approach has the potential to change how to view the missed thrust problem.

Asteroid exploration has been attracting more attention in recent years. Nevertheless, we have just visited tens of asteroids while we have discovered more than one million bodies. As our current observation and knowledge should be biased, it is essential to explore multiple asteroids directly to better understand the remains of planetary building materials. One of the mission design solutions is utilizing asteroid flyby cycler trajectories with multiple Earth gravity assists.

An asteroid flyby cycler trajectory design problem is a subclass of global trajectory optimization problems with multiple flybys, involving a trajectory optimization problem for a given flyby sequence and a combinatorial optimization problem to decide the sequence of the flybys. As the number of flyby bodies grows, the computation time of this optimization problem expands maliciously.

This paper presents a new method to design asteroid flyby cycler trajectories utilizing a surrogate model constructed by deep neural networks approximating trajectory optimization results. Since one of the bottlenecks of machine learning approaches is the computation time to generate massive trajectory databases, we propose an efficient database generation strategy by introducing pseudo-asteroids satisfying the Karush-Kuhn-Tucker conditions.

The numerical result applied to JAXA’s DESTINY+mission shows that the proposed method is practically applicable to space mission design and can significantly reduce the computational time for searching asteroid flyby sequences.

We present OR-Tools, the suite of Operations Research tools build at Google and exported to github.

We give a more detailed overview of the CP-SAT solver, an award winning hybrid solver using MaxSAT, CP, MIP, and Meta-Heuristics techniques.

Space Logistics, which studies the design, operation, and maintenance of in-space infrastructures, requires reconciling combinatorial aspects of the problem with the underlying orbital mechanics. In this light, we begin by exploring the history of Space Logistics, from the Space Shuttle era to the present decade. We then explore two space-based applications of the facility location problem (FLP) in closer detail. The first example is for the placement of in-orbit servicing depots and their allocation to GNSS constellations. In this example, due to the periodicity of the depots’ candidate orbits and the difference in time scale between the servicing allocation and the orbital periods, we assume a time-independent formulation. In contrast, the second example studying the placement and sensor-tasking of a cislunar space situational awareness constellation is time-dependent, requiring a time-expanded FLP. To tackle the problem size growth with the inclusion of discretized time, we develop a Lagrangian relaxation scheme that features an analytical relaxed solution, customized heuristics for the feasible solution, and that scales linearly with the number of time-steps. We conclude by looking towards the future – areas such as coordinated space traffic management, data logistics, and planetary defense, present exciting research avenues with real-life implications for the space economy.

Integrating Large Language Models (LLMs) with traditional solving techniques creates new synergies in automated reasoning. This talk explores both (i) how LLMs can enhance SAT and constraint solving through structural analysis and search guidance and (ii) how formal reasoning can help LLMs tackle hard reasoning and optimization problems. We will present case studies exploring the practical advances and future potential of combining neural and symbolic approaches in computational reasoning.

Future lunar exploration will depend on building a sustainable logistics framework that connects data, mission components, and technologies into a coherent system. Yet critical uncertainties remain: how much and what type of lunar data is sufficient for planning? How should interdependent mission elements – landers, habitats, power systems, and resource utilization – be prioritized? And who will coordinate logistics standards across multiple players? This talk highlights the challenges and trade-offs of sustainable lunar logistics, emphasizing the tension between incomplete knowledge and long-term commitments. Rather than presenting solutions, it frames the open questions that must be addressed before a truly sustainable lunar supply chain can emerge.

The 12th Global Trajectory Optimization Competition (GTOC12) focused on the challenge of asteroid mining. Teams were tasked with designing trajectories for multiple mining spacecraft departing from Earth, visiting asteroids, extracting resources, and returning the mined material to Earth. The primary objective was to maximize the total returned mass of minerals. The problem combined optimal control and combinatorial optimization. From the control perspective, spacecraft needed to rendezvous with asteroids, requiring precise position and velocity matching under a two-body low-thrust dynamical model. From the combinatorial side, teams had to decide how many spacecraft to use, which asteroids to target, in what order, and at what times. The competition highlighted the intersection of astrodynamics, optimization, and mission design. Ultimately, innovative strategies enabled the top teams to achieve impressive results. The next competition, GTOC13, will be hosted by NASA JPL.