Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

TL;DR

This paper presents a hybrid method combining path-sum formalism and weighted model counting for efficient and complete equivalence checking of quantum circuits, outperforming existing tools.

Contribution

It introduces a novel WMC encoding for path-sums and integrates it with path-sum reductions to enhance quantum circuit equivalence verification.

Findings

Hybrid method outperforms individual components in benchmarks.

The approach is complete up to a global phase.

Competitiveness with state-of-the-art tools is demonstrated.

Abstract

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.