理解 SLS 算法的长尾运行时间

可满足性问题（SAT）是计算机科学中最著名的问题之一。其 NP 完全性被用来论证 SAT 是难解的。然而，已有巨大进展使得 SAT 求解器能够求解具有数百万变量的实例。一个特别成功的范式是随机局部搜索（SLS）。在大多数情况下，存在不同的方式来表述底层问题。虽然已知这会影响求解器的运行时间，但找到有用的表述通常并非易事。最近提出的 GapSAT 求解器 [Lorenz and Wörz 2020] 展示了一种成功的方法，通过学习从原问题逻辑蕴含的附加信息，平均上改进了 SLS 求解器的性能。尽管如此，仍存在性能轻微恶化的情况。这证明了有必要深入研究学习逻辑蕴涵如何影响 SLS 的运行时间。在这项工作中，我们提出了一种生成逻辑等价问题表述的方法，推广了 GapSAT 的思想。这使得能够对 SLS 求解器运行时间上的影响进行严格的数学研究。若将修改过程视为随机的，Johnson SB 分布对难度给出了完美的刻画。由于观测到的 Johnson SB 分布趋近于对数正态分布，我们的分析也表明难度是长尾的。作为第二项贡献，我们从理论上证明了重启对于长尾分布是有用的。这意味着额外的重启可进一步改进所有采用上述修改技术的算法。由于实证研究有力地表明运行时间分布遵循 Johnson SB 分布，我们对此性质进行了理论研究。我们成功证明了 Schöning 随机游走算法的运行时间近似为 Johnson SB 分布。