Author name cluster

Jan Dreier

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

1 author row

STOC Conference 2025 Conference Paper

Merge-Width and First-Order Model Checking

Jan Dreier
Szymon Torunczyk

We introduce merge-width , a family of graph parameters that unifies several structural graph measures, including treewidth, degeneracy, twin-width, clique-width, and generalized coloring numbers. Our parameters are based on new decompositions called construction sequences . These are sequences of ever coarser partitions of the vertex set, where each pair of parts has a specified default connection, and all vertex pairs of the graph that differ from the default are marked as resolved . The radius- r merge-width is the maximum number of parts reached from a vertex by following a path of at most r resolved edges. Graph classes of bounded merge-width – for which the radius- r merge-width parameter can be bounded by a constant, for each fixed r =1,2,3,… – include all classes of bounded expansion or of bounded twin-width, thus unifying two central notions from the Sparsity and Twin-width frameworks. Furthermore, they are preserved under first-order transductions, which attests to their robustness. We conjecture that classes of bounded merge-width are equivalent to the previously introduced classes of bounded flip-width. As our main result, we show that the model checking problem for first-order logic is fixed-parameter tractable on graph classes of bounded merge-width, assuming the input includes a witnessing construction sequence. This unites and extends two previous model checking results: the result of Dvorak, Kral, and Thomas for classes of bounded expansion, and the result of Bonnet, Kim, Thomasse, and Watrigant for classes of bounded twin-width. Finally, we suggest future research directions that could impact the study of structural and algorithmic graph theory, in particular of monadically dependent graph classes, which we conjecture to coincide with classes of almost bounded merge-width .

Details

FOCS Conference 2024 Conference Paper

First-Order Model Checking on Monadically Stable Graph Classes

Jan Dreier
Ioannis Eleftheriadis
Nikolas Mählmann
Rose McCarty
Michal Pilipczuk
Szymon Torunczyk

A graph class $\mathscr{C}$ is called monadically stable if one cannot interpret, in first-order logic, arbitrary large linear orders in colored graphs from $\mathscr{C}$. We prove that the model checking problem for first-order logic is fixed-parameter tractable on every monadically stable graph class. This extends the results of [Grohe, Kreutzer, Siebertz; J. ACM '17] for nowhere dense classes and of [Dreier, Mählmann, Siebertz; STOC '23] for structurally nowhere dense classes to all monadically stable classes. This result is complemented by a hardness result showing that monadic stability is precisely the dividing line between tractability and intractability of first-order model checking on hereditary classes that are edge-stable: exclude some half-graph as a semi-induced subgraph. Precisely, we prove that for every hereditary graph class $\mathscr{C}$ that is edge-stable but not monadically stable, first-order model checking is $\text{AW}[*]$ -hard on $\mathscr{C}$, and W[1]-hard when restricted to existential sentences. This confirms, in the special case of edge-stable classes, an open conjecture that the notion of monadic dependence delimits the tractability of first-order model checking on hereditary classes of graphs. For our tractability result, we first prove that monadically stable graph classes have almost linear neighborhood complexity, by combining tools from stability theory and from sparsity theory. We then use this result to construct sparse neighborhood covers for monadically stable graph classes, which provides the missing ingredient for the algorithm of [Dreier, Mählmann, Siebertz; STOC '23]. The key component of this construction is the usage of orders with low crossing number [Welzl; SoCG '88], a tool from the area of range queries. For our hardness result, we first prove a new characterization of monadically stable graph classes in terms of forbidden induced subgraphs. We then use this characterization to show that in hereditary classes that are edge-stable but not monadically stable, one can efficiently interpret the class of all graphs using only existential formulas; this implies W[1]-hardness of model checking already for existential formulas.

Details

STOC Conference 2024 Conference Paper

Flip-Breakability: A Combinatorial Dichotomy for Monadically Dependent Graph Classes

Jan Dreier
Nikolas Mählmann
Szymon Torunczyk

