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.

翻译：我们探讨了利用SMT（可满足性模理论）求解器扩展量子电路验证方法的思路。提出两种主要策略：（1）通过组合式验证分解证明义务，（2）利用门效应的线性过近似技术。通过两个示例展示了这些思想在证明汉明权重保持性方面的应用。