QSolver: 一种量子约束求解器
QSolver: A Quantum Constraint Solver
AI总结：
QSolver是一种首个量子约束求解器，通过结构化框架和自动断言生成模块，高效处理量子约束并验证量子状态的正确性。
摘要：
随着对量子程序兴趣的增加，确保其正确性成为一项基本挑战。尽管约束求解技术可以克服传统测试和验证的一些局限性，但在量子程序背景下尚未得到充分探索。为解决这一差距，我们提出了QSolver，这是首个量子约束求解器。QSolver提供了一个处理五种类型量子约束的结构化框架，并集成了一个自动断言生成模块来验证量子状态。QSolver将量子程序和多时刻约束转换为符号表示，并利用SMT求解器获取满足这些约束的量子状态。为了验证生成的输入状态的正确性，QSolver会自动为每个约束生成对应的断言程序。实验结果表明，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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
