First Order Logic on Pathwidth Revisited Again

2025-05-06 0 0 650.01KB 25 页 10玖币

侵权投诉

Michael Lampis !

Université Paris-Dauphine, PSL University, CNRS, LAMSADE, 75016, Paris, France

Abstract

Courcelle’s celebrated theorem states that all MSO-expressible properties can be decided in

linear time on graphs of bounded treewidth. Unfortunately, the hidden constant implied by this

theorem is a tower of exponentials whose height increases with each quantiﬁer alternation in the

formula. More devastatingly, this cannot be improved, under standard assumptions, even if we

consider the much more restricted problem of deciding FO-expressible properties on trees.

In this paper we revisit this well-studied topic and identify a natural special case where the

dependence of Courcelle’s theorem can, in fact, be improved. Speciﬁcally, we show that all FO-

expressible properties can be decided with an elementary dependence on the input formula, if the

input graph has bounded pathwidth (rather than treewidth). This is a rare example of treewidth and

pathwidth having diﬀerent complexity behaviors. Our result is also in sharp contrast with MSO logic

on graphs of bounded pathwidth, where it is known that the dependence has to be non-elementary,

under standard assumptions. Our work builds upon, and generalizes, a corresponding meta-theorem

by Gajarský and Hliněný for the more restricted class of graphs of bounded tree-depth.

2012 ACM Subject Classiﬁcation

Theory of Computation

→

Design and Analysis of Algorithms

→Parameterized Complexity and Exact Algorithms

Keywords and phrases Algorithmic Meta-Theorems, FO logic, Pathwidth

Acknowledgements

This work is partially supported by the ANR project ANR-21-CE48-0022

(S-EX-AP-PE-AL).

1 Introduction

Algorithmic meta-theorems are general statements of the form “all problems in a certain class

are tractable on a particular class of inputs”. Probably the most famous and celebrated result

of this type is Courcelle’s theorem [

], which states that all graph properties expressible in

Monadic Second Order (MSO) logic are solvable in linear time on graphs of bounded treewidth.

This result has proved to be of immense importance to parameterized complexity theory,

because a vast collection of natural NP-hard problems can be expressed in MSO logic (and

its variations that allow optimization objectives [

]) and because treewidth is the most well-

studied structural graph parameter. Thanks to Courcelle’s theorem, we immediately obtain

that all such problems are ﬁxed-parameter tractable (FPT) parameterized by treewidth.

Despite its great success, Courcelle’s theorem suﬀers from a signiﬁcant weakness: the

algorithm it guarantees has a running time that is astronomical for most problems. Indeed, a

careful reading of the theorem shows that the running time increases as a tower of exponentials

whose height is equal to the number of quantiﬁer alternations of the input MSO formula.

Hence, even though Courcelle’s theorem shows that any MSO formula φcan be decided on

-vertex graphs of treewidth

in time

(

φ, tw

)

, the function

is non-elementary, that is,

it cannot be bounded from above by any tower of exponentials of ﬁxed height.

One could hope that this terrible dependence on

is an artifact of Courcelle’s proof

technique. Unfortunately, it was shown in a very inﬂuential work by Frick and Grohe [

]

that this non-elementary dependence on the number of quantiﬁers of

is best possible

(under standard assumptions), even if one considers the severely restricted special case of

model-checking First Order (FO) logic on trees. Recall that FO logic is a basic logic formalism

that allows us to express graph properties using quantiﬁcation over the vertices of the graph,

arXiv:2210.09899v1 [cs.DS] 18 Oct 2022

2 First Order Logic on Pathwidth Revisited Again

Parameter FO MSO

Treewidth Non-elementary on Trees [13] Non-elementary on Trees [13]

Pathwidth Elementary (Theorem 24) Non-elementary on Caterpillars [13]

Tree-depth Elementary [14] Elementary [14]

Table 1

Summary of the state of the art for FO and MSO model checking on graphs of bounded

treewidth, pathwidth, and tree-depth. Elementary (green cells) indicates that there is an algorithm

which, when the corresponding width is bounded by an absolute constant, decides any formula

time

(

)

nO(1)

, where

is a function that can be bounded above by a ﬁnite tower of exponentials.

For the remaining cases, this is known to be impossible, under standard assumptions, hence it is

inevitable to have an f(φ)that is a tower of exponentials whose height increases with φ.

while MSO logic also allows quantiﬁcation over sets of vertices. Since FO logic is trivially

