For a fixed "pattern" graph G, the \textit{colored} G\textit{-subgraph isomorphism problem} (denoted \mathrm{SUB}(G)) asks, given an n-vertex graph H and a coloring V(H) \to V(G), whether H contains a properly colored copy of G. The complexity of this problem is tied to parameterized versions of \mathit{P} {=}? \mathit{NP} and \mathit{L} {=}? \mathit{NL}, among other questions. An overarching goal is to understand the complexity of \mathrm{SUB}(G), under different computational models, in terms of natural invariants of the pattern graph G.
In this paper, we establish a close relationship between the \textit{formula complexity} of \mathrm{SUB} and an invariant known as \textit{tree-depth} (denoted \mathrm{td}(G)). \mathrm{SUB}(G) is known to be solvable by monotone \mathit{AC^0} formulas of size O(n^{\mathrm{td}(G)}). Our main result is an n^{\tilde\Omega(\mathrm{td}(G)^{1/3})} lower bound for formulas that are monotone \textit{or} have sub-logarithmic depth. This complements a lower bound of Li, Razborov and Rossman (SICOMP 2017) relating tree-width and \mathit{AC^0} circuit size. As a corollary, it implies a stronger homomorphism preservation theorem for first-order logic on finite structures (Rossman, ITCS 2017).
The technical core of this result is an n^{\Omega(k)} lower bound in the special case where G is a complete binary tree of height k, which we establish using the \textit{pathset framework} introduced in (Rossman, SICOMP 2018). (The lower bound for general patterns follows via a recent excluded-minor characterization of tree-depth (Czerwi\'nski et al, arXiv:1904.13077).) Additional results of this paper extend the pathset framework and improve upon both, the best known upper and lower bounds on the average-case formula size of \mathrm{SUB}(G) when G is a path.