Treewidth relations between Boolean formulas and Tseitin encodings

Question

Suppose you have a propositional formula $\varphi$ in CNF. You want to efficiently obtain an equisatisfiable CNF formula encoding $\neg \varphi$. You use the usual Tseitin encoding with auxiliary variables. Now,

Question. If the primal treewidth of $\varphi$ is $k$, what is the primal treewidth of $\neg\varphi$ after transforming into CNF via the Tseitin procedure? Is it bounded by some function of $k$, or does it depend on the entire size of $\varphi$?

Here by primal treewidth I mean the treewidth of the primal graph of $\varphi$, that is, the graph where the nodes are the variables of the formula and two nodes are connected if the corresponding variables appear together in some clause.

Answer 1

There is a relation between the treewidth of a circuit and the primal treewidth of its Tseitin transformation but you will have to take the fan-in of the circuit into account, which is large when considering a naive circuit for $\neg \phi$ as you have a conjunction whose fan-in is the number of clauses of $\phi$ (even if you push the negation to the input to have a DNF-representation of $\neg \phi$, you have a large fan-in $\vee$-gate in the circuit).

Notations and definitions: For a Boolean circuit $C$, the treewidth of $C$, $tw(C)$, is the treewidth of the underlying graph of $C$ where inputs having the same label have been identified. We denote by $tseit(C)$ the Tseitin transform of $C$. It has one variable $x_u$ per gate of $C$. For each internal gates $u$ with input $u_1, \dots, u_k$ computing $f_u(u_1, \dots, u_k)$, it has several clauses $\mathcal{F}(u)$ on variables $x_u, x_{u_1}, \dots, x_{u_k}$. The conjunction of $\mathcal{F}$ is logically equivalent to $x_u \Leftrightarrow f(x_{u_1}, \dots, x_{u_k})$.

We have the following:

Lemma 1: The primal treewidth of $tseit(C)$ is at most $(k+1) \cdot (tw(C)+1)-1$, where $k$ is the fan-in of $C$.

Proof (sketch): Let $T$ be a tree decomposition of (the underlying graph of) $C$ of width $w$. We will transform it into a tree decomposition of $tseit(C)$. For every gate $u$ of $C$ with input $u_1, \dots, u_k$, there is a variable $x_u$ in $tseit(C)$ and clauses involving $x_u, x_{u_1}, \dots, x_{u_k}$.

We thus define $T'$ by replacing every occurrence of $u$ in $T$ by $x_u, x_{u_1}, \dots, x_{u_k}$. It can be verified that $T'$ is a tree decomposition of width $(k+1)(w+1)-1$ of the primal graph of $tseit(C)$.

$\square$

You cannot remove the dependency in the fan-in since a gate of fan-in $k$ in a circuit will be translated into a clause of size $(k+1)$ in $tseit(C)$, hence a $(k+1)$-clique in the primal graph. Artur Riazanov's comment shows that you cannot avoid this even by rewriting your large fan-in gates into trees of fan-in $2$.

This is however not the end of the story. You have a better relation between the incidence treewidth of $tseit(C)$ and the treewidth of $C$. And in turn, between the incidence treewidth of $\phi$ and the treewidth of $\neg \phi$.

I do not have any reference for this however and I would not tag it as folklore neither but it is known by some people working in parametrized complexity of SAT (I think the first time I discussed this was with Stefan Mengel on a simplification of the proof in [1, Section 4] showing thatbounded tw circuits can be transformed in FPT-size d-DNNF).

Lemma 2: The incidence treewidth of $tseit(C)$ is at most $2\cdot tw(C)+1$.

Proof: The incidence graph $G_C$ of $tseit(C)$ has vertices $x_u$ (corresponding to variable $x_u$ of $tseit(C)$) and $c_u$ (corresponding to clauses encoding that $x_u$ functionnally depends on $x_{u_1},\dots,x_{u_k}$) for each gate $u$ with input $u_1, \dots, u_k$. The edges of $G_C$ are of the form $(c_u, x_u)$ or $(c_u, x_v)$ where $v$ is an input of $u$, that is, when $(u,v)$ is an edge of $C$.

