EAGER: From Theory to Practice of Quantum Circuit Decidability

Quantum computers are extremely powerful devices capable of solving certain problems much faster than traditional computers. However, programming these advanced systems is challenging, and converting code into instructions that the quantum hardware can interpret often introduces unwanted errors. This project will develop a framework that will automatically analyze code to identify these errors, ensuring that programs run correctly on quantum computer hardware. The intellectual merit of this work lies in the central idea that integrating Weighted Model Counting with a theory propagator that detects Pauli-transfer inconsistencies and commutativity constraints during conflict-driven search may provide a better understanding of error propagation during: high-level code translation into gate-level circuits; optimizing the gate count and depth; routing the circuit onto actual quantum hardware; and embedding the problem space into an error-correcting code. The project will integrate dynamic weighted Pauli-basis reasoning directly into a constraint solver loop to efficiently verify quantum circuits. The project is organized into four specific thrusts. Thrust one develops a formal theory specification and assesses mathematical properties, such as convexity and theory combination compatibility. Thrust two creates a custom Satisfiability Modulo Theories user-propagator within the Conflict-Driven Clause Learning loop to generate dynamic conflict explanations and commutativity lemmas. Thrust three incorporates this propagator with a Weighted Model Counting pipeline. Thrust four conducts comprehensive benchmarking to validate reductions in decision branches and execution runtime. The project will have significant broader impacts by making the entire toolchain and benchmarks fully open source, thereby accelerating scientific discovery in this important field. Detecting errors in code translation will ensure the correctness of quantum programs, saving time and costs in the development and deployment of advanced quantum computer systems. The research findings will be integrated into Kansas State University graduate courses for students with limited backgrounds in quantum computing. Educational outreach will include interactive quantum computing demonstrations for high school students at engineering open houses and technical presentations at major quantum computer and information science and engineering conferences to support workforce development. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.