Structure-Guided Automated Reasoning

The concept of treewidth was discovered multiple times. The name was coined in the work by Robertson and Seymour [28], while the concept was studied by Arnborg and Proskurowski [2] under the name partial $k$-trees simultaneously. However, treewidth was discovered even earlier by Bertelè and Brioschi [6], and independently by Halin [19]. Courcelle’s Theorem was proven in a series of articles by Bruno Courcelle [12], see also the textbook by Courcelle and Engelfriet for a detailed introduction [13]. The expressive power of monadic second-order logic was studied before, prominently by Büchi who showed that mso over strings characterizes the regular languages [9]. Related to our treewidth-aware reduction from mc(mso) to sat is the work by Gottlob, Pichler, and Wei, who solve mc(mso) using monadic Datalog [18]; and the work of Bliem, Pichler, and Woltran, who solve it using asp [8].

We provide preliminaries in the next section, prove Theorem 1 and 2 in Section 3, and establish a sat version of Courcelle’s Theorem in Section 4. The technical details of the latter can be found in the technical report version of this article. We extend the result to Fagin-definable properties in Section 5 and provide corresponding $\mathrm{ETH}$ lower bounds in Section 6. We conclude and provide pointers for further research in the last section, which also contains an overview table of this article’s results. Due to lack of space, most proofs are only avilable in the technical report and are replaced by a proof sketch within the main text. The corresponding positions are clearly marked with a “$\mathrm{▼}$”.

A vocabulary is a finite set $\tau =\{R_1^{a_1},R_2^{a_2},\mathrm{\dots },R_{\mathrm{\ell }}^{a_{\mathrm{\ell }}}\}$ of relational symbols $R_i$ of arity $a_i$. A (finite, relational) $\tau$-structure $𝒮$ is a tuple $(U(𝒮),R_1^{𝒮},R_2^{𝒮},\mathrm{\dots },R_{\mathrm{\ell }}^{𝒮})$ with universe $U(𝒮)$ and interpretations $R_i^{𝒮}\subseteq U{(𝒮)}^{a_i}$. The size of $𝒮$ is $|𝒮|=|U(𝒮)|+{\sum }_{i=1}^{\mathrm{\ell }}{a}_i\cdot |R_i^{𝒮}|$. We denote the set of all $\tau$-structures by $\text{struc}[\tau ]$ – e.g., $\text{struc}[\{E^2\}]$ is the set of directed graphs.

Let $\tau$ be a vocabulary and $x_0,x_1,x_2,\mathrm{\dots }$ be an infinite repertoire of first-order variables. The first-order language $ℒ(\tau )$ is inductively defined, where the atomic formulas are the strings $x_i=x_j$ and $R_i(x_1,\mathrm{\dots },x_{a_i})$ for relational symbols $R_i\in \tau$. If $\alpha ,\beta \in ℒ(\tau )$ then so are $\neg (\alpha )$, $(\alpha \wedge \beta )$, and $\exists x_i(\alpha )$. A variable that appears next to $\exists$ is called quantified and free otherwise. We denote a formula $\phi \in ℒ(\tau )$ with $\phi (x_{i_1},\mathrm{\dots },x_{i_q})$ if $x_{i_1},\mathrm{\dots },x_{i_q}$ are precisely the free variables in $\phi$. A formula without free variables is called a sentence. As customary, we extend the language of first-order logic by the usual abbreviations, e.g., $\alpha \to \beta \equiv \neg \alpha \vee \beta$ and $\forall x_i(\alpha )\equiv \neg \exists x_i(\neg \alpha )$. To increase readability, we will use other lowercase Latin letters for variables and drop unnecessary braces by using the usual operator precedence instead. Furthermore, we use the dot notation in which we place a “$\mathrm{\bullet }$” instead of an opening brace and silently close it at the latest syntactically correct position. A $\tau$-structure $𝒮$ is a model of a sentence $\phi \in ℒ(\tau )$, denoted by $𝒮\vDash \phi$, if it evaluates to true under the semantics of quantified propositional logic while interpreting equality and relational symbols as specified by the structure. For instance, ${\phi }_{\mathrm{undir}}=\forall x\forall y\mathrm{\bullet }Exy\to Eyx$ over $\tau =\{E^2\}$ describes the set of undirected graphs, and we have $⊧φundir$ and $⊧̸φundir$.

