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

"Model Checking Existential Logic on Partially Ordered Sets";

Talk: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vienna; 2014-07-14 - 2014-07-18; in: "CSL-LICS 2014", ACM New York, NY, USA, (2014), ISBN: 978-1-4503-2886-9.

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 fixedparameter

tractability results for model checking on digraphs of

bounded degree and bounded clique-width.

Project Head Stefan Szeider:

Exploiting New Types of Structure for Fixed Parameter Tractability

Project Head Stefan Szeider:

Parameterized Compilation

Project Head Stefan Szeider:

The Parameterized Complexity of Reasoning Problems

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