Enumerating Teams in First-Order Team Logics

TL;DR

This paper investigates the enumeration complexity of satisfiability problems in first-order team logics, revealing complexity classifications and extending understanding of these problems beyond traditional polynomial time bounds.

Contribution

It introduces a framework for hard enumeration in first-order team logics and classifies the complexity of enumerating satisfying teams for various logic formulas.

Findings

Enumeration of teams in dependence and independence logic is DelNP-complete.

Enumeration for inclusion logic formulas is in DelP.

Minimal solutions in inclusion logic are DelNP-complete.

Abstract

We start the study of the enumeration complexity of different satisfiability problems in first-order team logics. Since many of our problems go beyond DelP, we use a framework for hard enumeration analogous to the polynomial hierarchy, which was recently introduced by Creignou et al. (Discret. Appl. Math. 2019). We show that the problem to enumerate all satisfying teams of a fixed formula in a given first-order structure is DelNP-complete for certain formulas of dependence logic and independence logic. For inclusion logic formulas, this problem is even in DelP. Furthermore, we study the variants of this problems where only maximal, minimal, maximum and minimum solutions, respectively, are considered. For the most part these share the same complexity as the original problem. An exception is the minimum-variant for inclusion logic, which is DelNP-complete.