Model Checking Existential Logic on Partially Ordered Sets

TL;DR

This paper investigates the complexity of model checking existential logic on finite posets, showing fixed-parameter tractability for posets of bounded width and solving an open problem in order theory.

Contribution

It establishes fixed-parameter tractability of existential model checking on bounded-width posets and proves polynomial-time tractability of the isomorphism problem in this class.

Findings

Model checking existential logic is fixed-parameter tractable on bounded-width posets.

The isomorphism problem is polynomial-time solvable on bounded-width posets.

Complexity results are tight and relate to other classes like bounded degree and clique-width digraphs.

Abstract

We study the problem of checking whether an existential sentence (that is, a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (in short, a poset). A poset is a reflexive, antisymmetric, and transitive digraph. The problem encompasses the fundamental embedding problem of finding an isomorphic copy of a poset as an induced substructure of another poset. Model checking existential logic is already NP-hard on a fixed poset; thus we investigate structural properties of posets yielding conditions for fixed-parameter tractability when the problem is parameterized by the sentence. We identify width as a central structural property (the width of a poset is the maximum size of a subset of pairwise incomparable elements); our main algorithmic result is that model checking existential logic on classes of finite posets of bounded width is fixed-parameter tractable. We observe a similar phenomenon in classical complexity, where we prove that the isomorphism problem is polynomial-time tractable on classes of posets of bounded width; this settles an open problem in order theory. We surround our main algorithmic result with complexity results on less restricted, natural neighboring classes of finite posets, establishing its tightness in this sense. We also relate our work with (and demonstrate its independence of) fundamental fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.