We explore ideas for scaling verification methods for quantum circuits using SMT (Satisfiability Modulo Theories) solvers. We propose two primary strategies: (1) decomposing proof obligations via compositional verification and (2) leveraging linear over-approximation techniques for gate effects. We present two examples and demonstrate the application of these ideas to proof Hamming weight preservation.
@article{arxiv.2411.19177,
title = {Bounds for Quantum Circuits using Logic-Based Analysis},
author = {Benedikt Fauseweh and Ben Hermann and Falk Howar},
journal= {arXiv preprint arXiv:2411.19177},
year = {2024}
}