A conjecture in algorithmic model theory predicts that the model-checking problem for first-order logic is fixed-parameter tractable on a hereditary graph class if and only if the class is monadically dependent. Originating in model theory, this notion is defined in terms of logic, and encompasses nowhere dense classes, monadically stable classes, and classes of bounded twin-width. Working towards this conjecture, we provide the first two combinatorial characterizations of monadically dependent graph classes. This yields the following dichotomy. On the structure side, we characterize monadic dependence by a Ramsey-theoretic property called flip-breakability. This notion generalizes the notions of uniform quasi-wideness, flip-flatness, and bounded grid rank, which characterize nowhere denseness, monadic stability, and bounded twin-width, respectively, and played a key role in their respective model checking algorithms. Natural restrictions of flip-breakability additionally characterize bounded treewidth and cliquewidth and bounded treedepth and shrubdepth. On the non-structure side, we characterize monadic dependence by explicitly listing few families of forbidden induced subgraphs. This result is analogous to the characterization of nowhere denseness via forbidden subdivided cliques, and allows us to resolve one half of the motivating conjecture: First-order model checking is AW[*]-hard on every hereditary graph class that is monadically independent. The result moreover implies that hereditary graph classes which are small, have almost bounded twin-width, or have almost bounded flip-width, are monadically dependent. Lastly, we lift our result to also obtain a combinatorial dichotomy in the more general setting of monadically dependent classes of binary structures.

Details

SODA Conference 2023 Conference Paper

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

Benjamin Bergougnoux
Jan Dreier
Lars Jaffke

We introduce a logic called distance neighborhood logic with acyclicity and connectivity constraints (A&C DN for short) which extends existential MSO 1 with predicates for querying neighborhoods of vertex sets in various powers of a graph and for verifying connectivity and acyclicity of vertex sets. Building upon [Bergougnoux and Kante, ESA 2019; SIDMA 2021], we show that the model checking problem for every fixed 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 (ETH) for tree-width, clique-width and rank-width; the above mentioned run time for mim-width is nearly tight under the 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-NP-hard when parameterized by mim-width plus formula length. * The full version of the paper can be accessed at https: //arxiv. org/abs/2202. 13335. This research is part of a project that has received funding from the Research Council of Norway Grant Agreement 274526 (LJ).

Details

STOC Conference 2023 Conference Paper

First-Order Model Checking on Structurally Sparse Graph Classes

Jan Dreier
Nikolas Mählmann
Sebastian Siebertz

A class of graphs is structurally nowhere dense if it can be constructed from a nowhere dense class by a first-order transduction. Structurally nowhere dense classes vastly generalize nowhere dense classes and constitute important examples of monadically stable classes. We show that the first-order model checking problem is fixed-parameter tractable on every structurally nowhere dense class of graphs. Our result builds on a recently developed game-theoretic characterization of monadically stable graph classes. As a second key ingredient of independent interest, we provide a polynomial-time algorithm for approximating weak neighborhood covers (on general graphs). We combine the two tools into a recursive locality-based model checking algorithm. This algorithm is efficient on every monadically stable graph class admitting flip-closed sparse weak neighborhood covers, where flip-closure is a mild additional assumption. Thereby, establishing efficient first-order model checking on monadically stable classes is reduced to proving the existence of flip-closed sparse weak neighborhood covers on these classes -- a purely combinatorial problem. We complete the picture by proving the existence of the desired covers for structurally nowhere dense classes: we show that every structurally nowhere dense class can be sparsified by contracting local sets of vertices, enabling us to lift the existence of covers from sparse classes.

Details

SODA Conference 2021 Conference Paper

Approximate Evaluation of First-Order Counting Queries

Jan Dreier
Peter Rossmanith

Kuske and Schweikardt introduced the very expressive first-order counting logic FOC( P ) to model database queries with counting operations. They showed that there is an efficient model-checking algorithm on graphs with bounded degree, while Grohe and Schweikardt showed that probably no such algorithm exists for trees of bounded depth. We analyze the fragment FO({>0}) of this logic. While we remove for example subtraction and comparison between two nonatomic counting terms, this logic remains quite expressive: We allow nested counting and comparison between counting terms and arbitrarily large numbers. Our main result is an approximation scheme of the model-checking problem for FO({>0}) that runs in linear fpt time on structures with bounded expansion. This scheme either gives the correct answer or says “I do not know. ” The latter answer may only be given if small perturbations in the number-symbols of the formula could make it both satisfied and unsatisfied. This is complemented by showing that exactly solving the model-checking problem for FO({>0}) is already hard on trees of bounded depth and just slightly increasing the expressiveness of FO({>0}) makes even approximation hard on trees.

Details