Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Complexity of the Two-Variable Fragment with (Binary-Coded) Counting Quantifiers

Ian Pratt-Hartmann

TL;DR

This work establishes that both satisfiability and finite satisfiability for the two-variable first-order fragment with counting quantifiers, $ abla$C$^2$, lie in $NEXPTIME$ even when counting subscripts are binary-coded. The authors develop a robust framework built around a normal-form $ abla$C$^2$^*$ formula, 1-types and 2-types, counting signatures, and a rich set of approximation techniques (notably $(\Pi,B)$-approximations, patches, and the notion of frames) to reduce model existence to a finite combinatorial search. A key contribution is the introduction of $Z$-solutions for frames, enabling a bounded search space and yielding a small-model property: finite satisfiability implies a frame with dimension at most $X$ and a $Z$-solution exists; extended $Z$-solutions extend the result to general satisfiability over $\mathbb{N}^*$. Together, these results generalize prior unary-coding bounds to binary coding and provide a tractable complexity characterization for both finite and infinite models of $ abla$C$^2$ formulas.

Abstract

We show that the satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NEXPTIME, even when counting quantifiers are coded succinctly.

Complexity of the Two-Variable Fragment with (Binary-Coded) Counting Quantifiers

TL;DR

This work establishes that both satisfiability and finite satisfiability for the two-variable first-order fragment with counting quantifiers, C, lie in even when counting subscripts are binary-coded. The authors develop a robust framework built around a normal-form C^*(\Pi,B)ZXZZ\mathbb{N}^* abla^2$ formulas.

Abstract

We show that the satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NEXPTIME, even when counting quantifiers are coded succinctly.

Paper Structure

This paper contains 5 sections, 22 theorems, 19 equations, 2 figures.

Table of Contents

  1. Background
  2. Preliminaries
  3. Profiles and approximations
  4. Deciding finite satisfiability
  5. Deciding satisfiability

Key Result

Lemma 1

Let $\phi$ be a sentence in $\mathcal{C}^2$. We can construct, in time bounded by a polynomial function of $\lVert \phi \rVert$, a formula satisfying the following conditions: $(i)$$\alpha$ is a quantifier-free, equality-free formula with $x$ as its only variable, $(ii)$$\beta$ is a quantifier-free, equality-free formula with $x$ and $y$ as its only variables, $(iii)$ the $f_h$$(1 \leq h \leq m)$

Figures (2)

  • Figure 1: Arrangement of $\Pi'$-profiles and $\Pi"$-profiles in $B$.
  • Figure 2: Dealing with non-invertible messages.

Theorems & Definitions (66)

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