Tseitin-transformatie

In de logica is de Tseitin-transformatie (ook Tseitin-afgeleide genoemd) een manier om een propositie in lineaire tijd om te zetten naar een vervulbaarheidsequivalente propositie in conjunctieve normaalvorm. De Tseitin-transformatie kan bijvoorbeeld worden gebruikt bij het DPLL-algoritme en resolutie, bewijstechnieken in automatische stellingbewijzers.

De Tseitin-transformatie is vernoemd naar G.S. Tseitin die het publiceerde in 1968.

Belang

Met behulp van de regels van De Morgan en distributiviteit kan elke propositie naar een equivalente propositie in conjunctieve normaalvorm worden omgezet. Hierbij is het echter mogelijk dat de lengte van de propositie exponentieel stijgt. Met de Tseitin-transformatie kan een propositie naar conjunctieve normaalvorm omgezet worden die slechts een bepaalde factor langer is dan de oorspronkelijke propositie, wat voor veel toepassingen een belangrijke eigenschap is. Hierbij verkijgt men echter geen equivalente propositie, maar slechts een vervulbaarheidsequivalente.

Werking

De vervulbaarheidsequivalente formule wordt geconstrueerd door elke (sub)formule in de oorspronkelijke propositie een naam te geven en de onderlinge equivalenties tussen deze subformules uit te drukken. Een voorbeeld hiervan is $r\equiv s\wedge t$, wat gelezen kan worden als $(r\rightarrow (s\wedge t))\wedge ((s\wedge t)\rightarrow r)$. Hierbij wordt begonnen bij de gehele propositie en vervolgens wordt deze procedure recursief herhaald voor elke subformule. Deze equivalenties worden met conjuncties samengevoegd waardoor één formule ontstaat.

Nadat de verbanden tussen de subformules zijn uitgedrukt, wordt elke subformule omgezet naar een formule in conjunctieve normaalvorm; deze kunnen van tevoren berekend worden voor alle connectieven. Een voorbeeld hiervan is:

$p\equiv q\wedge r$ is in conjunctieve normaalvorm: $(p\vee \neg q\vee \neg r)\wedge (\neg p\vee q)\wedge (\neg p\vee r)$

Omzetten naar conjunctieve normaalvorm

Het volgende overzicht geeft voor elk connectief de bijbehorende formule in conjunctieve normaalvorm:

Formule	Conjunctieve normaalvorm
$p\equiv \neg q$	$(p\vee q)\wedge (\neg p\vee \neg q)$ Toelichting: $p\equiv \neg q$ $(p\rightarrow \neg q)\wedge (\neg q\rightarrow p)$ $(\neg p\vee \neg q)\wedge (q\vee p)$ $(p\vee q)\wedge (\neg p\vee \neg q)$
$p\equiv q\wedge r$	$(\neg p\vee q)\wedge (\neg p\vee r)\wedge (p\vee \neg q\vee \neg r)$ Toelichting: $p\equiv q\wedge r$ $(p\rightarrow (q\wedge r))\wedge ((q\wedge r)\rightarrow p)$ $(\neg p\vee (q\wedge r))\wedge (\neg (q\wedge r)\vee p)$ $(\neg p\vee (q\wedge r))\wedge (\neg q\vee \neg r\vee p)$ $(\neg p\vee q)\wedge (\neg p\vee r)\wedge (p\vee \neg q\vee \neg r)$
$p\equiv q\vee r$	$(p\vee \neg q)\wedge (p\vee \neg r)\wedge (\neg p\vee q\vee r)$ Toelichting: $p\equiv q\vee r$ $(p\rightarrow (q\vee r))\wedge ((q\vee r)\rightarrow p)$ $(\neg p\vee q\vee r)\wedge (\neg (q\vee r)\vee p)$ $(\neg p\vee q\vee r)\wedge ((\neg q\wedge \neg r)\vee p)$ $(\neg p\vee q\vee r)\wedge (\neg q\vee p)\wedge (\neg r\vee p)$
$p\equiv q\rightarrow r$	$(p\vee q)\wedge (p\vee \neg r)\wedge (\neg p\vee \neg q\vee r)$ Toelichting: $p\equiv q\rightarrow r$ $(p\rightarrow (q\rightarrow r))\wedge ((q\rightarrow r)\rightarrow p)$ $(p\rightarrow (\neg q\vee r))\wedge ((\neg q\vee r)\rightarrow p)$ $(\neg p\vee (\neg q\vee r))\wedge (\neg (\neg q\vee r)\vee p)$ $(\neg p\vee \neg q\vee r)\wedge ((q\wedge \neg r)\vee p)$ $(\neg p\vee \neg q\vee r)\wedge (q\vee p)\wedge (\neg r\vee p)$ $(p\vee q)\wedge (p\vee \neg r)\wedge (\neg p\vee \neg q\vee r)$

