工业 SAT 实例中的社区结构
人工智能
2023-03-14 v3 社会与信息网络
摘要
现代 SAT 求解器在求解工业实例方面取得了显著进展。大多数技术是在密集实验过程之后开发的。人们相信这些技术利用了工业实例的底层结构。然而，很少有工作试图精确刻画这一结构的主要特征。复杂网络研究社区已经开发了可用于 SAT 社区的分析技术和算法来研究真实世界图。近期，已有若干尝试从复杂网络的角度分析工业 SAT 实例的结构，以解释 SAT 求解技术成功的原因并可能改进它们。在本文中，受复杂网络结果的启发，我们研究了工业 SAT 实例的社区结构或模度。在具有清晰社区结构或高模度的图中，我们可以找到节点的划分使得大多数边连接同一社区中的变量。在我们的分析中，我们将 SAT 实例表示为图，并表明大多数应用基准实例以高模度为特征。相反，随机 SAT 实例更接近经典的 Erdős-Rényi 随机图模型，其中观察不到任何结构。我们还分析了这种结构如何受 CDCL SAT 求解器执行的影响。特别是，我们利用社区结构来检测求解器在搜索过程中学习到的新子句倾向于破坏公式的原始结构。即，学习到的子句倾向于包含来自不同社区的变量。
引用
@article{arxiv.1606.03329,
title = {Community Structure in Industrial SAT Instances},
author = {Carlos Ansótegui and Maria Luisa Bonet and Jesús Giráldez-Cru and Jordi Levy and Laurent Simon},
journal= {arXiv preprint arXiv:1606.03329},
year = {2023}
}