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 kann man in Polynomialzeit einen chordalen Obergraphen G' konstruieren (durch Hinzufügen von Kanten).

Graph G heißt chordal, wenn er keinen sehnenlosen Kreis einer Länge $\ge$4 enthält.

Vorsicht: chordal $\neq$ trianguliert, Beispiel.

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