An Algorithmic Metatheorem for Directed Treewidth

The notion of directed treewidth was introduced by Johnson, Robertson, Seymour and Thomas [Journal of Combinatorial Theory, Series B, Vol 82, 2001] as a first step towards an algorithmic metatheory for digraphs. They showed that some NP-complete properties such as Hamiltonicity can be decided in polynomial time on digraphs of constant directed treewidth. Nevertheless, despite more than one decade of intensive research, the list of hard combinatorial problems that are known to be solvable in polynomial time when restricted to digraphs of constant directed treewidth has remained scarce. In this work we enrich this list by providing for the first time an algorithmic metatheorem connecting the monadic second order logic of graphs to directed treewidth. We show that most of the known positive algorithmic results for digraphs of constant directed treewidth can be reformulated in terms of our metatheorem. Additionally, we show how to use our metatheorem to provide polynomial time algorithms for two classes of combinatorial problems that have not yet been studied in the context of directed width measures. More precisely, for each fixed $k,w in mathbb{N}$, we show how to count in polynomial time on digraphs of directed treewidth $w$, the number of minimum spanning strong subgraphs that are the union of $k$ directed paths, and the number of maximal subgraphs that are the union of $k$ directed paths and satisfy a given minor closed property. To prove our metatheorem we devise two technical tools which we believe to be of independent interest. First, we introduce the notion of tree-zig-zag number of a digraph, a new directed width measure that is at most a constant times directed treewidth. Second, we introduce the notion of $z$-saturated tree slice language, a new formalism for the specification and manipulation of infinite sets of digraphs.

On the Satisfiability of Quantum Circuits of Small Treewidth

It has been known for almost three decades that many $mathrm{NP}$-hard optimization problems can be solved in polynomial time when restricted to structures of constant treewidth. In this work we provide the first extension of such results to the quantum setting. We show that given a quantum circuit $C$ with $n$ uninitialized inputs, $mathit{poly}(n)$ gates, and treewidth $t$, one can compute in time $(frac{n}{delta})^{exp(O(t))}$ a classical assignment $yin {0,1}^n$ that maximizes the acceptance probability of $C$ up to a $delta$ additive factor. In particular, our algorithm runs in polynomial time if $t$ is constant and $1/poly(n) < delta < 1$. For unrestricted values of $t$, this problem is known to be complete for the complexity class $mathrm{QCMA}$, a quantum generalization of MA. In contrast, we show that the same problem is $mathrm{NP}$-complete if $t=O(log n)$ even when $delta$ is constant. On the other hand, we show that given a $n$-input quantum circuit $C$ of treewidth $t=O(log n)$, and a constant $delta<1/2$, it is $mathrm{QMA}$-complete to determine whether there exists a quantum state $mid!varphirangle in (mathbb{C}^d)^{otimes n}$ such that the acceptance probability of $Cmid!varphirangle$ is greater than $1-delta$, or whether for every such state $mid!varphirangle$, the acceptance probability of $Cmid!varphirangle$ is less than $delta$. As a consequence, under the widely believed assumption that $mathrm{QMA} eq mathrm{NP}$, we have that quantum witnesses are strictly more powerful than classical witnesses with respect to Merlin-Arthur protocols in which the verifier is a quantum circuit of logarithmic treewidth.

Automated Verification, Synthesis and Correction of Concurrent Systems via MSO Logic

