随机几何 SAT 中维度对经验影响
计算机科学中的逻辑
2026-03-03 v1
摘要
布尔满足问题（SAT）或许是计算机科学中最著名的问题之一。一方面，已证明该问题是 NP 完全的，这意味着人们普遍认为很难解决。另一方面，SAT问题找到了许多实际应用，产生所谓的工业实例，SAT 求解器通常可以有效地找到此类实例的解决方案。弥合理论与实践之间的差距是当前研究的主题之一。一种方法是识别使 SAT 实例易于解决的性质。为此，有人提出了生成模型来模拟工业实例的属性。迄今为止，试图创建此类模型的尝试大多不成功，实例要么太容易要么太难解决，或缺少工业 SAT 实例的重要属性。在本工作中，我们分析了由 Gir\'aldez-Cru 和 Levy 提出的一种基于几何的 SAT 模型。我们对该几何维度对 SAT 实例的影响进行经验分析，涉及三个属性：满足阈值的位置、求解器时间以及不满足性证明的大小。补充理论工作，我们发现低维几何实例始终非常容易解决。随着维度的增加，来自几何模型的实例似乎收敼到难以求解的均匀实例，这意味着几何模型能够表示从易到难的完整范围。我们还观察到，在低维几何实例中，满足阈值发生在较低的密度处。此外，低维实例的行为与均匀实例截然不同，以它们在求解器时间的满足阈值处没有硬度峰值。这与证明大小相关联，我们证明在低维度上，证明大小与求解器时间不相关。
引用
@article{arxiv.2603.01892,
title = {Empirical Impact of Dimensionality on Random Geometric SAT},
author = {Flora Rädiker},
journal= {arXiv preprint arXiv:2603.01892},
year = {2026}
}
备注
This is my bachelor's thesis submitted at the Digital Engineering Faculty of University of Potsdam