Abstract
We consider the computational complexity of the problem of counting the number of answers 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. This new trichotomy theorem generalizes and unifies a number of existing classification results in the literature, including classifications on model checking primitive positive formulas, model checking existential positive formulas, and counting homomorphisms. 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. To justify our width minimization algorithm, we prove a dual to a classical theorem of Lovasz on counting homomorphisms between structures. This is joint work with Stefan Mengel (CNRS). The first part of the talk is based on a PODS '16 article.