维度对随机几何SAT问题影响的实证分析
Empirical Impact of Dimensionality on Random Geometric SAT
AI总结：
本文通过实证分析，研究了低维几何模型对SAT问题可满足性阈值、求解时间及证明大小的影响，发现该模型能涵盖从易到难的实例范围。
摘要：
布尔可满足性问题可能是理论计算机科学中最著名的难题之一。一方面，它被证明是NP难的，这意味着通常认为解决它很困难。另一方面，SAT问题已找到许多实际应用，产生所谓的工业实例，而SAT求解器往往能高效地解决这些实例。缩小理论与实践之间的差距是当前研究的主题。一种方法是识别使SAT实例可处理的属性。为此，提出了生成SAT实例的模型，以模仿工业实例的属性。迄今为止，尝试创建此类模型的努力大多失败了，实例要么太容易解决，要么太难解决，或缺少工业SAT实例的重要属性。在本工作中，我们分析了一个由Giráldez-Cru和Levy引入的有希望的SAT模型，该模型基于底层几何。我们实证分析了该几何的维度对SAT实例在三个属性上的影响：可满足性阈值的位置、求解器时间以及不可满足性证明的大小。补充理论工作，我们发现低维几何实例在整体上都非常可处理。随着维度的增加，几何模型生成的实例似乎趋于均匀实例，这意味着该几何模型能够代表从易到难的所有实例范围。我们还观察到，低维几何实例的可满足性阈值出现在较低的密度下。此外，低维实例与均匀实例的行为非常不同，因为它们在可满足性阈值处没有求解器时间的硬度峰值。这与证明大小一致，我们显示证明大小在低维情况下不与求解器时间相关。
英文摘要：
The Boolean Satisfiability Problem is perhaps one of the most well-known problems in theoretical computer science. On the one hand, it is proven to be NP-complete, which means that it is generally considered hard to solve. On the other hand, the SAT problem has found many practical applications, which yield so-called industrial instances, and SAT solvers can often efficiently find solutions to such instances. Closing this gap between theory and practice is a subject of current research. One approach is to identify properties of SAT instances that make them tractable. To aid in this, models for generating SAT instances have been proposed that mimic the properties of industrial instances. So far, attempts at creating such models were mostly unsuccessful, with instances being either too easy or too hard to solve, or missing important properties of industrial SAT instances. In this work, we analyse a promising SAT model introduced by Giráldez-Cru and Levy which is based on an underlying geometry. We empirically analyse the impact of this geometry's dimension on SAT instances with regard to three properties: the location of the satisfiability threshold, solver time, and size of proofs of unsatisfiability. Supplementing theoretical work, we find that low-dimensional geometric instances are throughout very tractable. As dimension increases, instances from the geometric model seem to converge to hard uniform instances, which means that the geometric model is capable of representing the full range of easy to hard instances. We also observe that the satisfiability threshold in low-dimensional geometric instances occurs at lower densities. Additionally, low-dimensional instances behave very unlike uniform instances in that they have no hardness peaks in solver time at the satisfiability threshold. This coincides with proof size, which we show to not correlate to solver time at low dimensions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
