blob: f4445528713f712dbc52ec18b971612054218cfb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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.
|
