Problems parameterized by treewidth tractable in single exponential time: a logical approach

TL;DR

This paper introduces a logical framework, ECML, that captures many problems solvable in single exponential time parameterized by treewidth, and extends it to include connectivity with randomized algorithms, highlighting limitations for certain non-acyclic problems.

Contribution

The paper presents ECML, a new modal logic capturing many tractable problems, and extends it with connectivity features using the Cut&Count technique, demonstrating single exponential algorithms under treewidth parameterization.

Findings

Model checking ECML is solvable in single exponential time.

Extended ECML with connectivity is also tractable with randomized algorithms.

Certain non-acyclic problems do not admit such algorithms unless ETH fails.

Abstract

We introduce a variant of modal logic, dubbed EXISTENTIAL COUNTING MODAL LOGIC (ECML), which captures a vast majority of problems known to be tractable in single exponential time when parameterized by treewidth. It appears that all these results can be subsumed by the theorem that model checking of ECML admits an algorithm with such complexity. We extend ECML by adding connectivity requirements and, using the Cut&Count technique introduced by Cygan et al. [4], prove that problems expressible in the extension are also tractable in single exponential time when parameterized by treewidth; however, using randomization. The need for navigationality of the introduced logic is justified by a negative result that two expository problems involving non-acyclic conditions, C_l VERTEX DELETION and GIRTH>l VERTEX DELETION for l>=5, do not admit such a robust algorithm unless Exponential Time Hypothesis fails.