1 files changed, 39 insertions, 0 deletions
diff --git a/content/zettel/2d4.md b/content/zettel/2d4.md
new file mode 100644
index 0000000..f444552
--- /dev/null
+++ b/content/zettel/2d4.md
@@ -0,0 +1,39 @@
++++
+title = "Tseitin transformation"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["2d3"]
+forwardlinks = ["2d5"]
+zettelid = "2d4"
++++
+
+The Tseitin transformation is a way to transform a general formula into
+CNF form, by basically taking each sub-formula and assigning it to be
+equivalent to the original formula. Therefore the following formula can
+be created into the following CNF form, which only grows linearly in the
+number of clauses compared to the input.
+
+$$\phi = (a \land b) \lor c$$
+
+We can then set $x_1 \leftrightarrow a \land b$ and
+$x_2 \leftrightarrow x_1\lor c$. We can then transform the equivalence
+to the following form in terms of $\land$ and $\lor$.
+
+$$ x_1 \leftrightarrow a \land b \equiv (x_1 \rightarrow a \land b) \land (a\land b \rightarrow x_1) $$
+$$\equiv (\neg x_1 \lor (a \land b)) \land (\neg (a\land b) \lor x_1)$$
+$$\equiv (\neg x_1 \lor a) \land ( \neg x_1 \lor b) \land(\neg a \lor \neg b \lor x_1)$$
+
+For $\lor$ we can proceed in the same way:
+
+$$ x_2 \leftrightarrow x_1 \lor c \equiv (\neg x_2 \lor (x_1 \lor c)) \land(\neg (x_1 \lor c) \lor x_2) $$
+$$\equiv (\neg x_2 \lor x_1 \lor c) \land (\negx_1 \lor x_2) \land (\neg c \lor x_2)$$
+
+Then we can transform the formula in the following way:
+
+$$T(\phi) = x_2 \land (x_2 \leftrightarrow x_1 \lor c) \land (x_1\leftrightarrow a \land b) $$
+$$ = x_2 \land (\neg x_2 \lor x_1 \lor c) \land(\neg x_1 \lor x_2) \land (\neg c \lor x_2) \land (\neg x_1 \lor a) \land ( \negx_1 \lor b) \land (\neg a \lor \neg b \lor x_1) $$
+
+These two formulas are therefore equisatisfiable, as whenever the input
+is satisfiable, the output will also be satisfiable. These are, however,
+not equivalent, because the second formula has additional variables.