Thus, if $T$ is a tree decomposition of $C$ of width $w$, replacing occurrences of $u$ in $T$ by $C_u, x_u$ gives a tree decomposition $T'$ of $G_C$. Indeed, in $T'$, bags containing $x_u$ (or $c_u$) are connected since they exactly correspond to bags containing $u$ in $T$, which are connected by definition. And every edge of $G_C$ are covered in $T'$: edges of the form $(c_u, x_u)$ are covered in every bag of $T'$ corresponding to bags containing $u$ in $T$. And edges of the form $(c_u, x_v)$ are covered by the bag of $T'$ corresponding to the bag of $T$ containing both $u$ and $v$ (this bag exists since $(u,v)$ is an edge of $C$).

Clearly the largest bag of $T'$ has size $2(w+1)$ and thus, has treewidth $2w+1$.

$\square$

Now, interestingly, there is a clean relation between the incidence treewidth of a CNF $\phi$ and the treewidth of its circuit. Let $C_{\neg \phi}$ be the folowing circuit for $\neg \phi$: for each clause $c$ of $\phi$, we have a $\wedge$-gate $v_c$, for each variable $x$, we have a corresponding input $i_x$ labeled by $x$ and a negation gate $n_x$ having $i_x$ as input. If $x$ appears positively in clause $c$, we connect $n_x$ to $v_c$. If $x$ appears negatively in $c$, we connect $i_x$ to $v_c$. Finally, we have a large $\vee$-gate $v_{out}$ having every $v_c$ as input.

Lemma 3: Let $\phi$ be a CNF-formula of incidence treewidth $w$. $C_{\neg \phi}$ computes $\neg \phi$ and the treewidth of $C_{\neg \phi}$ is at most $2 \cdot (w+1)$.

Proof (sketch): $C_{\neg \phi}$ is clearly the circuit given by pushing the top negation of $\neg \phi$ to the input using De Morgan. Now given a tree decomposition of the incidence graph of $\phi$, it can be readily verified that we get a decomposition of $C_{\neg\phi}$ by replacing every occurrence of $c$ by $v_c$, every occurrence of $x$ by $n_x$ and $i_x$ and add $v_{out}$ in every bag.

$\square$

Lemma 1 and 2 together give:

Theorem: Let $\phi$ be a CNF-formula of incidence treewidth $w$. The incidence treewidth of $tseit(C_{\neg \phi})$ is at most $4w+5$.

References

[1] Connecting Knowledge Compilation Classes and Width Parameters, Antoine Amarilli, Florent Capelli, Mikaël Monet, Pierre Senellart, Theory of Computing Systems, 2020. https://arxiv.org/abs/1811.02944

Answer 2

Actually, we can transform any Boolean Circuit $C$ that uses only $\wedge$, $\vee$, and $\neg$ gates of treewidth $k$ into a CNF whose primal treewidth is within a constant factor of $k$, where this constant factor does not depend on the fan-in/fan-out.

However, in order to do this, we need to be given a tree decomposition of $C$ that has width $k$.

In fact, we can prove the following:

Lemma: Let $C$ be a circuit and $(T,\chi)$ a tree decomposition of $C$ with width $k$. Then we can construct in polynomial time a CNF $\phi$ such that $C$ and $\phi$ have the same number of models, have the same models restricted to the original labels of $C$, and such that the primal treewidth of $\phi$ is less or equal to $4(k+1)$.

Intuitively, this works by introducing auxiliary variables $v_{x,t}$ for each gate $x$ and vertex $t$ of the tree decomposition, where $v_{x,t}$ denotes the truth value of the gate $x$ taking into account the inputs that occur in $t$ or below in the tree decomposition.

