Optimal Synthesis of Stabilizer Codes via MaxSAT

Quantum Error Correction (QEC) codes are crucial for achieving fault-tolerant quantum computing in the long term. However, efficiently implementing these codes on hardware poses significant challenges, including hardware connectivity matching, efficient circuit scheduling, and fault-tolerance enforcement. In this study, we present an optimal synthesizer that stitches generic stabilizer codes onto diverse hardware structures via MaxSAT. Our evaluation demonstrates (1) the capability of our approach to be applied for various codes and devices and (2) the consistently better efficiency than the best prior heuristic approaches that only target specific QEC codes. By bridging the gap between high-level QEC code design and low-level hardware constraints, this work paves the way toward achieving long-term fault-tolerant quantum computing goals.