构建结构化SAT数据集,揭示图神经网络泛化能力与问题结构的关系。
Structure based SAT dataset for analysing GNN generalisation
- 基于图结构特性构建可细分的SAT数据集,支持细粒度分析
- 发现现有GNN SAT求解器在复杂结构上泛化能力差
- 适合研究图神经网络泛化、SAT求解优化的研究者
基于冲突驱动子句学习(CDCL)的可满足性(SAT)求解器在合成及工业实际问题中表现优异。尽管这些求解器仅针对单个问题运行,基于图神经网络(GNN)的求解器通过利用已解决问题的知识,可加速新问题的求解。然而,一个常被CDCL求解器研究但被忽视的领域——即SAT问题的图论结构特征与GNN求解器泛化能力之间的关系——仍未得到充分关注。为弥合这一差距,本文提出StructureSAT:一个精心构建的数据集,包含来自知名问题领域的多样化SAT实例,并提供生成新样本的代码。此外,我们采用一种新型拆分方法,依据结构属性将问题家族细化为更详细的层级。借助该数据集,旨在通过分析图结构特性来解释现有GNN SAT求解器的泛化缺陷。最后,我们提出多个未来研究方向,以帮助研究人员开发更高效、更具泛化能力的GNN-SAT求解器。
原文摘要 · Abstract (English)
Satisfiability (SAT) solvers based on techniques such as conflict driven clause learning (CDCL) have produced excellent performance on both synthetic and real world industrial problems. While these CDCL solvers only operate on a per-problem basis, graph neural network (GNN) based solvers bring new benefits to the field by allowing practitioners to exploit knowledge gained from solved problems to expedite solving of new SAT problems. However, one specific area that is often studied in the context of CDCL solvers, but largely overlooked in GNN solvers, is the relationship between graph theoretic measure of structure in SAT problems and the generalisation ability of GNN solvers. To bridge the gap between structural graph properties (e.g., modularity, self-similarity) and the generalisability (or lack thereof) of GNN based SAT solvers, we present StructureSAT: a curated dataset, along with code to further generate novel examples, containing a diverse set of SAT problems from well known problem domains. Furthermore, we utilise a novel splitting method that focuses on deconstructing the families into more detailed hierarchies based on their structural properties. With the new dataset, we aim to help explain problematic generalisation in existing GNN SAT solvers by exploiting knowledge of structural graph properties. We conclude with multiple future directions that can help researchers in GNN based SAT solving develop more effective and generalisable SAT solvers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。