超图神经网络加速 MUS 枚举
人工智能
2026-04-13 v1 机器学习
计算机科学中的逻辑
摘要
枚举最小不可满足子集（MUSes）是约束满足问题（CSPs）中的基本任务，其主要挑战在于搜索空间的指数级增长，尤其在可满足性检查成本较高时更为严峻。近期机器学习方法虽能降低布尔可满足性问题的检查成本，但依赖于显式的变量-约束关系，限制了其应用范围。本文提出一种基于超图神经网络（HGNNs）的领域无关方法，以加速 MUS 枚举。该方法递增构建超图，将约束作为顶点，将当前步骤枚举得到的 MUS 作为超边，运用经过强化学习训练的 HGNN-based agent 来最小化获取一个 MUS 所需的可满足性检查次数。实验结果表明，我们的方法在加速 MUS 枚举方面有效，显示在相同的可满足性检查预算下，本方法可枚举更多的 MUS 相较于传统方法。
引用
@article{arxiv.2604.09001,
title = {Hypergraph Neural Networks Accelerate MUS Enumeration},
author = {Hiroya Ijima and Koichiro Yawata},
journal= {arXiv preprint arXiv:2604.09001},
year = {2026}
}