We obtain the language of second-order logic by allowing quantification over relational variables of arbitrary arity, which we will denote by uppercase Latin letters. A relational variable is said to be monadic if its arity is one. A monadic second-order formula is one in which all quantified relational variables are monadic. The set of all such formulas is denoted by mso. The model checking problem for a vocabulary $\tau$ is the set ${\text{mc}}_{\tau }(\text{mso})$ that contains all pairs $(𝒮,\phi )$ of $\tau$-structures $𝒮$ and mso sentences $\phi$ with $𝒮\vDash \phi$. Whenever $\tau$ is not relevant (meaning that a result holds for all fixed $\tau$), we will refer to the problem as $\text{mc}(\text{mso})$. We note that in the literature there is often a distinction between ${\text{mso}}_1$- and ${\text{mso}}_2$-logic, which describes the way the input is encoded [20]. Since we allow arbitrary relations, we do not have to make this distinction.

While we consider graphs $G$ as relational structures $𝒢$ as discussed in the previous section, we also use common graph-theoretic terminology and denote with $V(G)=U(𝒢)$ and $E(G)=E^{𝒢}$ the vertex and edge set of $G$. Unless stated otherwise, graphs in this paper are undirected and we use the natural set notations and write, for instance, $\{v,w\}\in E(G)$. The degree of a vertex is the number of its neighbors. A tree decomposition of $G$ is a pair $(T,\chi )$ in which $T$ is a tree (a connected graph without cycles) and $\chi :V(T)\to 2^{V(G)}$ a function with the following two properties:

1. 1.

   for every $v\in V(G)$ the set $\{x\mid v\in \chi (x)\}$ is non-empty and connected in $T$;

2. 2.

   for every $\{u,v\}\in E(G)$ there is at least one node $x\in V(T)$ with $\{u,v\}\subseteq \chi (x)$.

The width of a tree decomposition is the maximum size of its bags minus one, i.e., $\mathrm{width}(T,\chi )={\max }_{x\in V(T)}|\chi (x)|-1$. The treewidth $\mathrm{tw}(G)$ of a graph $G$ is the minimum width any tree decomposition of $G$ must have. We do not require additional properties of tree decompositions, but we assume that $T$ is rooted at a $\mathrm{root}(T)\in V(T)$ and, thus, that nodes $t\in V(T)$ may have a $\mathrm{parent}(t)\in V(T)$ and $\mathrm{children}(t)\subseteq V(T)$. Without loss of generality, we may also assume $|\mathrm{children}(t)|\le 2$.

The definition of treewidth can be lifted to other objects by associating a graph to them. The most common graph for cnfs (or dnfs) $\psi$ is the primal graph $G_{\psi }$, which is the graph on vertex set $V(G_{\psi })=\mathrm{vars}(\psi )$ that connects two vertices by an edge if the corresponding variables appear together in a clause. We then define $\mathrm{tw}(\psi )≔\mathrm{tw}(G_{\psi })$ and refer to a tree decomposition of $G_{\psi }$ as one of $\psi$. Note that other graphical representations lead to other definitions of the treewidth of propositional formulas. A comprehensive listing can be found in the Handbook of Satisfiability [7, Chapter 17]. A labeled tree decomposition $(T,\chi ,\lambda )$ extends a tree decomposition with a mapping $\lambda :V(T)\to 2^{\psi }$ (i.e., a mapping from the nodes of $T$ to a subset of the clauses (or terms) of $\psi$) such that for every clause (or term) $C$ there is exactly one $t\in V(T)$ with $C\in \lambda (t)$ that contains all variables appearing in $C$. It is easy to transform a tree decomposition $(T,\chi )$ into a labeled one $(T,\chi ,\lambda )$ by traversing the tree once’s and by duplicating some bags. Hence, we will assume throughout this article that all tree decompositions are labeled.

