Bounds for Quantum Circuits using Logic-Based Analysis

Benedikt Fauseweh, Ben Hermann, Falk Howar

We explore ideas for scaling verification methods for quantum circuits using SMT (Satisfiability Modulo Theories) solvers. We propose two primary strategies: (1) decomposing proof…