用于晶格手术的 SAT 手术刀：表面码容错量子计算子程序的表示与综合

量子纠错对于大规模量子计算是必需的。一种有前景的量子纠错码是表面码。对于这种码，容错量子计算（FTQC）可以通过晶格手术来执行，即拆分和合并编码块。鉴于某些晶格手术子程序（LaS）的频繁使用，优化其设计以最小化 FTQC 的整体时空体积变得至关重要。在本研究中，我们定义了表示 LaS 的变量以及这些变量上的约束。利用这种形式化，我们开发了一个 LaS 综合器 LaSsynth，它将 LaS 构造问题编码为一个 SAT 实例，随后查询 SAT 求解器以获取解。从基线设计开始，我们可以逐步调用求解器，同时缩小时空体积，以推导出更紧凑的设计。由于我们的基础形式化和 SAT 求解器的使用，LaSsynth 可以穷举地探索设计空间，产生体积最优的设计。例如，对于 FTQC 中的一个瓶颈——15 到 1 的 T 工厂，它分别比两个最先进的人工设计减少了 8% 和 18% 的体积。