A similar approach can be used to define tree decompositions of arbitrary structures: The primal graph $G_{𝒮}$ of a structure $𝒮$, in this context also called the Gaifman graph, has as vertex set the universe of $𝒮$, i.e., $V(G_{𝒮})=U(𝒮)$, and contains an edge $\{u,v\}\in E(G_{𝒮})$ iff $u$ and $v$ appear together in some tuple of $𝒮$. As before, we define $\mathrm{tw}(𝒮)≔\mathrm{tw}(G_{𝒮})$. One can alternatively define the concept of tree decompositions directly over relational structures, which leads to the same definition [17].

We use a quantifier elimination scheme that eliminates the most-inner quantifier block at the cost of introducing $O(2^k|\phi |)$ new variables while increasing the treewidth by a factor of $12\cdot 2^k$. Let first $\phi =Q_1{S}_1\mathrm{\dots }{\forall }_{\mathrm{\ell }}{S}_{\mathrm{\ell }}\mathrm{\bullet }\psi$ be the given qbf, in which $\psi$ is a dnf. Let further $(T,\chi ,\lambda )$ be the given labeled width-$k$ tree decomposition of $\phi$. We describe an encoding into a qbf, in which the last quantifier block $Q_{\mathrm{\ell }}{S}_{\mathrm{\ell }}$ gets replaced by new variables in $S_{\mathrm{\ell }-1}$.

We have to encode the fact that for an assignment on ${\bigcup }_{i=1}^{\mathrm{\ell }-1}{S}_i$ all assignments to $S_{\mathrm{\ell }}$ satisfy $\psi$, i. e., at least one term in $\psi .$ For that end, we introduce auxiliary variables for every term $d\in \mathrm{terms}(\psi )$ and any partial assignment $\alpha$ of the variables in $S_{\mathrm{\ell }}$ that also appear in the bag that contains $d$. More precisely, let ${\lambda }^{-1}(d)$ be the node in $V(T)$ with $d\in \lambda (t)$ and let $\alpha \mathrm{⊑}\chi ({\lambda }^{-1}(d))\cap S_{\mathrm{\ell }}$ be an assignment of the variables of the bag that are quantified by $Q_{\mathrm{\ell }}$. We introduce the variable ${\mathrm{𝑠𝑎𝑡}}_d^{\alpha }$ that indicates that this assignment satisfies $d$:

We have to track whether $\psi$ can be satisfied by a local assignment $\alpha$. For every $t\in V(T)$ and every $\alpha \mathrm{⊑}\chi (t)\cap S_{\mathrm{\ell }}$ we introduce a variable ${\mathrm{𝑠𝑎𝑡}}_{\le t}^{\alpha }$ that indicates that $\alpha$ can be extended to a satisfying assignment for the subtree rooted at $t$. Furthermore, we create variables for $t^{\prime }\in \mathrm{children}(t)$ that propagate the information about satisfiability along the tree decomposition. That is, is set to true if there is an assignment $\beta \mathrm{⊑}\chi (t^{\prime })\cap S_{\mathrm{\ell }}$ that can be extended to a satisfying assignment and that is compatible with $\alpha$:

Finally, since $Q_{\mathrm{\ell }}=\forall$, we need to ensure that for all possible assignments of $S_{\mathrm{\ell }}$ there is at least one term that gets satisfied. Since satisfiability gets propagated to the root of the tree decomposition by the aforementioned constraint, we can enforce this property with:

The following lemma observes the correctness of the construction, and the subsequent lemma handles the case $Q_{\mathrm{\ell }}=\exists$.

