Transformation de Tseitin

En logique, la transformation de Tseitin prend un circuit logique et produit une formule booléenne équisatisfiable en forme normale conjonctive. La transformation est linéaire. Elle a été développée par le mathématicien russe Grigori Tseitin.

Motivation

L'approche naïve consiste à écrire le circuit sous forme d'expression booléenne et à utiliser la loi de De Morgan et la distributivité pour le convertir en forme normale conjonctive. Cependant, cela peut entraîner une augmentation exponentielle de la taille de l'équation. La transformation de Tseitin génère une formule dont la taille augmente linéairement par rapport à celle du circuit d'entrée.

Approche

L'équation de sortie est la constante 1 égale à une expression. Cette expression est une conjonction de sous-expressions, où la satisfaction de chaque sous-expression impose le bon fonctionnement d'une seule porte dans le circuit d'entrée. La satisfaction de l'expression de sortie entière impose donc que l'ensemble du circuit d'entrée opère correctement.

Pour chaque porte, une nouvelle variable représentant sa sortie est introduite. Une petite expression CNF précalculée qui relie les entrées et les sorties est ajoutée (via l'opération "et") à l'expression de sortie. Notez que les entrées de ces portes peuvent être soit les littéraux d'origine, soit les variables introduites représentant les sorties des sous-portes.

Bien que l'expression de sortie contienne plus de variables que l'entrée, elle reste équisatisfiable, ce qui signifie qu'elle est satisfiable si, et seulement si, l'équation d'entrée d'origine est satisfiable. Lorsqu'une affectation satisfaisante de variables est trouvée, ces affectations pour les variables introduites peuvent simplement être supprimées.

Une clause finale est ajoutée avec un seul littéral : la variable de sortie de la porte finale.

Exemple

Considérons la formule suivante $\phi$ .

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

Considérons toutes les sous-formules (à l'exception des variables simples):

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

On introduit une nouvelle variable pour chaque sous-formule:

${\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}}$

On fait la conjonction de toutes ces substitution et de la substitution de $\phi$:

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

Toutes les substitutions peuvent être transformées en CNF, par exemple

${\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}}$

Notes et références

Grigori Tseitin est un mathématicien et informaticien russe.