QSolver: A Quantum Constraint Solver

TL;DR

QSolver is a pioneering quantum constraint solver that transforms quantum programs into symbolic forms, uses SMT solvers for state generation, and verifies correctness through automated assertions, enhancing quantum program verification.

Contribution

Introduces the first quantum constraint solver, QSolver, with a structured framework for handling quantum constraints and automated verification of quantum states.

Findings

Efficiently processes common quantum gates.

Demonstrates scalability across various quantum program sizes.

Validates quantum states with automated assertion generation.

Abstract

With the growing interest in quantum programs, ensuring their correctness is a fundamental challenge. Although constraint-solving techniques can overcome some limitations of traditional testing and verification, they have not yet been sufficiently explored in the context of quantum programs. To address this gap, we present QSolver, the first quantum constraint solver. QSolver provides a structured framework for handling five types of quantum constraints and incorporates an automated assertion generation module to verify quantum states. QSolver transforms quantum programs and multi-moment constraints into symbolic representations, and utilizes an SMT solver to obtain quantum states that satisfy these constraints. To validate the correctness of the generated input states, QSolver automatically generates assertion programs corresponding to each constraint. Experimental results show that QSolver efficiently processes commonly used quantum gates and demonstrates good scalability across quantum programs of different sizes.