IGMaxHS -- 面向 XOR 子句的增量 MaxSAT 求解器
人工智能
2024-10-22 v1
摘要
最近提出了一种新型基于 MaxSAT 方法用于量子计算错误更正的技术，要求具备增量 MaxSAT 求解能力和对 XOR 约束的支持，但目前尚无专门的 MaxSAT 求解器满足这些要求。我们在此提出 IGMaxHS，它基于现有求解器 iMaxHS 和 GaussMaxHS 开发而来，但相较于 GaussMaxHS 对 XOR 约束的限制更少。IGMaxHS 使用 xwcnfuzz 进行模糊测试，该工具是 wcnfuzz 的扩展，可直接输出 XOR 约束。作为结果，IGMaxHS 是进行 10000 实例最终模糊测试比较中唯一未报告错误的不可满足判断、无效模型或不一致代价模型组合的求解器。我们详细阐述了在 CDCL SAT 求解器中实现对 XOR 约束的高斯消去步骤，并扩展最近提出的可重入增量 MaxSAT 求解器应用程序编程接口，以支持增量添加 XOR 约束。最后，我们展示 IGMaxHS 能够通过模拟在慕尼黑量子工具包中解码量子色码。
关键词
引用
@article{arxiv.2410.15897,
title = {IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses},
author = {Ole Lübke},
journal= {arXiv preprint arXiv:2410.15897},
year = {2024}
}
备注
Presented at the 15th International Workshop on Pragmatics of SAT (PoS 2024, see https://www.pragmaticsofssat.org/2024/ )