论文标题
基于逻辑的算法元元理论用于MIM宽度
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.基于[Bergougnoux和Kanté，ESA 2019; Sidma 2021]，我们表明，对于每个固定的$ \ Mathsf {a \＆c〜dn} $公式的模型检查问题可在$ n^{o（w）} $时间与输入图与MIM-Width $ W $的分支分解一起解决。在此框架中，几乎所有已知可以在多项式时间内解决的问题可以在多项式时间内解决。我们在此列表中添加了几个自然问题，包括提出各种解决方案的问题。只要输入图的给定分支分解就$ d $ - 纽伯格期等价（Bui-Xuan，Telle和Vatshelle，TCS 2013）而言，我们的模型检查算法都是有效的。因此，我们统一并扩展了已知的宽度，集团宽度和排名宽度的已知算法。我们的算法对这三个宽度测量值具有单指数的依赖性，并且渐近匹配几个问题的最快已知算法的运行时间。这导致在指数时间假设（$ \ mathsf {eth} $）下为树宽，集团宽度和排名宽度的算法带有紧张的运行时间；在$ \ mathsf {eth} $下，上述MIM宽度的运行时间几乎也很紧。我们的结果在逻辑的表达能力方面也很紧张：我们表明，逻辑的略有扩展使模型检查问题para-$ \ mathsf {np} $ - 当通过mim-width Plus formula长度参数化时，很难。
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é, 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.