Proof: We let $\ell(x)$ for $x$ a gate in $C$ denote the label/type of the gate $x$. For inputs $v \in \mathcal{V}$, we let $\ell(v) = v$.

Let $(T, \chi)$ be a tree decomposition of width $k$ for $C$. We construct a CNF $\psi$ as the set containing the following clauses:

• for $x \in \chi(t), \ell(x) = \wedge$ we add \begin{align*} v_{x,t} \leftrightarrow \left(\bigwedge_{t' \in child(t), x \in \chi(t')} v_{x,t'} \right) \wedge \left(\bigwedge_{y \in parent(x), y \in \chi(t)} y\right), \end{align*} where $child(t)$ is the set of children (i.e. direct descendants) of $t$ in the tree $T$ and $parent(x)$ is the set of parents (i.e. direct ancestors) of $x$ in the DAG $C$.
• for $x \in \chi(t), \ell(x) = \vee$ we add \begin{align*} v_{x,t} \leftrightarrow \left(\bigvee_{t' \in child(t), x \in \chi(t')} v_{x,t'} \right) \vee \left(\bigvee_{y \in parent(x), y \in \chi(t)} y\right), \end{align*} where $child(t)$ is the set of children (i.e. direct descendants) of $t$ in the tree $T$ and $parent(x)$ is the set of parents (i.e. direct ancestors) of $x$ in the DAG $C$.
• for $x,y \in \chi(t), \ell(x) = \neg, parent(x) = \{y\}$ we add $$ x \leftrightarrow \neg y $$
• for $x_{root}$ the output node of $C$ $$ x_{root} $$ Finally, we obtain $\phi$ by replacing, for $x \in \chi(t), \ell(x) \in \{\wedge, \vee\}, x \not \in t', \{t'\} = parent(t)$, the variable $x$ by $v_{x,t}$ in every clause of $\psi$.

We define $(T, \chi')$, a tree decomposition for $\phi$, by letting \begin{align*} \chi'(t) = \chi(t) \cup \{v_{x,t'} \mid x \in \chi(t')\cap \chi(t), t' \in child(t) \cup \{t\}, \ell(x) \not\in \mathcal{V}\}. \end{align*} Since, w.l.o.g., we can assume that for each $t \in V(T)$ it holds that $|child(t)| \leq 2$ (this holds for example when we have a nice tree decomposition [1]) we see that \begin{align*} |\chi'(t)| &= |\chi(t) \cup \{v_{x,t'} \mid x \in \chi(t')\cap \chi(t), t' \in child(t) \cup \{t\}, \ell(x) \not\in \mathcal{V}\}|\\ &= |\chi(t)| + |\{v_{x,t'} \mid x \in \chi(t')\cap \chi(t), t' \in child(t) \cup \{t\}, \ell(x) \not\in \mathcal{V}\}|\\ &\leq k + 1 + 3(k+1) = 4(k + 1) \end{align*}

$\square$

Note that actually an even tighter bound of $3(k+1)$ holds for this construction. This is shown by not adding $v_(x,t)$ and $v(x,t')$ for the children $t'$ all at the same time. Instead, we have $v(x,t')$ for the both children in the beginning. Then, we add $v(x, t)$, allowing us to remove $v(x,t')$ for the children. By doing this step by step for each of the gates $x$ we obtain the desired bound.

Thus, to answer the original question is you have a circuit $C$ of treewidth $k$, then there is a circuit $C'$ which corresponds to the negation of $C$ (we just add an additional gate that negates the output gate of $C$) of treewidth $k$ ($+1$ if the treewidth of $C$ was $0$). Then we can use the construction in the proof of the above lemma to obtain a CNF representing $C$ with primal treewidth $3(k + 1)$.

References:

[1] Ernst Althaus and Sarah Ziegler. Optimal tree decompositions revisited: A simpler linear-time fpt algorithm. arXiv preprint arXiv:1912.09144, 2019.