Reduktion zu Aussagenlogik (II)

Satz (Bryant und Velev, CAV-12, LNCS 1855, 2000):

es genügt, Transitivitäts-Constraints für sehnenlose Kreise hinzuzufügen.

Satz (Graphentheorie/Folklore):

zu jedem Graphen G mathend000# kann man in Polynomialzeit einen chordalen Obergraphen G' mathend000# konstruieren (durch Hinzufügen von Kanten).

Graph G mathend000# heißt chordal, wenn er keinen sehnenlosen Kreis einer Länge ≥4 mathend000# enthält.

Vorsicht: chordal ≠ mathend000# trianguliert, Beispiel.

Algorithmus: wiederholt: einen Knoten entfernen,
dessen Nachbarn zu Clique vervollständigen.