Es sei ein ungerichteter Graph mit Knoten 1,...,n gegeben. Jedem Paar i<k von Knoten wird eine Variable X_(i,k) zugeordnet, die den Wert 1 genau dann hat, falls es eine Kante zwischen i und k gibt.
Nun soll durch eine aussagenlogische Formel für eine beliebige Formel der Länge n gezeigt werden, dass der Graph einen Hamiltonkreis enthält.
Wie sieht so eine aussagenlogische Formel aus?
