TY - GEN

T1 - Parameterized Complexity of Elimination Distance to First-Order Logic Properties

AU - Fomin, Fedor V.

AU - Golovach, Petr A.

AU - Thilikos, Dimitrios M.

N1 - Publisher Copyright:
© 2021 IEEE.

PY - 2021/6/29

Y1 - 2021/6/29

N2 - The elimination distance to some target graph property \mathcal P is a general graph modification parameter introduced by Bulian and Dawar. We initiate the study of elimination distances to graph properties expressible in first-order logic. We delimit the problem's fixed-parameter tractability by identifying sufficient and necessary conditions on the structure of prefixes of first-order logic formulas. Our main result is the following meta-theorem: For every graph property \mathcal P expressible by a first order-logic formula Σ3, that is, of the form\begin equation*\varphi = \exists x_1\exists x_2 \cdots \exists x_r\forall y_1\forall y_2 \cdots \forall y_s\quad \exists z_1\exists z_2 \cdots \exists z_t\,\psi ,\end equation*where ψ is a quantifier-free first-order formula, checking whether the elimination distance of a graph to \mathcal P does not exceed k, is fixed-parameter tractable parameterized by k. Properties of graphs expressible by formulas from Σ3 include being of bounded degree, excluding a forbidden subgraph, or containing a bounded dominating set. We complement this theorem by showing that such a general statement does not hold for formulas with even slightly more expressive prefix structure: There are formulas Π3, for which computing elimination distance is W[2]-hard.

AB - The elimination distance to some target graph property \mathcal P is a general graph modification parameter introduced by Bulian and Dawar. We initiate the study of elimination distances to graph properties expressible in first-order logic. We delimit the problem's fixed-parameter tractability by identifying sufficient and necessary conditions on the structure of prefixes of first-order logic formulas. Our main result is the following meta-theorem: For every graph property \mathcal P expressible by a first order-logic formula Σ3, that is, of the form\begin equation*\varphi = \exists x_1\exists x_2 \cdots \exists x_r\forall y_1\forall y_2 \cdots \forall y_s\quad \exists z_1\exists z_2 \cdots \exists z_t\,\psi ,\end equation*where ψ is a quantifier-free first-order formula, checking whether the elimination distance of a graph to \mathcal P does not exceed k, is fixed-parameter tractable parameterized by k. Properties of graphs expressible by formulas from Σ3 include being of bounded degree, excluding a forbidden subgraph, or containing a bounded dominating set. We complement this theorem by showing that such a general statement does not hold for formulas with even slightly more expressive prefix structure: There are formulas Π3, for which computing elimination distance is W[2]-hard.

KW - descriptive complexity

KW - elimination distance

KW - first-order logic

KW - parameterized complexity

UR - http://www.scopus.com/inward/record.url?scp=85111188153&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85111188153&partnerID=8YFLogxK

U2 - 10.1109/LICS52264.2021.9470540

DO - 10.1109/LICS52264.2021.9470540

M3 - Conference contribution

AN - SCOPUS:85111188153

T3 - Proceedings - Symposium on Logic in Computer Science

BT - 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021

Y2 - 29 June 2021 through 2 July 2021

ER -