Facets of Automated Reasoning
Automated reasoning is a subfield of mathematical logic, artificial intelligence, and philosophy that is concerned with knowledge representation and the automatization of logical deduction. Its primal subject is the mechanized search for proofs in formal systems. Automated reasoning is used to ensure that software and hardware systems are correct, robust, and safe. In this context, automated reasoning is also called formal verification, which has the goal of rigorously proving what the behavior of software or hardware systems is.
Complexity Theoretic Aspects
Mathematical logic is called the calculus of computer science and is surprisingly tightly linked to computational complexity [1]. In the light of automated reasoning, the complexity classes P and NP (polynomial and nondeterministic polynomial time) correspond to classical reasoning, while PP and #P (probabilistic polynomial time and its counting version) can be considered as classes of probabilistic reasoning. Unfortunately, these classes bear high complexity and, thus, automated reasoning was considered mainly theoretical for various decades. However, immense algorithmic breakthroughs and engineering efforts have rendered formal methods practical to the extent that they scale to industry-sized instances.
These advances are counterintuitive to the worst-case performance predicted by classical complexity theory. Researchers of the Advanced Concepts Team study the fine details of this complexity by taking structural parameters of the input data and syntactic restrictions of the given logical formula into account. A typical example is the treewidth of the input [2].
Maximum Satisfaction
The maximum satisfiability problem (MaxSAT) is the canonical problem in logic-based optimization that plays a crucial role in the theory of optimization and approximation algorithms. MaxSAT became a valuable tool in the arsenal of formal methods, with applications in combinatorial testing, detecting communities in complex networks, fault localization, fault diagnosis, group testing, cost-optimal planning, routing, scheduling, team formation, and data analysis.
The Advanced Concepts Team fosters ESA's in-house experience with this technology and is pursuing the development of open-source solvers. We study the applicability of MaxSAT in satellite scheduling and as a tool in verifiable classical-quantum hybrid algorithms. Furthermore, we investigate the use of MaxSAT in early-stage mission design for multi-rendezvous spacecraft trajectories. Details on the latter application can be found in the related Keplerian TSP project.
Probabilistic Reasoning
Many reasoning and inferencing tasks have to be performed under the assumption that decision variables obey some probability distribution. Such probabilistic reasoning tasks can formally be modeled using the model counting problem (#SAT). Model counting is extremely difficult from a computational complexity perspective. Still, remarkable progress in solver technology has been made in recent years. Applications of #SAT include contingency planning, Bayesian reasoning, statistical physics, statistical sampling, explainable AI, and security vulnerability analysis.
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. They are essential for quantum communication over intercontinental range, which is currently impossible via terrestrial connections. The satellites of a constellation define a network of communication links, which may fail with some error probability due to factors like geography, weather conditions, hardware malfunctions, or positioning errors. Within this project, we study the reliability of satellite constellations with inter-satellite links using model counting. This approach allows us to find theoretically sound estimates of the probability for events such as the existence of a connection between two endpoints. The related Satellite Quantum Network Optimisation project studies corresponding models and simulations.
Automated Reasoning in Quantum Computing
Tensor networks are graphical representations of computations on high-dimensional arrays. They have their origin in physics, where they play a central role in the study of many-body quantum systems [3]. They have also proven useful in large-scale machine learning and artificial intelligence [4]. In particular, tensor networks are the backbone of modern probabilistic inference engines, as tensor contractions are closely related to the problem of counting the number of models of a propositional formula [5].
Nodes in tensor networks aggregate information that they send through layers of the network. To a certain degree, this is a property tensor networks share with common notations from structural graph theory. For instance, a tree decomposition aggregates parts of a graph in so-called bags. It is known that tree decompositions can be used to simulate tensor network contractions and, thus, to simulate quantum circuits [6]. Within this project, we advance the development of new algorithms to quickly compute tree decompositions of industry-sized graphs, explore the applicability of tensor networks in applications arising within the agency, and evaluate how far state-of-the-art model counters based on structural graph theory can be applied in these scenarios. Primary, we study the possibility of utilizing probabilistic reasoning engines based on structure-guided model counters to simulate quantum circuits. See also the related project Structure-guided Quantum Computing.
References
[1] Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, and Victor Vianu:
On the unusual effectiveness of logic in computer science.
Bull. Symb. Log. 7(2): 213-236 (2001)
[2] Hans L. Bodlaender:
A Tourist Guide through Treewidth.
Acta Cybern. 11(1-2): 1-21 (1993)
[3] Jacob Biamonte and Ville Bergholm
Tensor Networks in a Nutshell
CoRR abs/1708.00006 (2017)
[4] Adnan Darwiche:
An Advance on Variable Elimination with Applications to Tensor-Based Computation.
ECAI 2020
[5] Jeffrey M. Dudek, and Moshe Y. Vardi:
Parallel Weighted Model Counting with Tensor Networks.
CoRR abs/2006.15512 (2020)
[6] Igor L. Markov and Yaoyun Shi:
Simulating Quantum Computation by Contracting Tensor Networks.
SIAM J. Comput. 38(3): 963-981 (2008)