Nikolas Mählmann — Page 2

arXiv2022

Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

We present a fixed-parameter tractable algorithm for first-order model checking on interpretations of graph classes with bounded local cliquewidth. Notably, this includes interpretations of planar graphs, and more generally, of classes of bounded genus. To obtain this result we develop a new tool which works in a very general setting of dependent classes and which we believe can be an important ingredient in achieving similar results in the future.

cs.DS↗

arXiv2021

Recursive Backdoors for SAT

A strong backdoor in a formula $ϕ$ of propositional logic to a tractable class $\mathcal{C}$ of formulas is a set $B$ of variables of $ϕ$ such that every assignment of the variables in $B$ results in a formula from $\mathcal{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.

cs.DS↗