  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\"{a}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\"{a}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.
