Deciding first-order properties for sparse graphs

被引:45
作者
Dvorak, Zdenek [1 ,3 ]
Kral', Daniel [1 ,3 ]
Thomas, Robin [2 ]
机构
[1] Charles Univ Prague, Dept Appl Math, Malostranske Namesti 25, CR-11800 Prague, Czech Republic
[2] Georgia Inst Technol, Sch Mat, Atlanta, GA 30332 USA
[3] Charles Univ Prague, Fac Math & Phys, Inst Theoret Comp Sci, Prague 11800, Czech Republic
来源
2010 IEEE 51ST ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE | 2010年
关键词
algorithmic metatheorems; graphs with bounded expansion; graphs with bounded degree; minor-closed classes of graphs; graphs with locally bounded tree-width; BOUNDED EXPANSION; GRAD;
D O I
10.1109/FOCS.2010.20
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present a linear-time algorithm for deciding first-order logic (FOL) properties in classes of graphs with bounded expansion. Many natural classes of graphs have bounded expansion: graphs of bounded tree-width, all proper minor-closed classes of graphs, graphs of bounded degree, graphs with no subgraph isomorphic to a subdivision of a fixed graph, and graphs that can be drawn in a fixed surface in such a way that each edge crosses at most a constant number of other edges. We also develop an almost linear-time algorithm for deciding FOL properties in classes of graphs with locally bounded expansion; those include classes of graphs with locally bounded tree-width or locally excluding a minor. More generally, we design a dynamic data structure for graphs belonging to a fixed class of graphs of bounded expansion. After a linear-time initialization the data structure allows us to test an FOL property in constant time, and the data structure can be updated in constant time after addition/deletion of an edge, provided the list of possible edges to be added is known in advance and their addition results in a graph in the class. In addition, we design a dynamic data structure for testing existential properties or the existence of short paths between prescribed vertices in such classes of graphs. All our results also hold for relational structures and are based on the seminal result of Nesetril and Ossona de Mendez on the existence of low tree-depth colorings.
引用
收藏
页码:133 / 142
页数:10
相关论文
共 28 条
[1]   THE MONADIC 2ND-ORDER LOGIC OF GRAPHS .1. RECOGNIZABLE SETS OF FINITE GRAPHS [J].
COURCELLE, B .
INFORMATION AND COMPUTATION, 1990, 85 (01) :12-75
[2]  
Dawar A., P LICS 07, P270
[3]  
Dawar A., 2009, EL C COMP COMPL
[4]  
Dvorak Z., 3 COLORING TRI UNPUB
[5]  
Dvorak Z., 2009, LNCS, V5911, P17
[6]  
Dvorák Z, 2009, PROCEEDINGS OF THE TWENTIETH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, P1176
[7]  
Dvorák Z, 2009, PROCEEDINGS OF THE TWENTIETH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, P120
[8]  
Eppstein D., 1999, Journal of Graph Algorithms and Applications, V3
[9]   Diameter and treewidth in minor-closed graph families [J].
Eppstein, D .
ALGORITHMICA, 2000, 27 (3-4) :275-291
[10]  
Eppstein D., P SODA 95, P632