SAT后门：深度节拍大小
SAT Backdoors: Depth Beats Size
摘要：
几十年来，人们一直致力于寻找一类可满足性可以在多项式时间内判定的CNF公式。经典的结果是Horn公式（Aspvall，Plass和Tarjan，1979）和Krom（即，2CNF）公式（Dowling和Gallier，1984）。由Williams Gomes和Selman（2003）引入的后门，逐渐将这样一个易于处理的类扩展到所有与该类有界距离的公式。后门大小提供了一个公式和易处理类之间的自然但相当粗糙的距离度量。后门深度由Mählmann，Siebertz和Vigny（2021）引入，是一种更精确的距离度量，它允许并行使用不同的后门变量。有界后门大小意味着有界后门深度，但存在常数后门深度和任意大后门大小的公式。我们提出FPT近似算法计算后门深度到类霍恩和克罗姆。这导致了一个线性时间算法，用于确定这些类的有界后门深度公式的可满足性。我们基于我们的FPT近似算法上一个复杂的概念的障碍，扩展Mählmann等人。的障碍树的各种方式，包括增加分离障碍。我们通过一个新的博弈论框架，简化了后门的推理算法。最后，我们表明，有界后门深度捕获不易处理类CNF公式没有捕获任何已知的方法。
英文摘要：
For several decades, much effort has been put into identifying classes of CNF formulas whose satisfiability can be decided in polynomial time. Classic results are the linear-time tractability of Horn formulas (Aspvall, Plass, and Tarjan, 1979) and Krom (i.e., 2CNF) formulas (Dowling and Gallier, 1984). Backdoors, introduced by Williams Gomes and Selman (2003), gradually extend such a tractable class to all formulas of bounded distance to the class. Backdoor size provides a natural but rather crude distance measure between a formula and a tractable class. Backdoor depth, introduced by Mählmann, Siebertz, and Vigny (2021), is a more refined distance measure, which admits the utilization of different backdoor variables in parallel. Bounded backdoor size implies bounded backdoor depth, but there are formulas of constant backdoor depth and arbitrarily large backdoor size. We propose FPT approximation algorithms to compute backdoor depth into the classes Horn and Krom. This leads to a linear-time algorithm for deciding the satisfiability of formulas of bounded backdoor depth into these classes. We base our FPT approximation algorithm on a sophisticated notion of obstructions, extending Mählmann et al.'s obstruction trees in various ways, including the addition of separator obstructions. We develop the algorithm through a new game-theoretic framework that simplifies the reasoning about backdoors. Finally, we show that bounded backdoor depth captures tractable classes of CNF formulas not captured by any known method.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