Recall that the input for pmc is a cnf $\psi$ and a set $X\subseteq \mathrm{vars}(\psi )$. The task is to count the assignments $\alpha \mathrm{⊑}X$ that can be extended to models ${\alpha }^{\ast }\mathrm{⊑}\mathrm{vars}(\psi )$ of $\psi$. We can also think of a formula $\psi (X)=\exists Y\mathrm{\bullet }{\psi }^{\prime }(X,Y)$ with free variables $X$ and existential quantified variables $Y$ (${\psi }^{\prime }$ is quantifier-free), for which we want to count the assignments to $X$ that make the formula satisfiable. The idea is to rewrite $\psi (X)=\exists Y\mathrm{\bullet }{\psi }^{\prime }(X,Y)\equiv \exists X\exists Y\mathrm{\bullet }{\psi }^{\prime }(X,Y),$ and to use a similar encoding as in the proof of Lemma 9 to remove the second quantifier.

In detail, we add a variable ${\mathrm{𝑠𝑎𝑡}}_c^{\alpha }$ for every clause $c\in \mathrm{clauses}(\psi )$ and every assignment of the corresponding bag $\alpha \mathrm{⊑}\chi ({\lambda }^{-1}(c))\cap Y$. The semantic of this variable is that the clause $c$ is satisfiable under the partial assignment $\alpha$. We further add the propagation variables ${\mathrm{𝑠𝑎𝑡}}_{\le t}^{\alpha }$ and for all $t\in V(T)$, $t^{\prime }\in \mathrm{children}(t)$, and $\alpha \mathrm{⊑}\chi ({\lambda }^{-1}(c))\cap Y$. The former indicates that the assignment $\alpha$ can be extended to a satisfying assignment of the subtree rooted at $t$; the later propagates partial solutions from children to parents within the tree decomposition:

Observe that the constraints (1)–(4) contain no variable from $Y$ (we removed them by locally speaking about $\alpha$) and, furthermore, constraints (1), (3), and (4) are pure propagations, which leave no degree of freedom on the auxiliary variables. Hence, models of these constraint only have freedom in the variables in $X$ within constraint (2). We are left with the task to count only models that actually satisfy the input formula, which we achieve with:

Let $\psi$ be a propositional formula and $X\subseteq \mathrm{lits}(\psi )$ be an arbitrary set of literals. A cardinality constraint ${\mathrm{card}}_{\bowtie c}(X)$ with $\bowtie \in \{\le ,=,\ge \}$ ensures that { at most, exactly, at least } $c$ literals of $X$ get assigned to true. Classic encodings of cardinality constraints increase the treewidth of $\psi$ by quite a lot. For instance, the naive encoding for ${\mathrm{card}}_{\le 1}(X)\equiv {\bigwedge }_{u,v\in X;u\ne v}(\neg u\vee \neg v)$ completes $X$ into a clique. We encode a cardinality constraint without increasing the treewidth by distributing a sequential unary counter:

To prove Lemma 11 we construct a qbf for a given mso sentence $\phi$, structure $𝒮$, and tree decomposition of $𝒮$. We first define the primary variables of $\psi$, i.e., the prefix of $\psi$ (primary here refers to the fact that we will also need some auxiliary variables later). For every second-order quantifier $\exists X$ or $\forall X$ we introduce, as we did in the introduction, an indicator variable $X_u$ for every element $u\in U(𝒮)$ with the semantic that $X_u$ is true iff $u\in X$. These variables are either existentially or universally quantified, depending on the second-order quantifier. If there are multiple quantifiers (say $\exists X\forall Y$), the order in which the variables are quantified is the same as the order of the second-order quantifiers. For first-order quantifiers $\exists x$ or $\forall x$ we do the same construction, i.e., we add variables $x_u$ for all $u\in U(𝒮)$ with the semantics that $x_u$ is true iff $x$ was assigned to $u$. Of course, of these variables we have to set exactly one to true, which we enforce by adding ${\mathrm{card}}_{=1}(\{x_u\mid u\in U(𝒮)\})$ using Lemma 12.

