Deciding first-order properties of locally tree-decomposable structures
Deciding first-order properties of locally tree-decomposable structures
复制标题
DOI：
10.1145/504794.504798
复制
发表时间：
2000-04
期刊：
影响因子：
--
通讯作者：
Markus Frick;Martin Grohe
中科院分区：
文献类型：
--
作者：
Markus Frick;Martin Grohe
我们引入了一类图的概念，或者更一般地说，关系结构，是局部树可分解的。有许多局部树可分解类的例子，其中包括平面图类和所有有界价或有界树宽的类。我们还考虑了一类具有有界局部树宽的结构的更一般的概念，证明了对于在一阶逻辑中可定义的结构的每一个性质φ和对于每一个局部树可分解的结构类C，存在一个判定给定结构A ∈ C是否具有性质φ的线性时间算法。对于局部树宽有界的类C，我们证明了对每个k ≥ 1，存在一个算法在O（n1+（1/k））时间内解决同一问题（其中n是输入结构的基数）.
We introduce the concept of a class of graphs, or more generally, relational structures, being locally tree-decomposable. There are numerous examples of locally tree-decomposable classes, among them the class of planar graphs and all classes of bounded valence or of bounded tree-width. We also consider a slightly more general concept of a class of structures having bounded local tree-width.We show that for each property φ of structures that is definable in first-order logic and for each locally tree-decomposable class C of structures, there is a linear time algorithm deciding whether a given structure A ∈ C has property φ. For classes C of bounded local tree-width, we show that for every k ≥ 1 there is an algorithm solving the same problem in time O(n1+(1/k)) (where n is the cardinality of the input structure).