Das Erfüllbarkeitsproblem der Aussagenlogik – auch als SAT-Problem bezeichnet nach dem englischen Begriff satisfiablity für Erfüllbarkeit – fragt nach der Erfüllbarkeit einer gegebenen aussagenlogischen Formel durch eine geeignete Variablenbelegung. Man kann das Problem natürlich durch Aufstellen einer Wahrheitstabelle lösen, aber dann wächst der Zeitverbrauch exponentiell mit der Anzahl der Variablen. Man weiß bis heute nicht,…