# Treewidth relations between Boolean formulas and Tseitin encodings

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.

• Seems that in some cases it can increase quite a bit and it depends on the particular way you represent $\lnot \phi$ as a circuit. Consider a CNF $\phi = \bigwedge_{i \in [n-1]}(x_i \lor x_{i+1})$. Its primal graph is a path. Then let the large conjunction in $\phi$ be represented as a tree such that $(x_i \lor x_{i+1})$ and $(x_{i+\sqrt{n}} \lor x_{i+\sqrt{n}+1})$ share the parent. Then the primal graph of the new formula should have a $\Omega(\sqrt{n}) \times \Omega(\sqrt{n})$ grid minor. Apr 18, 2022 at 17:42

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

 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

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 ) 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:

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

• Interesting, I never tried to have this result directly as incidence treewidth is usually enough for tractability. Now, you could recover this result from my Lemma 2 + and an adaptation of Lemma 4 (a bit hidden) of Marko Samer, Stefan Szeider: Constraint satisfaction with bounded treewidth revisited. J. Comput. Syst. Sci. 76(2): 103-114 (2010) where they "roughly" prove that a CNF of itw k can be encoded into a 3-CNF of itw k, hence of primal treewdith 3k.
– holf
Dec 9, 2022 at 15:53
• Yes that makes sense. Thank you for the reference. Dec 12, 2022 at 12:01
• You are welcome. This is a nice paper but what is proven in Lemma 4 is not spilled out as I have written it in my previous comment hence the result is not that well-known. Actually, Stefan Szeider told me about it or I would have missed the connection!
– holf
Dec 12, 2022 at 13:03