Wie funktioniert Tarjan-Algorithmus für die 2-Sat-Sat

Question

Tarjans Algorithmus für 2 SAT basiert auf der Wahrheit:

Eine 2-CNF-Formel ist erfüllt, wenn und nur, wenn keine Variable vorhanden ist, die zu derselben stark angeschlossenen Komponente wie seine Negation gehört.

Aber ich finde keinen Grund für das Recht auf linke Richtung. Wie kann das Nichtbeachtung dieser Variablen Zufriedenheit der CNF-Zufriedenheit von CNF?

Ich habe versucht, den Schritten des Algorithmus zu folgen, und ich war hier stecken:

Für jede Komponente in der umgekehrten topologischen Reihenfolge, wenn seine Variablen nicht bereits Wahrheitsaufgaben aufweisen, setzen Sie alle Literale in der Komponente, um wahr zu sein. Dies führt dazu auch, dass alle Literatur in der komplementären Komponente auf false eingestellt werden.

Ist es nicht möglich, dass die Variable bereits falsch zugewiesen wird? Wenn wir immer true von hinten zuweisen, weisen wir das FALSE in der Mitte zu, aber der TRUE ist der nächsten Variablen zugewiesen zu werden. In diesem Fall bricht die Machbarkeit ab.

Natürlich passiert diese Art von Fall nie, weil der Algorithmus richtig ist und viele Menschen diesen Algorithmus gut nutzen. Aber so viele Post sagt es als die trivialen Dinge.

.
• Ich denke, der Grund, warum diese Aufgabe möglich ist, ist für den skew-symmetrischen Zustand des Graphen relevant, da (x -> ~ x -> y -> ~ y) niemals wahre Aufträge hat.

Answer 1

Eine 2-CNF-Formel ist faszinierend, wenn und nur, wenn keine Variable vorhanden ist, die zu derselben stark angeschlossenen Komponente als Negation gehört.

Aber ich finde keinen Grund für das Recht auf linke Richtung. Wie kann das Nichtbeachtung dieser Variablen Zufriedenheit der CNF-Zufriedenheit von CNF?

Denken Sie an eine variable Zuordnung für einige unatissierbare 2-Sat-Instanz. Dies bedeutet, dass eine oder mehrere Klauseln unzufrieden bleiben müssen, unabhängig von der Aufgabe. Sie ändern die Einstellung einer oder mehrerer Variablen, um diese Klauseln zu erfüllen, aber dies bleibt unvermeidlich einige neue Klausel oder Klauseln, da die Instanz unbefriedigend ist. Das Versagen Ihrer Änderung, um die Instanz zu erfüllen, bedeutet, dass sich ein anderer Wert einer anderen Variablen ändern muss. Sie wiederholen den Vorgang immer wieder, wodurch andere Variablen als Implikationsanforderungen geändert werden, aber es gelingt niemals, alle Klauseln zu befriedigen. Wenn die Anzahl der Variablen endlich ist, impliziert ein Fehler, dass Sie den Wert einer Variablen ändern, die Sie bereits besucht haben ... und dies ist Ihre kreisförmige Implikation von $ x $ < / span> bis $ \ bar {x} $ Zurück zu $ x $ . Ohne kreisförmige Implikation erreichen Sie schließlich das Ende der Implikationskette und haben eine erfüllende Aufgabe. Der einzige Weg, das Ende der Kette nicht zu erreichen, ist, dass die Kette zwischen einer Variablen und seiner Negation kreisförmig ist.