S. Bova, R. Ganian, S. Szeider:

"Model Checking Existential Logic on Partially Ordered Sets";

ACM Transactions on Computational Logic,17(2015), 2; 1 - 35.

We study the problem of checking whether an existential sentence (i.e., a first-order sentence in prefix

form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered

set (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, in which we prove that the isomorphism problem is polynomialtime

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.

http://dx.doi.org/10.1145/2814937

http://publik.tuwien.ac.at/files/PubDat_247976.pdf

Created from the Publication Database of the Vienna University of Technology.