用超图神经网络减少求解约束问题的验证次数，提速找最小不满足子集。
Hypergraph Neural Networks Accelerate MUS Enumeration
- 构建超图：约束作顶点，已找的不满足子集作超边
- 强化学习训练模型，减少验证次数，同等预算下多找MUS
- 不依赖具体领域，适用于各类约束问题
最小不满足子集（MUS）枚举是约束满足问题中的基础任务，其主要挑战在于搜索空间随规模呈指数级增长，尤其当可满足性检查成本高昂时更为严重。现有机器学习方法虽能降低布尔可满足性问题的开销，但依赖显式的变量-约束关系，限制了适用范围。本文提出一种无领域依赖的方法，利用超图神经网络（HGNN）加速MUS枚举。该方法逐步构建超图，以约束为顶点、已枚举的MUS为超边，并通过强化学习训练一个HGNN代理，以最小化获取MUS所需的可满足性检查次数。实验表明，本方法在相同检查预算下能枚举更多MUS，显著提升效率。
原文摘要 · Abstract (English)
Enumerating Minimal Unsatisfiable Subsets (MUSes) is a fundamental task in constraint satisfaction problems (CSPs). Its major challenge is the exponential growth of the search space, which becomes particularly severe when satisfiability checks are expensive. Recent machine learning approaches reduce this cost for Boolean satisfiability problems but rely on explicit variable-constraint relationships, limiting their application domains. This paper proposes a domain-agnostic method to accelerate MUS enumeration using Hypergraph Neural Networks (HGNNs). The proposed method incrementally builds a hypergraph with constraints as vertices and MUSes enumerated until the current step as hyperedges, and employs an HGNN-based agent trained via reinforcement learning to minimize the number of satisfiability checks required to obtain an MUS. Experimental results demonstrate the effectiveness of our approach in accelerating MUS enumeration, showing that our method can enumerate more MUSes within the same satisfiability check budget compared to conventional methods.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。