Now showing 1 - 5 of 5
  • Some of the metrics are blocked by your 
    Item type:Publication,
    Combinatorial and Algorithmic Aspects of Monadic Stability
    (Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022) ; ; ; ;
    Nowhere dense classes of graphs are classes of sparse graphs with rich structural and algorithmic properties, however, they fail to capture even simple classes of dense graphs. Monadically stable classes, originating from model theory, generalize nowhere dense classes and close them under transductions, i.e. transformations defined by colorings and simple first-order interpretations. In this work we aim to extend some combinatorial and algorithmic properties of nowhere dense classes to monadically stable classes of finite graphs. We prove the following results. - For every monadically stable class C and fixed integer s ≥ 3, the Ramsey numbers R_C(s,t) are bounded from above by 𝒪(t^{s-1-δ}) for some δ > 0, improving the bound R(s,t) ∈ 𝒪(t^{s-1}/(log t)^{s-1}) known for the class of all graphs and the bounds known for k-stable graphs when s ≤ k. - For every monadically stable class C and every integer r, there exists δ > 0 such that every graph G ∈ C that contains an r-subdivision of the biclique K_{t,t} as a subgraph also contains K_{t^δ,t^δ} as a subgraph. This generalizes earlier results for nowhere dense graph classes. - We obtain a stronger regularity lemma for monadically stable classes of graphs. - Finally, we show that we can compute polynomial kernels for the independent set and dominating set problems in powers of nowhere dense classes. Formerly, only fixed-parameter tractable algorithms were known for these problems on powers of nowhere dense classes.
    conference paper
      20  39
  • Some of the metrics are blocked by your 
    Item type:Publication,
    Recursive Backdoors for SAT
    (Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021) ; ;
    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.
    conference paper
      19  26
  • Some of the metrics are blocked by your 
    Item type:Publication,
    Advances in Algorithmic Meta Theorems
    (Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024) ;
    Tractability results for the model checking problem of logics yield powerful algorithmic meta theorems of the form: Every computational problem expressible in a logic ℒ can be solved efficiently on every class C of structures satisfying certain conditions. The most prominent logics studied in the field are (counting) monadic second-order logic (C)MSO and first-order logic FO and its extensions. The complexity of CMSO model checking in general and of FO model checking on monotone graph classes is very well understood. In recent years there has been a rapid and exciting development of new algorithmic meta theorems. On the one hand there has been major progress for FO model checking on hereditary graph classes. This progress was driven by the development of a combinatorial structure theory for the logically defined monadically stable and monadically dependent graph classes, as well as by the advent of the new width measure twinwidth. On the other hand new algorithmic meta theorems for new logics with expressive power between FO and CMSO offer a new unifying view on methods like the irrelevant vertex technique and recursive understanding. In this paper we overview the recent advances in algorithmic meta theorems and provide rough sketches for the methods to prove them.
    conference paper
      7  22
  • Some of the metrics are blocked by your 
    Item type:Publication,
    First-Order Logic with Connectivity Operators
    (Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022) ; ;
    First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates conn_k(x,y,z_1,…,z_k) that hold true in a graph if there exists a path between (the valuations of) x and y after (the valuations of) z_1,…,z_k have been deleted, we obtain separator logic FO+conn. We show that separator logic can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes. Denote by FO+conn_k the fragment of separator logic that is restricted to connectivity predicates with at most k+2 variables (that is, at most k deletions). We show that FO+conn_{k+1} is strictly more expressive than FO+conn_k for all k ≥ 0. We then study the limitations of separator logic and prove that it cannot express planarity, and, in particular, not the disjoint paths problem. We obtain the stronger disjoint-paths logic FO+DP by adding the atomic predicates disjoint-paths_k[(x_1,y_1),…,(x_k,y_k)] that evaluate to true if there are internally vertex-disjoint paths between (the valuations of) x_i and y_i for all 1 ≤ i ≤ k. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Again we show that the fragments FO+DP_k that use predicates for at most k disjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitive-closure logics and monadic second-order logic.
    conference paper
      15  19
  • Some of the metrics are blocked by your 
    Item type:Publication,
    Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures
    (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022)
    Pilipczuk, Michał
    ;
    ; ; ;
    We introduce a new data structure for answering connectivity queries in undirected graphs subject to batched vertex failures. Precisely, given any graph G and integer parameter k, we can in fixed-parameter time construct a data structure that can later be used to answer queries of the form: "are vertices s and t connected via a path that avoids vertices u₁,…, u_k?" in time 2^𝒪(k). In the terminology of the literature on data structures, this gives the first deterministic data structure for connectivity under vertex failures where for every fixed number of failures, all operations can be performed in constant time. With the aim to understand the power and the limitations of our new techniques, we prove an algorithmic meta theorem for the recently introduced separator logic, which extends first-order logic with atoms for connectivity under vertex failures. We prove that the model-checking problem for separator logic is fixed-parameter tractable on every class of graphs that exclude a fixed topological minor. We also show a weak converse. This implies that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor. The backbone of our proof relies on a decomposition theorem of Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [SICOMP '19], which provides a tree decomposition of a given graph into bags that are unbreakable. Crucially, unbreakability allows to reduce separator logic to plain first-order logic within each bag individually. Guided by this observation, we design our model-checking algorithm using dynamic programming over the tree decomposition, where the transition at each bag amounts to running a suitable model-checking subprocedure for plain first-order logic. This approach is robust enough to provide also an extension to efficient enumeration of answers to a query expressed in separator logic.
    conference paper
      14  35