In this work we provide algorithmic solutions to five fundamental problems concerning the verification, synthesis and correction of concurrent systems that can be modeled by bounded p/t-nets. We express concurrency via partial orders and assume that behavioral specifications are given via monadic second order logic. A c-partial-order is a partial order whose Hasse diagram can be covered by c paths. For a finite set T of transitions, we let P(c,T,phi) denote the set of all T-labelled c-partial-orders satisfying phi. If N=(P,T) is a p/t-net we let P(N,c) denote the set of all c-partially-ordered runs of N. A (b, r)-bounded p/t-net is a b-bounded p/t-net in which each place appears repeated at most r times. We solve the following problems: 1. Verification: given an MSO formula phi and a bounded p/t-net N determine whether P(N,c)subseteq P(c,T,phi), whether P(c,T,phi)subseteq P(N,c), or whether P(N,c)cap P(c,T,phi)=emptyset. 2. Synthesis from MSO Specifications: given an MSO formula phi, synthesize a semantically minimal (b,r)-bounded p/t-net N satisfying P(c,T,phi)subseteq P(N, c). 3. Semantically Safest Subsystem: given an MSO formula phi defining a set of safe partial orders, and a b-bounded p/t-net N, possibly containing unsafe behaviors, synthesize the safest (b,r)-bounded p/t-net N whose behavior lies in between P(N,c)cap P(c,T,phi) and P(N,c). 4. Behavioral Repair: given two MSO formulas phi and psi, and a b-bounded p/t-net N, synthesize a semantically minimal (b,r)-bounded p/t net N whose behavior lies in between P(N,c) cap P(c,T,phi) and P(c,T,psi). 5. Synthesis from Contracts: given an MSO formula phi^yes specifying a set of good behaviors and an MSO formula phi^no specifying a set of bad behaviors, synthesize a semantically minimal (b,r)-bounded p/t-net N such that P(c,T,phi^yes) subseteq P(N,c) but P(c,T,phi^no ) cap P(N,c)=emptyset.

Subgraphs Satisfying MSO Properties on z-Topologically Orderable Digraphs

We introduce the notion of z-topological orderings for digraphs. We prove that given a digraph G on n vertices admitting a z-topological order- ing, together with such an ordering, one may count the number of subgraphs of G that at the same time satisfy a monadic second order formula {phi} and are the union of k directed paths, in time f ({phi}, k, z) * n^O(k*z) . Our result implies the polynomial time solvability of many natural counting problems on digraphs admitting z-topological orderings for constant values of z and k. Concerning the relationship between z-topological orderability and other digraph width measures, we observe that any digraph of directed path-width d has a z- topological ordering for z <= 2d + 1. On the other hand, there are digraphs on n vertices admitting a z-topological order for z = 2, but whose directed path-width is {Theta}(log n). Since graphs of bounded directed path-width can have both arbitrarily large undirected tree-width and arbitrarily large clique width, our result provides for the first time a suitable way of partially trans- posing metatheorems developed in the context of the monadic second order logic of graphs of constant undirected tree-width and constant clique width to the realm of digraph width measures that are closed under taking subgraphs and whose constant levels incorporate families of graphs of arbitrarily large undirected tree-width and arbitrarily large clique width.

Canonizable Partial Order Generators and Regular Slice Languages

In a previous work we introduced slice graphs as a way to specify both infinite languages of directed acyclic graphs (DAGs) and infinite languages of partial orders. Therein we focused on the study of Hasse diagram generators, i.e., slice graphs that generate only transitive reduced DAGs, and showed that they could be used to solve several problems related to the partial order behavior of p/t-nets. In the present work we show that both slice graphs and Hasse diagram generators are worth studying on their own. First, we prove that any slice graph SG can be effectively transformed into a Hasse diagram generator HG representing the same set of partial orders. Thus from an algorithmic standpoint we introduce a method of transitive reducing infinite families of DAGs specified by slice graphs. Second, we identify the class of saturated slice graphs. By using our transitive reduction algorithm, we prove that the class of partial order languages representable by saturated slice graphs is closed under union, intersection and even under a suitable notion of complementation (cut-width complementation). Furthermore partial order languages belonging to this class can be tested for inclusion and admit canonical representatives in terms of Hasse diagram generators. As an application of our results, we give stronger forms of some results in our previous work, and establish some unknown connections between the partial order behavior of $p/t$-nets and other well known formalisms for the specification of infinite families of partial orders, such as Mazurkiewicz trace languages and message sequence chart (MSC) languages.