The last ingredient of our qbf encoding is the evaluation of the atoms in the mso sentence $\phi$. An atom is $R{x}_1,\mathrm{\dots },x_a$ for a relational symbol $R$ from the vocabulary of arity $a$, containment in a second-order variable $Xu$, equality $x=y$, and the negation of the aforementioned. For every atom $\iota$ that appears in $\phi$ we introduce variables $p_t^{\iota }$ and $p_{\le t}^{\iota }$ for all $t\in V(T)$ that indicate that $\iota$ is true in bag $t$ or somewhere in the subtree rooted at $t$, respectively. Note that the same atom can occur multiple times in $\phi$, for instance in

there are two atoms $x=y$. However, since $\phi$ is in prenex normal form (and, thus, variables cannot be rebound), these always evaluate in exactly the same way. Hence, it is sufficient to consider the set of atoms, which we denote by $\mathrm{atoms}(\phi )$. We can propagate information about the atoms along the tree decomposition with:

This encoding introduces two variables per atom $\iota$ per bag $t$ (namely $p_t^{\iota }$ and $p_{\le t}^{\iota }$), which increases the treewidth by at most $2\cdot |\mathrm{atoms}(\phi )|$. To synchronize with the two children $t^{\prime }$ and $t^{\prime \prime }$, we add $p_{\le t^{\prime }}^{\iota }$ and $p_{\le t^{\prime \prime }}^{\iota }$ to $\chi (t)$, yielding a total treewidth of at most $4\cdot |\mathrm{atoms}(\phi )|$.

An easy atom to evaluate is $x=y$, since if $x$ and $y$ are equal (i.e., they both got assigned to the same element $u\in U(𝒮)$), we can conclude this fact within a bag that contains $u$:

For every $u\in U(𝒮)$ and every quantifier $\exists x$ (or $\forall x$), we add the propositional variable $x_u$ to all bags containing $u$. We increase the treewidth by at most the quantifier rank and, in return, cover constraints as the above trivially. Similarly, if there is a second-order variable $X$ and a first-order variable $x$, the atom $Xx$ can be evaluated locally in every bag:

We have to evaluate atoms corresponding to relational symbols $R$ of the vocabulary. For each such symbol of arity $a$ we encode:

Here “$R(x_1,x_2,\mathrm{\dots },x_a)$” is an atom in which $R$ is a relational symbol and $x_1,x_2,\mathrm{\dots },x_a$ are quantified first-order variables. In the inner “big-or” we consider all $u_1,\mathrm{\dots },u_a$ in $\chi (t)$, i.e., elements $u_1,\mathrm{\dots },u_a\in U(𝒮)$ that are in the relation $(u_1,\mathrm{\dots },u_a)\in R^{𝒮}$. Then “${(x_i)}_{u_i}$” is a variable that describes that $x_i$ gets assigned to $u_i$. Note that all tuples in $R^{𝒮}$ appear together in at least one bag of the tree decomposition and, hence, there is at least one bag $t$ for which $p_t^{R(x_1,x_2,\mathrm{\dots },x_a)}$ can be evaluated to true. The propagation ensures that, for every $\iota \in \mathrm{atoms}(\phi )$, the variable $p_{\le \mathrm{root}(T)}^{\iota }$ will be true iff $\iota$ is true. Since the quantifier-free part of $\phi$ is a cnf ${\bigwedge }_{j=1}^p{\psi }_j$, we can encode it by replacing every occurrence of $\iota$ in ${\psi }_j$ with $p_{\le \mathrm{root}(T)}^{\iota }$.

For the readers convenience, we compiled the encoding into Figure 1. Combining the insights of the last sections proves Lemma 11, but if the inner-most quantifier is universal, existentially projecting the encoding variables would produce a qbf with one more block. This can, however, be circumvent using Lemma 13. We formally prove that “combining the insights” indeed leads to a sound proof of Lemma 11 in the technical report.

For qsat one can “move” complexity from the quantifier rank of the formula to its treewidth and vice versa [16]. By Lemma 16, this means that any reduction from qsat to mc(mso) may produce an instance with small treewidth or quantifier alternation while increasing the other. We show that one can also decrease the treewidth by increasing the block size.