Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Data-Complexity of the Two-Variable Fragment with Counting Quantifiers

Ian Pratt-Hartmann

TL;DR

The paper determines data-complexity boundaries for two counting-augmented two-variable logics: $ ext{C}^2$ and $ ext{GC}^2$. It proves that satisfiability and finite satisfiability for $ ext{C}^2$ lie in $NP$, while query-answering and finite query-answering for $ ext{GC}^2$ with positive conjunctive queries lie in $co$-$NP$, with tightness results including undecidability for unrestricted $ ext{C}^2$ query answering. The core method is a novel reduction to Presburger arithmetic via a frame-and-star-type encoding, enabling compact representation of models and polynomial-time data procedures. Together these results place sharp, practical limits on satisfiability and query answering for counting-quantified two-variable fragments, informing both theoretical understanding and database-querying techniques under counting quantifiers.

Abstract

The data-complexity of both satisfiability and finite satisfiability for the two-variable fragment with counting is NP-complete; the data-complexity of both query-answering and finite query-answering for the two-variable guarded fragment with counting is co-NP-complete.

Data-Complexity of the Two-Variable Fragment with Counting Quantifiers

TL;DR

The paper determines data-complexity boundaries for two counting-augmented two-variable logics: and . It proves that satisfiability and finite satisfiability for lie in , while query-answering and finite query-answering for with positive conjunctive queries lie in -, with tightness results including undecidability for unrestricted query answering. The core method is a novel reduction to Presburger arithmetic via a frame-and-star-type encoding, enabling compact representation of models and polynomial-time data procedures. Together these results place sharp, practical limits on satisfiability and query answering for counting-quantified two-variable fragments, informing both theoretical understanding and database-querying techniques under counting quantifiers.

Abstract

The data-complexity of both satisfiability and finite satisfiability for the two-variable fragment with counting is NP-complete; the data-complexity of both query-answering and finite query-answering for the two-variable guarded fragment with counting is co-NP-complete.

Paper Structure

This paper contains 7 sections, 21 theorems, 60 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The fragment $\mathcal{C}^2$
  4. Data-complexity of satisfiability and finite satisfiability for $\mathcal{C}^2$
  5. The fragment $\mathcal{GC}^2$
  6. Data-complexity of query-answering and finite query-answering
  7. Acknowledgments

Key Result

Lemma 1

Let $\varphi$ be a $\mathcal{C}^2$-formula. There exist $($i$)$ a $\mathcal{C}^2$-formula $\alpha$ containing no quantifiers and no occurrences of $\approx$, $($ii$)$ a list of positive integers $C_1, \ldots, C_m$ and $($iii$)$ a list of binary predicates $f_1, \ldots, f_m$, with the following prope and $C = \max_h C_h$, then $($i$)$$\varphi^* \models \varphi$, and $($ii$)$ any model of $\varphi$

Figures (5)

  • Figure 1: The configuration of the claim in the proof of Lemma \ref{['lma:bigStrongLoops']}. An arrow on a line indicates a message-type; absence of an arrow on a line indicates a non-message type; a parenthetical arrow on a line indicates a 2-type which may or may not be a message-type. For definiteness, $e$ and $f$ have been drawn outside the set of elements accessible from $a$ or $b$ in $\Omega-2$ steps; however, this is not required by the claim.
  • Figure 2: Ensuring that ${\rm tp}^{\mathfrak{A}'}[a,d]$ is silent. Types displayed in the drawing of $\mathfrak{A}'$ are to be read left-to-right: thus, ${\rm tp}^{\mathfrak{A}'}[a,d] = {\rm tp}^\mathfrak{A}[e,f]$, ${\rm tp}^{\mathfrak{A}'}[e,d] = {\rm tp}^{\mathfrak{A}}[a,d]$, and ${\rm tp}^{\mathfrak{A}'}[e,f] = {\rm tp}^{\mathfrak{A}}[e,d]$. Lines and arrows are interpreted as in Fig. \ref{['fig:bigConfig']}.
  • Figure 3: Destroying a strong t-cycle: the two-types in $\mathfrak{A}"$ are to be read from left to right; thus, ${\rm tp}^{\mathfrak{A}"}[a,b] = {\rm tp}^{\mathfrak{A}'}[a,d]$, ${\rm tp}^{\mathfrak{A}"}[a,d] = {\rm tp}^{\mathfrak{A}'}[a,b]$, ${\rm tp}^{\mathfrak{A}"}[c,b] = {\rm tp}^{\mathfrak{A}'}[c,d]$ and ${\rm tp}^{\mathfrak{A}"}[c,d] = {\rm tp}^{\mathfrak{A}'}[c,b]$. Lines and arrows are interpreted as in Fig. \ref{['fig:bigConfig']}.
  • Figure 4: Organization of $\mathfrak{A}^*$ as a tree of copies of $\mathfrak{A}_0$, in the case where $Y = |S|$ is finite; for legibility, the elements of $S$ are numbered, arbitrarily, as $s_1, \ldots s_Y$.
  • Figure 5: Re-direction of non-invertible messages in $\mathfrak{A}_\epsilon$ in the proof of Lemma \ref{['lma:bigLoops']}.

Theorems & Definitions (64)

  • Definition 1
  • Definition 2
  • Remark 1
  • Lemma 1
  • proof
  • Definition 3
  • Definition 4
  • Remark 2
  • Definition 5
  • Lemma 2
  • ...and 54 more