Automated Reasoning for Quantum Circuit Analysis and Optimization
Automated reasoning has proven highly effective in classical domains for solving complex combinatorial problems, including hardware and software verification, probabilistic inference, and planning. This talk explores how these techniques can be extended to the quantum computing domain, specifically for analyzing and optimizing quantum circuits.
We focus on the use of model counting (#SAT), the counting variant of the satisfiability problem, as a central tool. By encoding quantum circuits into propositional logic, we can leverage powerful #SAT solvers not only to simulate, verify, synthesize, and optimize quantum circuits, but also to make their behavior more accessible—particularly for those less familiar with the standard linear algebraic formalism of quantum computing.
This logical perspective opens up new possibilities for understanding and improving quantum algorithms using classical techniques. We will also discuss how these methods contribute to the broader goal of achieving quantum supremacy—demonstrating tasks that quantum computers can perform faster than their classical counterparts.
Date, time and place: Wednesday 02/07, 16:30-18:30, Middelheim campus, A building, room 143
Suggested reading, watching:
About the speaker
Alfons Laarman leads the System Verification Lab (SVL) at the Leiden Institute for Advanced Computer Science (LIACS). He is also a co-founder of the applied quantum algorithms (aQa) initiative, an inter-disciplinary team researching quantum algorithms and their applications across multiple Leiden institutes. His main research interests include formal verification, automated reasoning, quantum computing, and parallel computing. Dr. Laarman is involved in numerous projects on quantum computing, including leading a work package on optimization techniques for quantum circuits in the EU Horizon grant EQUALITY, collaborating on a case study in quantum probabilistic risk analysis in the EU H2020 grant NEASQC, and serving as the PI for the NWO NWA grant Divide & Quantum. He was also awarded an NWO national growth fund grant for the BoostQA project, focusing on adding classical technologies to quantum algorithms. He has been an invited speaker at various academic events related to model checking, automated reasoning, parallel computing, and quantum computing. He is also the founder of LUdev, a student-run software development company.