Das algorithmische Verfahren, das entscheidet, ob eine gegebene propositionale oder Boolesche Formel mindestens eine Belegung von Wahrheitswerten besitzt, die die Formel wahr macht; üblich für Formeln in konjunktiver Normalform (KNF) und implementiert durch SAT-Solver.

Prinzip

Die Logiksatisfiabilität wird auf eine geführte Suche über Belegungen plus Inferenz und Lernen reduziert: systematisches Durchsuchen partieller Belegungen, Propagation impliziter Werte, Konflikterkennung, Backtracking mit gelernten Klauseln oder Heuristiken und Terminierung, wenn eine vollständige erfüllende Belegung gefunden oder Unlösbarkeit bewiesen ist.

Demonstration

Für KNF-Klauseln (x ∨ y), (¬x ∨ z), (¬y ∨ ¬z) kann ein CDCL-Solver x=true setzen, y=true propagieren, einen Konflikt mit (¬y ∨ ¬z) erzeugen, den Konflikt analysieren und die Klausel (¬x ∨ ¬z) lernen, zurückspringen und dann eine vollständige Belegung wie x=false, y=true, z=false finden, die alle Klauseln erfüllt.

Fehlanwendung

SAT-Solving als Optimierungsroutine zu missverstehen, die notwendigerweise das «beste» Modell liefert, oder anzunehmen, ein Solver würde standardmäßig alle erfüllenden Belegungen aufzählen; oder propositionale SAT-Methoden direkt auf prädikatenlogische Formeln ohne Grounding oder Theorieeinbindung anzuwenden.

Konsequenz

Richtige Anwendung liefert ein Zertifikat: entweder eine konkrete erfüllende Belegung (Modell) oder einen Beweis der Unerfüllbarkeit (z. B. abgeleitete leere Klausel) und ermöglicht automatisierte Verifikation, Gegenbeispielgenerierung und Reduktionen vieler NP-Probleme auf SAT.

Umkehrung

Statt nach einer erfüllenden Belegung zu suchen, ist die invertierte Aufgabe die Extraktion eines unsat-Kerns oder die Modellauszählung; man kann das Verfahren so umkehren, dass minimale unlösbare Teilmengen statt Modelle aufgelistet werden.

Abgrenzung

Geltungsbereich sind propositionale/Boolsche Formeln (endliche boolesche Kombinationen). Ausgeschlossen sind, sofern nicht erweitert, prädikatenlogische Formeln mit Funktionssymbolen und unendlichen Domänen sowie SMT-Instanzen, die zusätzliche Theorien erfordern.

Semantische Spannung

Spannung besteht zwischen reinem SAT und SMT: beide entscheiden Satisfiabilität, aber SMT integriert Theoriebehandlung, sodass Methoden und Garantien differieren; ferner Spannung zwischen Entscheidungsaufgabe (existiert ein Modell?) und Such-/Optimierungsaufgaben (bestes Modell).

Synthese

Erfüllbarkeitsprüfung kombiniert Suche, Propagation, Konfliktanalyse und Heuristiken, um die Entscheidungsfrage für boolesche Formeln zu beantworten: entweder durch Konstruktion einer erfüllenden Belegung oder durch Herleitung von Unerfüllbarkeit für Anwendungen in Verifikation und Synthese.