一句话：提出首个量子约束求解器 QSolver，将量子程序与多时刻约束符号化并用 SMT 求解满足约束的量子态。
量子程序正确性保障是基本挑战，传统测试与验证存在局限，而约束求解在量子程序场景中尚未被充分探索。本文提出首个量子约束求解器 QSolver，提供处理五类量子约束的结构化框架，并集成自动断言生成模块以验证量子态。QSolver 将量子程序与多时刻约束转换为符号表示，利用 SMT 求解器获得满足约束的量子态；为验证生成的输入态，它自动为每类约束生成对应的断言程序。实验表明，QSolver 能高效处理常用量子门，并在不同规模量子程序上展现良好可扩展性。
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.