a subset of MSO logic and trees have treewidth 1, this result established that Courcelle’s

theorem is essentially best possible.

Frick and Grohe’s lower bound thus provided the motivation for the search for subclasses

of bounded-treewidth graphs where avoiding the non-elementary dependence on

may

be possible. The obvious next place to look was naturally, pathwidth, which is the most

well-known restriction (and close cousin) of treewidth. Unfortunately, Frick and Grohe’s

paper provided a negative result for MSO model checking also for this parameter. More

precisely, they showed that MSO model checking on strings with a total order relation has a

non-elementary dependence on the formula (unless P=NP), but such structures can easily

be embedded into caterpillars (which are graphs of pathwidth 1) if one allows quantiﬁcation

over sets. Notice, however, that this does not settle the complexity of FO logic for graphs of

counstant pathwidth, as it is not clear how one could implement the total ordering relation

of a string without access to set quantiﬁers (we expand on this question further below).

On the positive side, Frick and Grohe’s lower bounds motivated the discovery of sev-

eral meta-theorems with elementary dependence on the formula for other, more restricted

variations of treewidth (we review some such results below). Of all these results, the one

that is “closest” to treewidth, is the theorem of Gajarský and Hliněný [

], which states

that on graphs of constant tree-depth, MSO (and hence FO) model checking has elementary

dependence on the input formula. It is known that for all

-vertex graphs

we have

(

)

≤pw

(

)

≤td

(

)

≤tw

(

)

log n

, where

tw,pw,td

denote the treewidth, pathwidth

and tree-depth. In a sense, this positive result seemed to go as far as one could possibly go

towards emulating treewidth, while retaining the elementary dependence on the formula and

avoiding the lower bound of Frick and Grohe. This state of the art is summarized in Table 1.

Our result

In this paper we revisit this well-studied topic and address the one remaining

case of Table 1 where it is still unknown whether it is possible to obtain an elementary

dependence on the formula for model checking. We answer this question positively, showing

that if we restrict ourselves to graphs of pathwidth

, where

is an absolute constant, then

FO formulas with

quantiﬁers can be decided in time

(

)

nO(1)

, where

is an elementary

function of

. More precisely, the function

is at most a tower of exponentials of height

(

). In other words, our result trades the non-elementary dependence on

which is inherent

in Courcelle’s theorem, with a non-elementary dependence on

. Though this may seem

disappointing at ﬁrst, it is known that this is the best one could have hoped for. In fact,

the meta-theorem of [

] also has this behavior (its parameter dependence is a tower of

exponentials whose height increases with the tree-depth), and it was shown in [

] that this is

best possible (under standard assumptions). Since pathwidth is a more general parameter, we

Michael Lampis 3

cannot evade this lower bound and our algorithm needs to have a non-elementary dependence

on pathwidth, if its dependence on the formula is elementary.

The result we obtain is, therefore, in a sense best possible and ﬁlls a natural gap in

our knowledge regarding FO model checking for a well-studied graph width. Beyond ﬁlling

this gap, the fact that we are able to give a positive answer to this question and obtain an

algorithm with “good” dependence on the formula is interesting, and perhaps even rather

striking, for several reasons. First, in many cases in this domain, it is impossible to obtain

an elementary dependence on

, no matter how much we are willing to sacriﬁce on our

dependence on the graph width, as demonstrated by the fact that the lower bounds of Table 1

apply for classes with the smallest possible width (trees and caterpillars). Second, even

though FO seems much weaker than MSO in general, the complexities of model checking

the two logics seem to be similar (that is, at most one level of exponentiation apart) for

most parameters (we review some further examples below). Indeed, a main contribution

of [

] was to prove that for graphs of bounded tree-depth, the two logics are actually

equivalent. It is therefore somewhat unusual (for this context) that for pathwidth FO has

quite diﬀerent complexity from MSO logic. Third, even though treewidth and pathwidth are

arguably the two most well-studied graph widths in parameterized complexity, by and large

the complexities of the vast majority of problems are the same for both parameters (for more

information on this, see [

] which only recently discovered the ﬁrst example of a natural

problem separating the two parameters). It is therefore remarkable that the complexity of

FO model checking is so diﬀerent for pathwidth and treewidth.

Finally, one aspect of our result that makes it more surprising is that it does not seem to

generalize to dense graphs. Meta-theorems that give a non-elementary dependence on the

formula by using a restriction of treewidth, generally have a dense graph analogue, using a

