Time-to-time transformation

The Zeitin transformation (also Zeitin method , Tseitin transformation , Tseitin method ) describes a method with which formulas from propositional logic can be converted to a conjunctive normal form (CNF). The resulting conjunctive normal form is not equivalent , but only equivalent to satisfiability . The process was developed by Grigori Zeitin .

motivation

Conventionally, equivalence transformations such as De Morgan's Laws , the Distributive Law and others are used to convert any propositional formula into a conjunctive normal form .

Applying the distributive law can generally lead to an exponential increase in the number of conjunctions . In order to limit this increase, the formula is converted into a form that can be satisfied .

For an example with 2 clauses with 4 variables each, to which the distributive law is applied, one can see the resulting exponential increase in the conjunctions:

${\displaystyle {\begin{aligned}(p_{1}\land p_{2}\land p_{3}\land p_{4})\lor (q_{1}\land q_{2}\land q_{3}\land q_{4})\equiv \;&(p_{1}\lor q_{1})\land (p_{1}\lor q_{2})\land (p_{1}\lor q_{3})\land (p_{1}\lor q_{4})\land \\&(p_{2}\lor q_{1})\land (p_{2}\lor q_{2})\land (p_{2}\lor q_{3})\land (p_{2}\lor q_{4})\land \\&(p_{3}\lor q_{1})\land (p_{3}\lor q_{2})\land (p_{3}\lor q_{3})\land (p_{3}\lor q_{4})\land \\&(p_{4}\lor q_{1})\land (p_{4}\lor q_{2})\land (p_{4}\lor q_{3})\land (p_{4}\lor q_{4})\end{aligned}}}$

idea

By using a transformation that is equivalent to satisfiability , it is possible to introduce variables during the transformation .

The basic idea is to introduce a variable for each sub-formula. With the help of propositional equivalence , these sub-formulas are then connected with the new variables and all resulting conditions are conjugated with one another. After that, each of these conditions is brought to KNF separately.

example

The example is to be shown here using the formula . ${\displaystyle \phi }$

${\displaystyle \phi :=((p\lor q)\land r)\to (\neg s)}$

First, all sub-formulas are listed according to their length:

${\displaystyle {\begin{aligned}&\neg s\\&p\lor q\\&(p\lor q)\land r\\&((p\lor q)\land r)\to (\neg s)\end{aligned}}}$

Now 4 variables are introduced and linked to the subformulas using the biconditional . On this occasion, sub-formulas are already substituted by corresponding variables:

${\displaystyle {\begin{aligned}x_{1}&\leftrightarrow \neg s\\x_{2}&\leftrightarrow p\lor q\\x_{3}&\leftrightarrow x_{2}\land r\\x_{4}&\leftrightarrow x_{3}\to x_{1}\end{aligned}}}$

Now all of these substitutions are conjugated. It is important that the variable that stood for the original formula is added as a separate conjunct. ${\displaystyle \phi }$

The corresponding new formula looks like this:

${\displaystyle T(\phi ):=x_{4}\land (x_{4}\leftrightarrow x_{3}\to x_{1})\land (x_{3}\leftrightarrow x_{2}\land r)\land (x_{2}\leftrightarrow p\lor q)\land (x_{1}\leftrightarrow \neg s)}$

Now all the conjuncts have to be converted separately into CNF, which are carried out with the usual equivalent conversions. This is exemplified by a conjunct:

${\displaystyle {\begin{aligned}x_{2}\leftrightarrow p\lor q&\equiv x_{2}\to (p\lor q)\land ((p\lor q)\to x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg (p\lor q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land ((\neg p\land \neg q)\lor x_{2})\\&\equiv (\neg x_{2}\lor p\lor q)\land (\neg p\lor x_{2})\land (\neg q\lor x_{2})\end{aligned}}}$

Note that the distributive law was applied again in the last step, but in this step there is only a constant increase in conjunctions.

In the end, this transformation is applied to all conjuncts and the resulting CNF is equivalent to the initial formula and generally has fewer clauses. It may happen that this does not apply to smaller formulas.

Since the variable that stands for the original formula is (here:) part of the constructed formula, trivially applies . Conversely, every model of can be expanded so that it is also a model of . For this purpose, the introduced variables (here:) are each set in such a way that they meet the required equivalence under the interpretation . ${\displaystyle x_{4}}$ ${\displaystyle T(\phi )\models \phi }$ ${\displaystyle \alpha }$ ${\displaystyle \phi }$ ${\displaystyle T(\phi )}$ ${\displaystyle x_{i}}$ ${\displaystyle \alpha }$

It is therefore satisfiable if and only if it is satisfiable, and every satisfying assignment of is also a satisfying assignment of . This is an advantage because it has fewer clauses and it is therefore easier to find a satisfactory assignment than on the original formula. ${\displaystyle T(\phi )}$ ${\displaystyle \phi }$ ${\displaystyle T(\phi )}$ ${\displaystyle \phi }$ ${\displaystyle T(\phi )}$

Extension according to Plaisted and Greenbaum

This extension of the classic Zeitin method uses the concept of polarity (NV Murray, 1982) as an essential component.

polarity

Polarity describes the parity of the number of negations in the syntax tree of a propositional formula from the root node to the desired node. Accordingly, a node which has an odd number of negations from the root symbol to it has a negative polarity (corresponding to an even number of negations and positive polarity).

With the extension according to Plaisted and Greenbaum there are two essential differences to the normal Zeitin transformation:

1. The polarity of a sub-formula has no effect on the introduction of new variables.
2. Instead of bi- implication , an implication is introduced for each new variable .

The direction of the introduced implication depends on the polarity:

In the case of a partial formula with positive polarity, the new variable is introduced as follows: ${\displaystyle p\land q}$ ${\displaystyle x}$

${\displaystyle {\begin{aligned}x\rightarrow (p\land q)\end{aligned}}}$

The same sub-formula is replaced with negative polarity as follows:

${\displaystyle {\begin{aligned}(p\land q)\rightarrow x\end{aligned}}}$

In general, these two changes have the effect that the resulting CNF is smaller than with the Zeitin transformation, as long as not all sub-formulas occur in both polarities.

Future research will deal with heuristics for the appropriate introduction of new variables, so that not all subformulas lead to an increase in the number of variables.

swell

• GS Zeitin: On the complexity of derivation in propositional calculus. Leningrad Seminar on Mathematical Logic, 1970.
• DA Plaisted, S. Greenbaum: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation, 1986, doi : 10.1016 / S0747-7171 (86) 80028-1