首个支持XOR约束的增量MaxSAT求解器，用于量子纠错编码解码。
IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses
- 在CDCL框架中实现高斯消元处理XOR约束，支持增量添加
- 10000次模糊测试中无错误判决、无效模型或成本不一致
- 适用于量子纠错中的颜色码解码，兼容Munich量子工具包
近期提出了一种基于MaxSAT的量子计算纠错新方法，需要具备增量MaxSAT求解能力及对XOR约束的支持，但当时尚无满足此要求的专用求解器。为此，我们提出IGMaxHS，基于iMaxHS和GaussMaxHS，对XOR约束的限制更少。IGMaxHS使用xwcnfuzz（wcnfuzz的扩展，可直接输出XOR约束）进行模糊测试。在包含10000个实例的最终对比测试中，IGMaxHS是唯一未报告错误不可满足判断、无效模型或不一致成本组合的求解器。本文详细阐述了在CDCL SAT求解器中实现高斯消元处理XOR约束的步骤，并扩展了最近提出的可重入增量MaxSAT求解器接口，以支持增量添加XOR约束。最后，通过Munich Quantum Toolkit仿真，证明IGMaxHS能够成功解码量子颜色码。
原文摘要 · Abstract (English)
Recently, a novel, MaxSAT-based method for error correction in quantum computing has been proposed that requires both incremental MaxSAT solving capabilities and support for XOR constraints, but no dedicated MaxSAT solver fulfilling these criteria existed yet. We alleviate that and introduce IGMaxHS, which is based on the existing solvers iMaxHS and GaussMaxHS, but poses fewer restrictions on the XOR constraints than GaussMaxHS. IGMaxHS is fuzz tested with xwcnfuzz, an extension of wcnfuzz that can directly output XOR constraints. As a result, IGMaxHS is the only solver that reported neither incorrect unsatisfiability verdicts nor invalid models nor incoherent cost model combinations in a final fuzz testing comparison of all three solvers with 10000 instances. We detail the steps required for implementing Gaussian elimination on XOR constraints in CDCL SAT solvers, and extend the recently proposed re-entrant incremental MaxSAT solver application program interface to allow for incremental addition of XOR constraints. Finally, we show that IGMaxHS is capable of decoding quantum color codes through simulation with the Munich Quantum Toolkit.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。