restriction of clique-width (the dense graph analogue of treewidth). Indeed, this is the case

for vertex cover [

] (neighborhood diversity [

], twin cover [

]) but also for tree-depth

(shrub-depth [

]). One may have expected something similar to hold in our case. However,

the natural dense analogue of pathwidth is linear clique-width and it is already known that

FO logic has a non-elementary dependence on threshold graphs [

]. Since threshold graphs

have linear clique-width 2, we cannot hope to extend our result to this parameter and it

appears that the positive result of this paper is an isolated island of “tractability”.

High-level proof overview

Our technique extends and builds upon the meta-theorem of

[

] which handles the more restricted case of graphs of bounded tree-depth. We recall

that the heart of this meta-theorem is the basic observation that FO logic has bounded

counting power: if our graph contains

+ 1 identical parts (for some appropriate deﬁnition of

“identical”), then deleting one cannot aﬀect the validity of any FO formula with

quantiﬁers.

The approach of [

] is to partition the vertices of the graph depending on their height in

the tree-depth decomposition, then identify (and delete) identical vertices in the bottom

level. This bounds the degree of vertices one level up, which allows us to partition them

into a bounded number of types, delete components of the same type if we have too many,

hence bound the degree of vertices one level up, and so on until the size of the whole graph

is bounded.

Our approach borrows much of this general strategy: we will appropriately rank the

vertices of the graph and then move from lower to higher ranks, at each step bounding the

maximum degree of any vertex of the current rank. Besides the fact that ranking vertices

into levels is less obvious when given a path decomposition, rather than a tree of ﬁxed height,

the main diﬃculty we encounter is that no matter where we start, we cannot in general easily

4 First Order Logic on Pathwidth Revisited Again

ﬁnd identical parts where something can be safely deleted. Intuitively, this is demonstrated

by the contrast between the simplest bounded tree-depth graph (a star, where leaves are

twins, hence one can easily delete one if we have at least

+ 1) and the simplest bounded

pathwidth graph (a path, which contains no twins). In order to handle this more general

case, we need to combine the previous approach with arguments that rely on the locality of

FO logic.

To understand informally what we mean by this, recall the classical argument which

proves that Reachability is not expressible in FO logic. One way this is proved, is to show

that a graph

which is a long path (of say, 4

vertices) and a graph

which is a union of

a path and a cycle (of say, 2

q−1

vertices each) are indistinguishable for FO formulas with

quantiﬁers. Our strategy is to ﬂip this argument: if we are asked to model check a formula

on a long path, we might as well model check the same formula on a simpler (less connected)

graph which contains a shorter path and a cycle. Of course, our input graphs will be more

complicated than long paths; we will, however, be dealing with long path-like structures, as

our graph has small pathwidth. Our strategy is to perform a surgical rewiring operation

on the path decomposition, producing the union of a shorter decomposition and a ring-like

structure, while still satisfying the same formulas (the reader may skip ahead to Figure 1

to get a feeling for this operation). In other words, the main technical ingredient of our

algorithm is inspired by (and exploits) a classical impossibility result on the expressiveness of

FO logic. The abstract idea is (in a rough sense) to apply this argument repeatedly, so that

if we started with a long path decomposition, we end up with a short path decomposition

and many “disconnected rings”. Eventually, we will be able to produce some such rings which

are identical, delete them, and simplify the graph.

There are, of course, now various technical diﬃculties we need to overcome in order to

turn this intuition into a precise argument. First, when we cut at two points in the path

decomposition to extract the part that will form the “ring”, we need to make sure that at an

appropriate radius around the cut points the decompositions are isomorphic. It is not hard

to calculate the appropriate radius we need in the graph (it is known that

-quantiﬁer FO

formulas depend on balls of radius roughly 2

), but a priori two vertices which are close in

the graph could be far in the path decomposition. To handle this, we take care when we

rank the vertices, so that vertices of lower rank are guaranteed to only appear in a bounded

number of bags, hence distances in the path decomposition approximate distances in the

graph. Second, we need to calculate how long our decomposition needs to be before we

can guarantee that we will be able to ﬁnd some appropriate cut points. Here we use some

counting arguments and pigeonhole principle to show that a path decomposition with length

double-exponential in the desired radius is suﬃcient. Finally, once we ﬁnd suﬃciently many

points to rewire and produce suﬃciently many “rings”, we need to prove that this did not

aﬀect the validity of the formula. Then, we are free to delete one, using the same argument

as [

] and obtain a smaller equivalent graph. In the end, once we can no longer repeat this

