One sided Tseytin Encoding is equisatisfiable

Question

I am trying to show that the one sided Tseytin Encoding of a Formula in negative normal form with $\lor$ and $\land$ is equisatisfiable with the formula itself. By one sided, I mean I use one way implications instead of two way implications.

Since a formal definition of this transformation was not available, I tried to come up with my own.

First, given a formula $\varphi$, define $\varphi^*$ to be as follows:

1. If $\varphi = p$ (respectively, $\neg p$) is a literal, define $p^* = (x_p, \{\})$ (respectively, $(\neg p)^*= (\neg x_p, \{ \} )$)
2. If $\varphi = \alpha \lor \beta$, define $\varphi^* = (x_\alpha \lor x_\beta, \{x_\alpha \rightarrow u_\alpha\} \cup \{x_\beta \rightarrow u_\beta\} \cup X_\alpha \cup X_\beta)$ where $x_\alpha, > x_\beta$ are fresh variables, $(u_\alpha, X_\alpha) = \alpha^*$ and $(u_\beta, X_\beta) = \beta^*$
3. If $\varphi = \alpha \land \beta$, define $\varphi^* = (x_\alpha \land x_\beta, \{x_\alpha \rightarrow u_\alpha\} \cup \{x_\beta \rightarrow u_\beta\} \cup X_\alpha \cup X_\beta)$ where $x_\alpha, > x_\beta$ are fresh variables, $(u_\alpha, X_\alpha) = \alpha^*$ and $(u_\beta, X_\beta) = \beta^*$

Now, define $\texttt{tseitin-encoding}(\varphi) = A \land \bigwedge B$ where $(A, B) = \varphi^*$

Now, I am trying to show that $\texttt{tseitin-encoding}(\varphi)$ is satisfiable iff $\varphi$ is. My attempt was to show by induction that for any $\alpha$, the first component of $\alpha^*$ is satisfiable if and only if $\alpha$ is, and the second component always is.

However, I cannot seem to make progress with this. Is my definition correct? How do I show this result?

Answer 1

Your definition does work, but your line of argument isn't quite right. The proof is easier if you use slightly different naming conventions: In the clause for literals, it is better to use $p$ rather than $x_p$ and in the clauses for conjunctions and disjunctions, the fresh variables introduced in the construction of $\alpha^*$ and $\beta^*$ need to be renamed as necessary to ensure that the only variables that $\alpha^*$ and $\beta^*$ have in common are the original variables of $\phi$.

Let's write $T(\phi)$ for your $\texttt{tseitin-encoding}(\phi)$. Here $\phi$ and hence all its sub formulas are assumed to be in negation-normal form. Let's show by induction on the structure of $\phi$, that a satisfying assignment for $T(\phi)$ restricts to a satisfying assignment for $\phi$ and that a satisfying assignment for $\phi$ extends to one for $T(\phi)$. This clearly implies that $T(\phi)$ is satisfiable iff $\phi$ is.

In the base case, $\phi$ is a literal, i.e., $p$ or $\lnot p$ where $p$ is a variable. We have, $T(p) \equiv p$ and $T(\lnot p) \equiv \lnot p$, i.e., $T(\phi) \equiv \phi$ and there is nothing to prove.

If $\phi \equiv \alpha \land \beta$, then $T(\phi) \equiv x \land y \land (x \to T(\alpha)) \land (y \land T(\beta))$ where $x$ and $y$ are variables that do not occur in $\phi$. Let $I$ be a satisfying assignment for $\phi$, then $I$ restricts to satisfying assignments $J$ and $K$ for $\alpha$ and $\beta$ respectively and, by induction, these extend to satisfying assignments $J'$ and $K'$ say for $T(\alpha)$ and $T(\beta)$ respectively. As the only variables that $T(\alpha)$ and $T(\beta)$ have in common are the original variables of $\phi$ and as $I = J \cup K$ is a satisfying assignment for $\phi$, $I' = J' \cup K' \cup \{x \mapsto \top, y \mapsto \top\}$ is a satisfying assignment for $T(\phi)$. Conversely if $I'$ is a satisfying assignment for $\phi \equiv \alpha \land \beta$, by induction, $I'$ restricts to satisfying assignments $J$ and $K$ for $\alpha$ and $\beta$ respectively and then $I = J \cup K$ is the restriction of $I'$ to the variables in $\phi$ and is a satisfying assignment for $\phi$.

The case when $\phi \equiv \alpha \lor \beta$ is similar: $T(\phi) \equiv (x \lor y) \land (x \to T(\alpha)) \land (y \land T(\beta))$. Let $I$ be a satisfying assignment for $\phi$, so that $I$ restricts to a satisfying assignment $J$ for one of $\alpha$ or $\beta$, say $\alpha$. But then, by induction, $J$ extends to a satisfying assignment $J'$ for $T(\alpha)$ and then $I$ extends to a satisfying assignment $I' = J' \cup K' \cup \{ x \mapsto \top, y \mapsto \bot\}$ for $T(\phi)$, where $K'$ is an arbitrary assignment to the variables of $T(\beta)$ that do not occur in $T(\alpha)$. Conversely if $I'$ is a satisfying assignment for $T(\phi)$, $I$ maps one of $x$ or $y$ to $\top$, say $x$. But then as $I'$ satisfies $T(\phi)$ and $T(\phi)$ implies $x \to T(\alpha)$, $I'$ restricts to a satisfying assignment for $T(\alpha)$ and hence to a satisfying assignment for $\phi \equiv \alpha \lor\beta$.