Abstracts of Stefan Mengel

On Compiling CNFs into Structured Deterministic DNNFs

Simone Bova, Florent Capelli, Stefan Mengel and Friedrich Slivovsky

We show that the traces of recently introduced dynamic programming algorithms for #SAT can be used to construct structured deterministic DNNF (decomposable negation normal form) representations of propositional formulas in CNF (conjunctive normal form). This allows us prove new upper bounds on the complexity of compiling CNF formulas into structured deterministic DNNFs in terms of parameters such as the treewidth and the clique-width of the incidence graph. Back

The Logic of Counting Query Answers: A Study via Existential Positive Queries

Hubie Chen and Stefan Mengel

We consider the computational complexity of counting the number of answers to a logical formula on a finite structure. In the setting of parameterized complexity, we present a trichotomy theorem on classes of existential positive queries. We then proceed to study an extension of first-order logic in which algorithms for the counting problem at hand can be naturally and conveniently expressed. Back

A Strongly Exponential Separation of DNNFs from CNFs

Simone Bova, Florent Capelli, Stefan Mengel and Friedrich Slivovsky

Decomposable Negation Normal Forms (DNNFs) are boolean circuits in negation normal form where the subcircuits leading into each AND gate are defined on disjoint sets of variables. We prove a strongly exponential lower bound on the size of DNNFs for a class of CNFs built from expander graphs. As a corollary, we obtain a strongly exponential separation between DNNFs and CNFs in prime implicates form. This settles an open problem in the area of knowledge compilation (Darwiche and Marquis, 2002). Back

A Trichotomy in the Complexity of Counting Answers to Conjunctive Queries

Hubie Chen and Stefan Mengel

Conjunctive queries are basic and heavily studied database queries; in relational algebra, they are the select-project-join queries. In this article, we study the fundamental problem of counting, given a conjunctive query and a relational database, the number of answers to the query on the database. In particular, we study the complexity of this problem relative to sets of conjunctive queries. We present a trichotomy theorem, which shows essentially that this problem on a set of conjunctive queries is either tractable, equivalent to the parameterized CLIQUE problem, or as hard as the parameterized counting CLIQUE problem; the criteria describing which of these situations occurs is simply stated, in terms of graph-theoretic conditions. Back

Understanding model counting for β-acyclic CNF-formulas

Johann Brault-Baron, Florent Capelli and Stefan Mengel

We extend the knowledge about so-called structural restrictions of #SAT by giving a polynomial time algorithm for β-acyclic #SAT. In contrast to previous algorithms in the area, our algorithm does not proceed by dynamic programming but works along an elimination order, solving a weighted version of constraint satisfaction. Moreover, we give evidence that this deviation from more standard algorithm is not a coincidence, but that there is likely no dynamic programming algorithm of theusual style for β-acyclic #SAT. Back

Hypergraph Acyclicity and Propositional Model Counting

Florent Capelli, Arnaud Durand and Stefan Mengel

We show that the propositional model counting problem #SAT for CNF- formulas with hypergraphs that allow a disjoint branches decomposition can be solved in polynomial time. We show that this class of hypergraphs is incomparable to hypergraphs of bounded incidence cliquewidth which were the biggest class of hypergraphs for which #SAT was known to be solvable in polynomial time so far. Furthermore, we present a polynomial time algorithm that computes a disjoint branches decomposition of a given hypergraph if it exists and rejects otherwise. Finally, we show that some slight extensions of the class of hypergraphs with disjoint branches decompositions lead to intractable #SAT, leaving open how to generalize the counting result of this paper. Back

Arithmetic Branching Programs with Memory

Stefan Mengel

We extend the well known characterization of VP_ws as the class of polynomials computed by polynomial size arithmetic branching programs to other complexity classes. In order to do so we add additional memory to the computation of branching programs to make them more expressive. We show that allowing different types of memory in branching programs increases the computational power even for constant width programs. In particular, this leads to very natural and robust characterizations of VP and VNP by branching programs with memory. Back

The arithmetic complexity of tensor contractions

Florent Capelli, Arnaud Durand and Stefan Mengel

We investigate the algebraic complexity of tensor calulus. We consider a generalization of iterated matrix product to tensors and show that the resulting formulas exactly capture VP, the class of polynomial families efficiently computable by arithmetic circuits. This gives a natural and robust characterization of this complexity class that despite its naturalness is not very well understood so far. Back

Structural Tractability of Counting of Solutions to Conjunctive Queries

Arnaud Durand and Stefan Mengel

In this paper we explore the problem of counting solutions to conjunctive queries. We consider a parameter called the quantified star size of a formula φ which measures how the free variables are spread in φ. We show that for conjunctive queries that admit nice decomposition properties (such as being of bounded treewidth or generalized hypertree width) bounded quantified star size exactly characterizes the classes of queries for which counting the number of solutions is tractable. This also allows us to fully characterize the conjunctive queries for which counting the solutions is tractable in the case of bounded arity.
To illustrate the applicability of our results, we also show that computing the quantified star size of a formula is possible in time nO(k) for queries of generalized hypertree width k. Furthermore, quantified star size is even fixed parameter tractable parameterized by some other width measures, while it is W[1]-hard for generalized hypertree width and thus unlikely to be fixed parameter tractable. We finally show how to compute an approximation of quantified star size in polynomial time where the approximation ratio depends on the width of the input. Back

The Complexity of Weighted Counting for Acyclic Conjunctive Queries

Arnaud Durand and Stefan Mengel

This paper is a study of weighted counting of the solutions of acyclic conjunctive queries (ACQ). The unweighted quantifier free version of this problem is known to be tractable (for combined complexity), but it is also known that introducing even a single quantified variable makes it #P-hard. We first show that weighted counting for quantifier-free ACQ is still tractable and that even minimalistic extensions of the problem lead to hard cases. We then introduce a new parameter for quantified queries that permits to isolate large island of tractability. We show that, up to a standard assumption from parameterized complexity, this parameter fully characterizes tractable subclasses for counting weighted solutions of ACQ queries. Thus we completely determine the tractability frontier for weighted counting for ACQ. Back

Monomials in arithmetic circuits: Complete problems in the counting hierarchy

Hervé Fournier, Guillaume Malod and Stefan Mengel

We consider the complexity of two questions on polynomials given by arithmetic circuits: testing whether a monomial is present and counting the number of monomials. We show that these problems are complete for subclasses of the counting hierarchy which had few or no known natural complete problems before. We also study these questions for circuits computing multilinear polynomials. Back

Characterizing Arithmetic Circuit Classes by Constraint Satisfaction Problems

Stefan Mengel

We explore the expressivity of constraint satisfaction problems (CSPs) in the arithmetic circuit model. While CSPs are known to yield VNP-complete polynomials in the general case, we show that for different restrictions of the structure of the CSPs we get characterizations of different arithmetic circuit classes. In particular we give the first natural non-circuit characterization of VP, the class of polynomial families efficiently computable by arithmetic circuits. Back

A generalization of Tutte's theorem on Hamiltonian cycles in planar graphs

Jochen Harant and Stefan Senitsch

In 1956, W.T. Tutte proved that a 4-connected planar graph is hamiltonian. Moreover, in 1997, D.P. Sanders extended this to the result that a 4-connected planar graph contains a hamiltonian cycle through any two of its edges. We prove that a planar graph G has a cycle containing a given subset X of its vertex set and any two prescribed edges of the subgraph of G induced by X if |X|≥3 and if X is 4-connected in G. If X=V(G) then Sanders’ result follows. Back