Author name cluster

Nikolas Mählmann

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.

5 papers

2 author rows

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

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

MFCS Conference 2021 Conference Paper

Recursive Backdoors for SAT

Nikolas Mählmann
Sebastian Siebertz
Alexandre Vigny

A strong backdoor in a formula φ of propositional logic to a tractable class C of formulas is a set B of variables of φ such that every assignment of the variables in B results in a formula from C. Strong backdoors of small size or with a good structure, e. g. with small backdoor treewidth, lead to efficient solutions for the propositional satisfiability problem SAT. In this paper we propose the new notion of recursive backdoors, which is inspired by the observation that in order to solve SAT we can independently recurse into the components that are created by partial assignments of variables. The quality of a recursive backdoor is measured by its recursive backdoor depth. Similar to the concept of backdoor treewidth, recursive backdoors of bounded depth include backdoors of unbounded size that have a certain treelike structure. However, the two concepts are incomparable and our results yield new tractability results for SAT.

Details

Highlights Conference 2021 Conference Abstract

SAT via Recursive Backdoors

Nikolas Mählmann

Due to its expressiveness the SAT problem of checking whether a formula of propositional logic is satisfiable is widely used as a general problem solving framework. While SAT is computationally hard on general formulas, there exist restricted tractable classes of formulas, for which SAT solving is known to be efficient. A backdoor of a CNF formula phi to a tractable class C of formulas is a set B of variables of phi that when assigned reduces phi to a formula from C. Backdoors of small size or with a good structure, lead to efficient solutions for SAT. In our paper we introduce the new notion of recursive backdoors, which generalize backdoors and exploit the structure of formulas that can be recursively split into independent parts by partial assignments. Our generalization is motivated by the observation that independent or loosely connected components are common among real world SAT instances and many industrial solvers use value caching heuristics or component analysis in order to exploit this property. The quality of a recursive backdoor is measured by its recursive backdoor depth. Recursive backdoors of bounded depth can contain an unbounded number of variables and allow for efficient SAT solving if they are given as an input to the solver. The challenge therefore lies in the detection of recursive backdoors. For the base class of empty formulas C0, we show that recursive backdoor detection is fixed-parameter tractable and yields new tractability results for SAT.

Details