Der algorithmische Mechanismus, der iterativ Werte zuweist, die durch Einheitsklauseln in einer aussagenlogischen Klauselmenge impliziert werden, um die Instanz zu vereinfachen und Konflikte zu erkennen; häufig als Boolean Constraint Propagation (BCP) bezeichnet.

Prinzip

Wenn eine Klausel zu einer Einheit wird (nur ein unzugewiesenes Literal), muss dieses Literal wahr gesetzt werden, um die Klausel zu erfüllen; diese Zuweisung wird durch die Klauselmenge propagiert, Klauseln werden vereinfacht und der Vorgang bis zum Fixpunkt oder Konflikt wiederholt.

Demonstration

Bei den Klauseln { {p}, {¬p, q}, {¬q} } propagiert man p=true aus {p}; damit ist {¬p, q} erfüllt und kann entfernt werden, es bleibt {¬q} übrig, das q=false erzwingt; die Reihe der Unit-Propagationen vereinfacht die Instanz und zeigt Konsistenz oder Konflikt auf.

Fehlanwendung

Unit-Propagation auf Formeln anzuwenden, die nicht in Klauselgestalt vorliegen, ohne die eingeführte Struktur zu beachten, oder zu behaupten, die Propagation erhalte andere Eigenschaften wie Quantorenbereich oder theorie-spezifische Einschränkungen.

Konsequenz

Unit-Propagation reduziert schnell den Suchraum, entdeckt Widersprüche früh und bildet die kostengünstige Inferenzgrundlage, die effiziente SAT-Löser und Pruning in DPLL/CDCL-Frameworks ermöglicht.

Umkehrung

Propagation auszulassen und nur Verzweigungen über Variablen vorzunehmen zwingt zu einer kombinatorischen Durchsuchung der Belegungen, die Unit-Propagation sonst beschnitt, und erhöht typischerweise die Suchkosten exponentiell.

Abgrenzung

Definiert für propositionale CNF-Klauselmengen; Erweiterungen auf reichere Theorien erfordern theorie-spezifische Propagation (z. B. Kongruenz, lineare Arithmetik) und müssen sorgfältig implementiert werden, um korrekt zu sein.

Semantische Spannung

Unit-Propagation wird oft mit allgemeiner Constraint-Propagation oder vollständiger boolescher Vereinfachung verwechselt; es ist eine enge, syntaktische, units-getriebene Inferenz, deren Stärke von der Klauselstruktur und Solverdatenstrukturen (watched literals) abhängt.

Synthese

Unit-Propagation ist der deterministische, iterative Prozess des Zuordnens und Propagierens erzwungener Literale aus Einheitsklauseln zur Vereinfachung von Klauseln und Erkennung von Konflikten und bildet das leichte Inferenzgerüst moderner SAT-Verfahren.