基于公式长度的 SAT 进一步改进

本文证明一般 CNF 可满足性问题可在 $O^*(1.0638^L)$ 时间内求解，其中 $L$ 为输入 CNF 公式的长度（即公式中文字的总数），这改进了 2009 年得到的 $O^*(1.0652^L)$ 的先前结果。我们的算法使用 measure-and-conquer 方法进行分析。我们的改进主要归因于以下两点：我们仔细设计分支规则以处理 5 度与 4 度变量，从而避免先前的瓶颈；我们证明某些最坏情况不会总发生，进而可使用均摊技术获得进一步改进。在我们的分析中，我们提供了若干用于分析的一般框架以及关于度量减少量的一些下界，以简化论证。这些技术可用于分析更多基于 measure-and-conquer 方法的算法。