Kurt Gödel Research Center

2015 seminar talk: The Parameterized Complexity Classification of – and the Logic of – Counting Answers to Existential Positive Queries

Talk held by Hubie Chen (University of the Basque Country, Spain) at the KGRC seminar on 2015-10-22.

Abstract

We consider the computational complexity of the problem of counting the number of answers (satisfying assignments) to a logical formula on a finite structure.

We present two contributions.

First, in the setting of parameterized complexity, we present a classification theorem on classes of existential positive queries. In particular, we prove that (relative to the problem at hand) any class of existential positive formulas is interreducible with a class of primitive positive formulas. In the setting of bounded arity, this allows us to derive a trichotomy theorem indicating the complexity of any class of existential positive formulas, as we previously proved a trichotomy theorem on classes of primitive positive formulas (Chen and Mengel '15). This new trichotomy theorem generalizes and unifies a number of existing classification results in the literature, including the classifications on model checking primitive positive formulas (Grohe '07), model checking existential positive formulas (Chen '14), and counting homomorphisms (Dalmau and Jonsson '04).

Our second contribution is to introduce and study an extension of first-order logic in which algorithms for the counting problem at hand can be naturally and conveniently expressed. In particular, we introduce a logic which we call #-logic where the evaluation of a so-called #-sentence on a structure yields an integer, as opposed to just a propositional value (true or false) as in usual first-order logic. We discuss the width of a formula as a natural complexity measure and show that this measure is meaningful in #-logic and that there is an algorithm that minimizes width in the "existential positive fragment" of #-logic.

This is joint work with Stefan Mengel.