SAT 后门：深度胜过规模

数十年来，人们投入大量努力识别其可满足性可在多项式时间内判定的 CNF 公式类。经典结果包括 Horn 公式（Aspvall、Plass 和 Tarjan，1979）与 Krom（即 2CNF）公式（Dowling 和 Gallier，1984）的线性时间可处理性。由 Williams、Gomes 和 Selman（2003）引入的后门，将此类可处理类逐步扩展到与该类别有有界距离的所有公式。后门规模提供了公式与可处理类之间自然但相当粗糙的距离度量。由 M"{a}hlmann、Siebertz 和 Vigny（2021）引入的后门深度是一种更精细的距离度量，允许并行使用不同后门变量。有界后门规模蕴含 bounded 后门深度，但存在常后门深度且后门规模任意大的公式。我们提出 FPT 近似算法来计算到 Horn 与 Krom 类的后门深度。这导出了判定这些类中具有界后门深度公式可满足性的线性时间算法。我们的 FPT 近似算法基于一种复杂的阻碍概念，以多种方式推广 M"{a}hlmann 等人的阻碍树，包括添加分隔阻碍。我们通过一个新的博弈论框架来开发该算法，简化了关于后门的推理。最后，我们表明有界后门深度捕获了任何已知方法都未捕获的可处理 CNF 公式类。