Variablenmuster.

Der Sinn der so genannten Variablenmuster ist es, die Konsistenz zwischen den Variablenbelegungen der einzelnen Klauseln zu erzwingen. Dies wird mit einem Variablenmuster erreicht, wie es Abbildung A.6 zeigt. Das Muster einer Variablen besteht aus zwei Schächten mit einer Ecke oben rechts, die mit $F$ beziehungsweise $T$ bezeichnet ist. Zusätzlich hat jeder Schacht $s$ Spitzen, wobei $s$ die Anzahl der Klauseln ist, in denen die Variable vorhanden ist. Einer der beiden Punkte $F$ oder $T$ muss einen Wachposten besitzen, um die Ecke bei $q$ einsehen zu können. Falls allen Variablen konsistente Wahrheitswerte zugewiesen wurden, sind keine weiteren Wachposten nötig, um das Variablenmuster einzusehen. Eine vollständige Konstruktion verdeutlicht diesen Sachverhalt.

Abbildung A.6: Das Variablenmuster. Zwei Schächte mit zwei Spitzen. Der Punkt $q$ kann von $T$ oder $F$ gesehen werden.