异质性与几何结构对随机可满足性问题证明复杂性的影响
计算复杂性
2021-11-24 v2 计算几何
离散数学
数据结构与算法
概率论
摘要
可满足性（Satisfiability）被视为典型的 NP 完全问题，在理论中用作困难归约的起点，而在实践中启发式 SAT 求解算法可非常高效地求解大规模工业 SAT 实例。理论与实践的这种差异被认为源于工业 SAT 实例使其易处理的固有属性。绝大多数真实世界 SAT 实例中似乎普遍存在两个特征属性：异质度分布与局部性。为理解这两个属性对 SAT 的影响，我们研究了可控制异质性与局部性的随机 k-SAT 模型的证明复杂性。我们的发现表明，仅异质性并不能使 SAT 变易，因为异质随机 k-SAT 实例具有超多项式的归结（resolution）大小。这意味着这些实例对现代 SAT 求解器而言是难处理的。另一方面，用底层几何建模局部性会导致小的不可满足子公式，并可在多项式时间内找到。关于几何随机 k-SAT 的结果的一个关键要素可在高阶 Voronoi 图的复杂性中找到。作为一项额外的技术贡献，我们给出了非空 Voronoi 区域数量的线性上界，该上界适用于非常一般设定下具有随机位置的点。特别地，它涵盖任意 p-范数、更高维度以及乘性地影响每点影响区域的权重。这与最坏情况下二次下界形成鲜明对比。
引用
@article{arxiv.2004.07319,
title = {The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability},
author = {Thomas Bläsius and Tobias Friedrich and Andreas Göbel and Jordi Levy and Ralf Rothenberger},
journal= {arXiv preprint arXiv:2004.07319},
year = {2021}
}
备注
53 pages, 2 figures