Quantified Conjunctive Queries on Partially Ordered Sets

TL;DR

This paper investigates the computational complexity of checking quantified conjunctive queries on finite posets, proving NP-hardness in general but identifying fixed-parameter tractability for posets of bounded width.

Contribution

It introduces an algorithmic approach for model checking on bounded-width posets and establishes complexity bounds, advancing understanding of query evaluation in poset structures.

Findings

NP-hardness of the problem on fixed posets

Fixed-parameter tractability for posets of bounded width

Complexity bounds based on poset invariants

Abstract

We study the computational problem of checking whether a quantified conjunctive query (a first-order sentence built using only conjunction as Boolean connective) is true in a finite poset (a reflexive, antisymmetric, and transitive directed graph). We prove that the problem is already NP-hard on a certain fixed poset, and investigate structural properties of posets yielding fixed-parameter tractability when the problem is parameterized by the query. Our main algorithmic result is that model checking quantified conjunctive queries on posets of bounded width is fixed-parameter tractable (the width of a poset is the maximum size of a subset of pairwise incomparable elements). We complement our algorithmic result by complexity results with respect to classes of finite posets in a hierarchy of natural poset invariants, establishing its tightness in this sense.