Abstract
Inter-satellite links are gaining prominence due to their capacity to provide low latency, enhanced data rates, improved security, and reduced interference compared to satellite-ground-satellite connections. Notably, they are slated for implementation in the second generation of the European Space Agency's (ESA) Galileo constellation—Europe's proprietary global navigation satellite system. Furthermore, inter-satellite links have already been successfully deployed in the existing generation of Starlink satellites. At a given epoch, the arrangement of satellites defines a network of communication links. These links may not always be present, for instance when satellites are out of range, or they might exhibit failure with some probability due to factors like geography, weather conditions, hardware malfunctions, or positioning errors. Ensuring a consistent quality of service necessitates the establishment of a reliable network at all times. This entails maintaining a high probability of having a functional path between any pair of satellites or ground stations. Reliable constellations with inter-satellite communication are particularly important for quantum communication over intercontinental range, which is currently not possible via terrestrial connections. In such constellations, satellites should not only be connected but connected via short paths of at most í µí±˜ hops, as otherwise quantum decoherence can cause problems. Measuring the reliability of networks is a classical #P-complete problem and, thus, extremely difficult. Reliability is traditionally studied with advanced Monte Carlo simulations, analytic approaches, or sampling methods such as line sampling and variance reduction schemes. Unfortunately, these strategies are computationally expensive and scale poorly. Weighted model counting, the problem of counting the weighted number of satisfying assignments of a propositional formula, is a promising alternative from the toolbox of probabilistic reasoning. Recent advances in incorporating structure-guided approaches, algebraic decision diagrams, and compilations into deterministic, decomposable negation normal forms provide a variety of open-source model counters that can handle industry-scale instances. We evaluate these tools on the problem of computing the reliability of a constellation with inter-satellite communication and, for the first time, provide theoretical sound estimates of the reliability of the imposed networks. Such estimates are the first and central step in developing an algorithmic pipeline to design robust inter-satellite topologies automatically. Our techniques generalize to the case in which we consider a network reliably if satellites are connected via short paths and, hence, we can provide similar estimates for quantum communication constellations.