Alfons Laarman (Leiden University) - The Effectiveness of Automated Reasoning in Quantum Computing*

*Full Title: The Unreasonable Effectiveness of Automated Reasoning in Quantum Computing
Abstract:
In this talk, we will show that existing classical automated reasoning methods perform exceedingly well for computationally hard problems in quantum computing. In particular, we demonstrate a linear-length #SAT encoding of the simulation and equivalence checking of universal quantum circuits. An implementation of this method, called Quokka#, outcompetes other state-of-the-art approaches using an off-the-shelve #SAT solver that supports negative weights (GPMC).
While decision diagrams offer a viable alternative, we unveil their inherent limitations stemming from their inability to represent the prevalent stabilizer states. This limitation is particularly noteworthy considering the efficient classical simulatability of circuits generating such states. To address this constraint, we introduce Local Invertible Map Decision Diagrams (LIMDDs), which offer exponential improvements in succinctness compared to the combination of stabilizer formalism and existing decision diagrams.
Finally, we show how these findings can be translated back to the domain of quantum physics, so that the results will be useful regardless of the existence of quantum computers. For this, we use Darwiche's seminal "knowledge compilation map" approach by providing a first knowledge compilation map for quantum information comparing various decision diagrams against tensor networks and Boltzmann machines; two formalisms extensively used in physics to tackle quantum-hard problems like simulation of many-body systems and finding the ground energy of such a system. Our results show that existing automated reasoning methods have a strong potential for quantum computing and physics.
Date of talk: 2024-05-24

[@jingyimei1182]

very useful and clear talk!👍