A logic-based algorithmic meta-theorem for mim-width

We introduce a logic called distance neighborhood logic with acyclicity and connectivity constraints ($\mathsf{A\&C~DN}$ for short) which extends existential $\mathsf{MSO_1}$ with predicates for querying neighborhoods of vertex sets and for verifying connectivity and acyclicity of vertex sets in various powers of a graph. Building upon [Bergougnoux and Kant\'e, ESA 2019; SIDMA 2021], we show that the model checking problem for every fixed $\mathsf{A\&C~DN}$ formula is solvable in $n^{O(w)}$ time when the input graph is given together with a branch decomposition of mim-width $w$. Nearly all problems that are known to be solvable in polynomial time given a branch decomposition of constant mim-width can be expressed in this framework. We add several natural problems to this list, including problems asking for diverse sets of solutions. Our model checking algorithm is efficient whenever the given branch decomposition of the input graph has small index in terms of the $d$-neighborhood equivalence [Bui-Xuan, Telle, and Vatshelle, TCS 2013]. We therefore unify and extend known algorithms for tree-width, clique-width and rank-width. Our algorithm has a single-exponential dependence on these three width measures and asymptotically matches run times of the fastest known algorithms for several problems. This results in algorithms with tight run times under the Exponential Time Hypothesis ($\mathsf{ETH}$) for tree-width, clique-width and rank-width; the above mentioned run time for mim-width is nearly tight under the $\mathsf{ETH}$ for several problems as well. Our results are also tight in terms of the expressive power of the logic: we show that already slight extensions of our logic make the model checking problem para-$\mathsf{NP}$-hard when parameterized by mim-width plus formula length.