Erfüllbarkeitsproblem für Schaltkreise
In der theoretischen Informatik (insbesondere in der Komplexitätstheorie) ist das Erfüllbarkeitsproblem für Schaltkreise (Vorlage:EnS, CircuitSAT, CSAT) das Entscheidungsproblem, ob es für eine gegebene boolesche Schaltung eine Eingabe gibt, die den Ausgang wahr macht.
Problemstellung
Betrachtet wird ein boolescher Schaltkreis, der aus binären Und-Gattern, binären Oder-Gattern, unären Nicht-Gattern, Input-Gattern und einem Output-Gatter besteht. Zu entscheiden ist, ob eine Eingabe (d. h. eine Zuordnung von Wahrheitswerten zu den Input-Gattern) existiert, für die das Output-Gatter wahr wird.
Die Auswahl der erlaubten Gatter im booleschen Schaltkreis variiert in der Literatur. Die Wahl von Und-, Oder- und Nicht-Gattern erlaubt es, alle Booleschen Funktionen mit Schaltkreisen zu bilden. Andere Varianten erlauben zum Beispiel zusätzlich Gatter für die beiden Wahrheitswerte oder verwenden NAND-Gatter anstatt der Und-, Oder- und Nicht-Gatter.
Komplexität
Das Erfüllbarkeitsproblem für Schaltkreise ist NP-vollständig. Es gilt als prototypisches NP-vollständiges Problem und wird in manchen Lehrbüchern als erstes NP-vollständiges Problem eingeführt. Es kann verwendet werden, um die NP-Schwere anderer Probleme mittels Reduktion zu beweisen. Insbesondere gibt es eine relativ einfache Reduktion auf das Erfüllbarkeitsproblem der Aussagenlogik (SAT), und CircuitSAT kann daher benutzt werden, um die NP-Schwere von SAT zu zeigen (Satz von Cook).
Die Größe eines Schaltkreises ist die Anzahl der Gatter des Schaltkreises, wobei Input-Gatter nicht mitgezählt werden. Für einen Schaltkreis mit Input-Gattern kann CircuitSAT in entschieden werden. Hierzu kann man für jede der möglichen Eingaben in Polynomialzeit testen, ob das Output-Gatter wahr wird (siehe Circuit Value Problem).
In Abhängigkeit von der Schaltkreisgröße kann das Problem in entschieden werden. Diese Schranke hält für Schaltkreise mit beliebigen binären Gattern.[1]