Optimalisatie

Er kunnen enkele optimalisaties uitgevoerd worden als subformules meerdere keren voorkomen, zoals bij $(p\rightarrow q)\wedge (p\rightarrow q)$. De CNF-clausulen die behoren bij de tweede subformule $p\rightarrow q$ kunnen weggelaten worden door de variabele die toegekend is aan de eerste subformule te hergebruiken. Uitgewerkt wordt dit: $a\wedge (a\equiv b\wedge c)\wedge (b\equiv p\rightarrow q)\wedge (c\equiv p\rightarrow q)$ wat vereenvoudigd kan worden tot $a\wedge (a\equiv b\wedge b)\wedge (b\equiv p\rightarrow q)$. Deze formule kan vervolgens omgezet worden naar conjunctieve normaalvorm.

Voorbeeld

Het berekenen van de Tseitin-transformatie voor $(p\rightarrow (q\wedge r))$ verloopt als volgt:

• Allereerst krijgt elke subformule een eigen naam toegekend, beginnend bij de gehele formule. Het is hierbij alleen nodig om subformules met connectieven een naam te geven aangezien proposities zoals p dezelfde naam kunnen gebruiken:

$a\equiv (p\rightarrow (q\wedge r))$

$b\equiv (q\wedge r)$

• Met behulp van deze namen is het mogelijk de oorspronkelijke formule uit te drukken als:

$a\wedge (a\equiv p\rightarrow b)\wedge (b\equiv (q\wedge r))$

• Elk van de deelformules wordt omgezet naar een subformule in conjunctieve normaalvorm:

$a\wedge ((p\vee a)\wedge (a\vee \neg b)\wedge (\neg p\vee \neg a\vee b))\wedge ((b\vee \neg q\vee \neg r)\wedge (\neg b\vee q)\wedge (\neg b\vee r))$

of, zonder de haakjes om de subformules:

$a\wedge (p\vee a)\wedge (a\vee \neg b)\wedge (\neg p\vee \neg a\vee b)\wedge (b\vee \neg q\vee \neg r)\wedge (\neg b\vee q)\wedge (\neg b\vee r)$

• De bovenstaande formule is vervulbaarheidsequivalent met de oorspronkelijke formule.

Kenmerken

De Tseitin-transformatie kan in lineaire tijd uitgevoerd worden.

Elke clausule bevat ten hoogste drie literalen en het aantal clausulen is lineair in de grootte van de oorspronkelijke formule.

Wanneer men een formule transformeert naar conjunctieve normaalvorm door logische regels toe te passen, kan men een formule in conjunctieve normaalvorm krijgen met exponentiële grootte in vergelijking met de oorspronkelijke formule. Door nieuwe variabelen te introduceren voorkomt de Tseitin-transformatie dit maar de verkregen formule in conjunctieve normaalvorm is niet langer logisch equivalent maar alleen vervulbaarheidsequivalent.

Bronnen, noten en/of referenties

---

• G.S. Tseitin - On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, Part 2, pagina's 115 - 125, 1968