Automated Reasoning with Complex Weights to Simulate and Verify Noisy Quantum Circuits - Study reference 24-5100

Sep 14, 2026

Uploaded by Fahsai

Automated reasoning techniques are used to advance automated verification and simulation of noisy quantum circuits by extending model counting to handle complex-valued weights. The study targets theoretical and practical development in which complex weights are incorporated either through new encoding methods for existing model-counting pipelines or via model counters designed to support complex weights from the outset. The resulting pipeline will be benchmarked against established noisy quantum simulators such as Qiskit and evaluated across broader model-counting instance sets, with participation in relevant computational challenges encouraged.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages5

Reading Time13 min

AccessFree to download

Project Summary

Objective

Study Objective

Background and Study Motivation

Technical Rationale and Approach

Figures and Illustrative Examples

Automated Reasoning with Complex Weights to Simulate and Verify Noisy Quantum Circuits Study reference number: 24-5100 Type of activity: Standard study Project Summary Objective To advance significantly the state-of-the-art in automated reasoning exploring the introduction of complex numbers in model counting techniques. To prove the value of the idea in the context of the simulation and verification of noisy quantum circuits. Target university partner competences Automated Reasoning, Formal Methods, Theoretical Computer Science ACT provided competences Quantum Computing, Fundamental Physics Keywords Quantum Computing, Model Counting, Simulation, Encodings Study Objective This study will examine either the theoretical background of algorithms and encoding techniques to manage complex weights in existing model counting pipelines, or the development of new model counters that support complex weights by design. Based on the chosen path, a new model-countingbased pipeline to simulate and verify quantum circuits with noise will be implemented, utilizing either existing counters in conjunction with the new encoding, or using the model counter developed within this study. The performance of the pipeline shall be assessed by comparing it to other quantum circuit simulators that support noise (e.g., Qiskit) and by benchmarking it on a broader range of model counting instances. To support this endeavour, the participation in computational challenges (e.g., the corresponding track of the model counting competition) is encouraged. Background and Study Motivation Interest in gate-based quantum computing has grown steadily in recent years, largely due to advancements in qubit scaling and improvements in error correction. Companies like IBM and Atom Computing have announced processors with over 1,000 qubits, marking important progress toward practical, large-scale quantum computers [1, 2] . While the increase in qubit count is notable, ongoing improvements in gate fidelity and coherence times are equally important for the realization of useful quantum systems. In the space domain, researchers are exploring quantum computing for optimizing satellite communication, mission scheduling, and processing large volumes of remote sensing data. For example, quantum algorithms have been proposed for satellite constellation optimization [4] and quantum machine learning techniques for analysing space-based sensor data [5] . The European Space Agency has initiated projects to assess quantum computing’s impact on Earth observation [6,7] . However, scalable quantum computing remains a distant goal, as current hardware is limited by noise, qubit connectivity, and the overhead of quantum error correction [8,9] . As a result, near-term exploration of quantum applications must rely heavily on classical simulators to assess the performance, robustness, and practical feasibility of quantum algorithms [10,11] . These simulators provide a crucial testing ground for studying quantum behaviour under realistic noise models and device constraints. Furthermore, once practical quantum computers become available, simulators will continue to play a vital role in the verification and debugging of quantum programs—ensuring correctness, identifying sources of error, and validating outputs that are otherwise intractable to compute classically [12] . Figure 1: A probabilistic circuit with three inputs and one output. The gates with dice flip the input with a certain probability, the other are the usual logical gates. In orange the layers of the circuit are highlighted, which are referenced in the encoding in Figure 2. Automated Reasoning emerged as a promising route in the quantum software development stack. For instance, SAT is used for quantum circuit mapping [20], MaxSAT is used to decode quantum colour codes [13], for quantum error correction decoders [14], and was deployed by ACT researchers as an intuitive interface to near-term qua

FAQs

What is the main objective of the study?

To significantly advance automated reasoning techniques by introducing complex numbers into model counting methods, enabling simulation and verification of noisy quantum circuits and demonstrating the value of this idea.

How will the study implement support for complex weights?

It will either develop theory and encodings that extend existing model-counting pipelines to manage complex weights, or build new model counters that support complex weights by design.

How will the proposed pipeline be evaluated?

Performance will be assessed by comparing against noisy quantum circuit simulators such as Qiskit and by benchmarking on a broader range of model counting instances.

Sep 14, 2026

Uploaded by Fahsai