First Order Logic and Twin-Width in Tournaments and Dense Oriented Graphs

TL;DR

The paper addresses FO model checking on hereditary classes of tournaments, establishing that the problem is FPT exactly when the class has bounded twin-width, and AW[*]-hard otherwise; bounded twin-width aligns with NIP and at most exponential growth, while unbounded twin-width yields factorial growth and the capacity to interpret all graphs. The authors develop a polynomial-time method based on binary search tree orders to witness or certify bounded twin-width, and, when necessary, extract canonical obstructions encoding permutations (F_=, F_≤, F_≥) via Ramsey arguments. These obstructions underpin the main equivalences and enable an FPT twin-width approximation via a witness-based contraction process. The framework extends to oriented graphs with bounded independence and to binary relational structures augmented by fixed binary relations, unifying and generalizing prior results for ordered graphs and offering a robust toolkit for FO model checking in dense directed settings.

Abstract

We characterise the classes of tournaments with tractable first-order model checking. For every hereditary class of tournaments $\mathcal T$, first-order model checking is either fixed parameter tractable or $\textrm{AW}[*]$-hard. This dichotomy coincides with the fact that $\mathcal T$ has either bounded or unbounded twin-width, and that the growth of $\mathcal T$ is either at most exponential or at least factorial. From the model-theoretic point of view, we show that NIP classes of tournaments coincide with bounded twin-width. Twin-width is also characterised by three infinite families of obstructions: $\mathcal T$ has bounded twin-width if and only if it excludes at least one tournament from each family. This generalises results of Bonnet et al.\ on ordered graphs. The key for these results is a polynomial time algorithm that takes as input a tournament $T$ and computes a linear order $<$ on $V(T)$ such that the twin-width of the birelation $(T,<)$ is at most some function of the twin-width of $T$. Since approximating twin-width can be done in polynomial time for an ordered structure $(T,<)$, this provides a polynomial time approximation of twin-width for tournaments. Our results extend to oriented graphs with stable sets of bounded size, which may also be augmented by arbitrary binary relations.

Figures (7)

• Figure 1: The three classes of obstructions to twin-width in tournaments. For readability, edges oriented from some $y_j$ to some $x_i$ have been omitted. Each class consists of some encoding of the class of all permutations, represented here with the permutation $\sigma = 31452$.
• Figure 2: A binary search tree in a tournament. The direction of omitted edges is not constrained.
• Figure 3: Example of construction of the quasi-order $\preceq_C^+$. The quasi-order is from left to right, and the triangles are equivalence classes. The direction of omitted edges (from $B_i$ to $B_j \cup \{c_j\}$ for $i < j$) is not constrained. For $\preceq_C^-$, the direction of all edges would be reversed.
• Figure 4: Sketch of the proof of \ref{['lem:bst-partition-extraction']}. In the upper half, the BST $T$ with the extracted branch $B$; circled in blue, the extracted subsequence $b_{i_\ell}$; in green arrows, the chain $C = B \cap L = \{b_2,b_4,b_5,b_6\}$. Below the tree, from top to bottom: the partition in $L'_\ell$ and $R'_\ell$; the initial family (here partition) $\mathcal{P}$, with the parts contained in some $L'_\ell$ or $R'_\ell$ highlighted; the final family $\mathcal{P}'$, obtained by selecting a part of $\mathcal{P}$ inside each possible $L'_\ell$.
• Figure 5: Chain representation of the matrix $M$ of the permutation $31452$. Vertices of $A$ are ordered bottom to top by a chain order $\preceq^+_{C_A}$, and similarly for $B$. Edges oriented from $A$ to $B$ correspond to '1's in $M$. For readability, edges from $B$ to $A$ (corresponding to '0's) are not drawn. The other omitted edges are unconstrained.

Theorems & Definitions (78)

• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Lemma 1.3
• Theorem 1.4
• Theorem 1.5
• Lemma 2.1
• proof
• Lemma 2.2
• proof