Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a compact representation with powerful reduction rules that yield a canonical form for the classically simulable Clifford fragment, but confluence fails beyond the Clifford fragment. We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art tools.

翻译：量子电路的等价性检查是量子计算中的一项核心验证任务，用于确保电路优化、硬件映射和编译流程的正确性。在此类主要符号化方法中，路径和形式体系通过强大的化简规则提供紧凑表示，可为经典可模拟的克利福德片段生成规范形式，但超出克利福德片段后其汇合性失效。我们提出了一种新的路径和加权模型计数编码，并将其与现有路径和化简规则结合，构建出既完整又高效的验证器。该方法尽可能应用化简规则，并对残余路径和调用基于加权模型计数的决策过程，实现全局相位意义下的完全语义检查。我们实现了该方法并在标准基准上进行了评估。结果表明，这种混合方法优于各独立组件的性能，且能与现有先进工具相竞争。