Erfüllbarkeitsprüfung

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.