CNF-Formel

Eine CNF-Formel ist eine logische Aussage in einer bestimmten Normalform — das heißt, in einer vorgeschriebenen, einheitlichen Struktur. Sie besteht aus mehreren Gruppen von Bedingungen, die alle gleichzeitig gelten müssen. Innerhalb jeder Gruppe muss mindestens eine Bedingung erfüllt sein. Man verknüpft also Gruppen mit UND und die Inhalte einer Gruppe mit ODER. Eine einzelne Bedingung ist dabei stets eine Variable oder deren Verneinung — zum Beispiel „es regnet“ oder „es regnet nicht“. Das Kürzel CNF steht für den englischen Begriff „conjunctive normal form“, auf Deutsch „konjunktive Normalform“ oder kurz KNF.

CNF als gemeinsame Sprache der Logik-Software

Viele Probleme in Informatik und Mathematik lassen sich als Frage formulieren: Gibt es eine Belegung von Variablen, die eine bestimmte Aussage wahr macht? Solche Fragen heißen Erfüllbarkeitsprobleme. CNF-Formeln sind dafür der Standard, weil ihre Struktur gleichmäßig und vorhersehbar ist. Ein Algorithmus, der CNF versteht, kann damit ein einziges allgemeines Werkzeug für hundert verschiedene Probleme sein.

Dazu kommt ein theoretischer Grund: Jede beliebige logische Aussage lässt sich mechanisch in eine äquivalente CNF-Formel umwandeln. „Äquivalent“ bedeutet hier: Die neue Formel ist genau dann erfüllbar, wenn es die ursprüngliche auch war. Das macht CNF zu einem universellen Zwischenformat — vergleichbar damit, wie man Musik in verschiedenen Formaten speichern kann, aber MP3 das Format ist, das alle Player verstehen.

Aufbau einer CNF-Formel im Detail

Die Grundbausteine heißen Literale. Ein Literal ist entweder eine Variable (z. B. A) oder ihre Verneinung (¬A, gesprochen „nicht A“). Mehrere Literale, die mit ODER verknüpft sind, bilden eine Klausel. Zum Beispiel ist (A ∨ ¬B ∨ C) eine Klausel — sie ist bereits wahr, sobald mindestens eines der drei Literale wahr ist. Eine CNF-Formel ist schließlich eine Kette solcher Klauseln, verbunden mit UND.

Ein konkretes Beispiel: (A ∨ B) ∧ (¬A ∨ C) ∧ (¬B ∨ ¬C). Diese Formel hat drei Klauseln. Sie ist erfüllbar, wenn man Werte für A, B und C findet, sodass jede der drei Klauseln wahr wird. Mit A = wahr, B = falsch, C = wahr klappt das. Ein häufiger Irrtum ist, CNF mit einer einfachen Liste von Bedingungen gleichzusetzen — entscheidend ist die Schachtelung: ODER innerhalb der Klauseln, UND zwischen den Klauseln, nie umgekehrt.

Eine wichtige Sonderform ist 3-CNF: Hier darf jede Klausel genau drei Literale enthalten. Das klingt wie eine Einschränkung, ist aber theoretisch genauso ausdrucksstark wie beliebige CNF. Die Frage, ob eine 3-CNF-Formel erfüllbar ist, heißt 3-SAT und ist eines der bekanntesten Probleme der Informatiktheorie.

CNF in der Praxis: SAT-Solver und KI-Planung

Programme, die prüfen, ob eine CNF-Formel erfüllbar ist, heißen SAT-Solver. Sie werden in der Chipentwicklung eingesetzt, um Schaltkreise auf Fehler zu prüfen, und in der Softwareanalyse, um sicherheitskritischen Code zu verifizieren. Moderne SAT-Solver können Formeln mit Millionen von Klauseln in Sekunden lösen — obwohl das Problem theoretisch zu den schwierigsten überhaupt gehört.

Auch in der KI taucht CNF auf. Planungsalgorithmen — etwa für Roboter oder automatisierte Logistiksysteme — übersetzen Ziele und Regeln in CNF-Formeln und fragen dann einen SAT-Solver, ob eine Lösung existiert. Wer in News über Chipdesign, formale Verifikation oder automatisches Schlussfolgern liest, stößt früher oder später auf dieses Format. CNF ist dabei selten das Thema selbst, aber fast immer das Werkzeug dahinter.