2
$\begingroup$

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?

$\endgroup$
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.