Vtyjkyuk

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 $texttttseitin-encoding(varphi) = A land bigwedge B$
where $(A, B) = varphi^*$

Now, I am trying to show that $texttttseitin-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?

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 $texttttseitin-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 lorbeta$.