Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers

Ian Pratt-Hartmann

TL;DR

This work proves that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers $\mathcal{GC}^2$ lies in $\text{EXPTIME}$, and provides a streamlined method that also yields Kazakov's EXPTIME result for plain satisfiability. The core technique is a translation of $\mathcal{GC}^2$ formulas into an exponential-sized system of integer constraints $\mathcal{E}$, built from 1-types, 2-types, and guarded counts, whose solvability in $\mathbb{N}$ corresponds exactly to finite satisfiability of the formula. The authors then reduce the constraint system to an integer programming problem (and further to linear programming) in exponential time, establishing the upper bound, and they extend the approach to show satisfiability (not just finite satisfiability) is also in $\text{EXPTIME}$ via a $\mathbb{N}^*$-based analysis that ultimately yields a two-valued Boolean Horn abstraction. The results imply tightness with known EXPTIME-hardness for related description-logics and offer a direct, self-contained proof strategy for the EXPTIME membership in both finite satisfiability and satisfiability for $\mathcal{GC}^2$.

Abstract

We show that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. The method employed also yields a simple proof of a result recently obtained by Y. Kazakov, that the satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME.

Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers

TL;DR

This work proves that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers lies in , and provides a streamlined method that also yields Kazakov's EXPTIME result for plain satisfiability. The core technique is a translation of formulas into an exponential-sized system of integer constraints , built from 1-types, 2-types, and guarded counts, whose solvability in corresponds exactly to finite satisfiability of the formula. The authors then reduce the constraint system to an integer programming problem (and further to linear programming) in exponential time, establishing the upper bound, and they extend the approach to show satisfiability (not just finite satisfiability) is also in via a -based analysis that ultimately yields a two-valued Boolean Horn abstraction. The results imply tightness with known EXPTIME-hardness for related description-logics and offer a direct, self-contained proof strategy for the EXPTIME membership in both finite satisfiability and satisfiability for .

Abstract

We show that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. The method employed also yields a simple proof of a result recently obtained by Y. Kazakov, that the satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME.

Paper Structure

This paper contains 5 sections, 12 theorems, 50 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Transformation into an integer constraint problem
  4. Main result
  5. The Satisfiability Problem

Key Result

Lemma 1

Let $\phi$ be a formula of $\mathcal{GC}^2$ and $\mathfrak{A}$ a structure over the signature of $\phi$. For $N \geq 1$, let $N \cdot \mathfrak{A}$ denote the union of $N$ disjoint copies of $\mathfrak{A}$. If $\phi$ is satisfied in $\mathfrak{A}$, then it is satisfied in $N \cdot \mathfrak{A}$.

Figures (3)

  • Figure 1: The decompositions of $A_\pi$ for the strings $s$ and $s'$.
  • Figure 2: The messages sent by $a \in A_\pi$. For each $j$ ($0 \leq j < P$), $a$ may or may not send a message labelled $\lambda_{a,j}$ (hence the dotted lines); if it does, then $\lambda_{a,j} \in \Lambda_{\pi,j}$. For each $k$ ($0 \leq k < R$), $a$ sends $n_{a,k}$ messages labelled $\mu_{\pi,k}$; but the numbers $n_{a,k}$ can be zero.
  • Figure 3: Fixing the non-invertible message-types.

Theorems & Definitions (28)

  • Definition 1
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Remark 1
  • Definition 2
  • Remark 2
  • Definition 3
  • Lemma 3
  • ...and 18 more