process, we obtain a bounded-degree graph, where it is known that FO model checking has

an elementary dependence on the formula.

Overall, even though the algorithm we present seems somewhat complicated, the basic

ingredients are simple and well-known: the fact that deleting one of many identical parts

does not aﬀect the validity of the formula (which is also used in [

]); the fact that FO

formulas are not aﬀected if we edit the graph in a way that preserves balls of a small radius

around each vertex; and simple counting arguments and the pigeonhole principle.

Michael Lampis 5

Paper Organization

We conclude this section below with a short overview of other related

work on algorithmic meta-theorems and continue in Section 2 with deﬁnitions and notation.

The rest of the paper is organized as follows:

In Section 3 we present two lemmas, which are standard facts on FO logic, with minor

adjustments to our setting. In particular, in Section 3.1 we present the lemma that states

that if we have

+ 1 identical parts, it is safe to delete one; and in Section 3.2 we present

the lemma that states that if two graphs agree on the local extended neighborhoods

around each vertex (for some appropriate radius), then they satisfy the same formulas

(that is, FO logic is local). Since these facts are standard, the reader may wish to skip the

proofs of Section 3, which are given for the sake of completeness, during a ﬁrst reading.

Then, in Section 4 we present the speciﬁc tools we will use to simplify our graph. In

Section 4.1 we explain how we rank the vertices of a path decomposition so that each

vertex has few neighbors of higher rank (but possibly many neighbors of lower rank).

This allows us to process the ranks from lower to higher, simplifying the graph step by

step. Then, in Section 4.2 we use some counting arguments to calculate the length of a

path decomposition that guarantees the existence of long isomorphic blocks, on which

we will apply the rewiring operation. We also show how distances in the graph can be

approximated by distances in the path decomposition, if we have bounded the number

of occurrences of each vertex in the decomposition. Finally, in Section 4.3 we formally

deﬁne the rewiring operation and show that if the points where we apply it are in the

middle of suﬃciently long isomorphic blocks of the decomposition, this operation is safe.

We also show that the “rings” it produces can be considered identical, in a sense that

will allow us to invoke the lemma of Section 3.1 and delete one.

We put everything together in Section 5, where we explain how the lemmas we have

presented form parts of an algorithm that ranks the vertices of a graph supplied with

a path decomposition and then processes ranks one by one, decreasing the number of

occurences of each vertex in the decomposition without aﬀecting the validity of any

formula (with

quantiﬁers). In the end, the processed graph has bounded degree and we

invoke known results to decide the formula.

Other related work

Algorithmic meta-theorems are a very well-studied topic in param-

eterized complexity ([

]) and much work has been devoted in improving and extending

Courcelle’s theorem. Among such results, we mention the generalization of this theorem

to MSO for clique-width, which covers dense graphs [

]. For FO logic, ﬁxed-parameter

tractability can be extended to much wider classes of graphs, with the recently introduced

notion of twin-width nicely capturing many results in the area [

]. Of course,

since all these classes include the class of all trees, the non-elementary dependence on the

formula implied by the lower bound of [

] still applies. Meta-theorems have also been

given for logics other than FO and MSO, with the goal of either targeting a wider class of

problems [

], or achieving better complexity [

]. Kernelization [

] and

approximation [8] are also topics where meta-theorems have been studied.

The meta-theorems which are more relevant to the current work are those which explicitly

try to improve upon the parameter dependence given by Courcelle, by considering more

restricted parameters. We mention here the meta-theorems for vertex cover, max-leaf, and

neighborhood diversity [

], twin-cover [

], shrub-depth [

], and vertex integrity [

]. As

mentioned, one common aspect of these meta-theorems is that they handle both FO and

MSO logic, without a huge diﬀerence in complexity (at most one extra level of exponentiation

in the parameter dependence), which makes the behavior of FO logic on treewidth somewhat

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

FirstOrderLogiconPathwidthRevisitedAgainMichaelLampis!UniversitéParis-Dauphine,PSLUniversity,CNRS,LAMSADE,75016,Paris,FranceAbstractCourcelle'scelebratedtheoremstatesthatallMSO-expressiblepropertiescanbedecidedinlineartimeongraphsofboundedtreewidth.Unfortunately,thehiddenconstantimpliedbythistheorem...

展开>> 收起<<

First Order Logic on Pathwidth Revisited Again.pdf

共25页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

First Order Logic on Pathwidth Revisited Again

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: