设计自动化与时空缩减：基于可满足性理论（SAT）的电子设计自动化（EDA）内核实现兼容通用编码的表面码逻辑运算
基于表面码与晶格手术的容错量子计算机（FTQC）已得到广泛研究，学界亟需一种能识别低时空代价逻辑操作、验证其功能与容错性、并在给定搜索空间中证明其最优性的框架——这与经典电路设计中的电子设计自动化（EDA）理念高度契合。本文提出KOVAL-Q，该EDA内核通过将表面码逻辑操作转化为可满足性问题（SAT）进行验证与优化。相较于LaSsynth等现有SAT框架，该团队的方法能处理采用更灵活表面码编码的逻辑量子比特（既可作为目标构型也可作为中间态），从而支持快速区块等高级布局优化，并拓展逻辑操作的搜索空间。实验证明KOVAL-Q能确定基础逻辑操作（如d周期逻辑CNOT门与2d周期区块旋转）在给定空间布局下的最短执行时间，在简化调度模型下可使主流FTQC应用的执行时间降低约10%。该内核包含三个对应不同约束类型的子模块，便于作为子组件集成至可扩展启发式框架中，为FTQC核心子程序的优化验证提供了关键基础设施。
