In dieser Arbeit
werden die Grundlagen der Modellgenerierung in propositionalen Logiken und der Constraint Satisfaction vorgestellt. Es wird gezeigt, daß jedes Constraint Satisfaction Problem als Problem der Aussagenlogik ausgedrückt werden kann, wie auch für jede aussagenlogische Formel die Frage der Erfüllbarkeit als Constraint Satisfaction Problem formulierbar ist. Weiter ist zu beobachten, daß das Erfüllbarkeitsproblem der Aussagenlogik als ein binäres Constraint Satisfaction Problem darstellbar ist. In der Folge wird dargestellt, welche Möglichkeiten zur Bearbeitung dieses Problems dadurch eröffnet werden. Es werden die entwickelten Methoden und Algorithmen vorgestellt und verglichen. Dabei wird festgestellt, daß die angewandten Verfahren der Lösungssuche von Erfüllbarkeitsproblmen unter Verwendung semantischer Tableaus ähnlich sind. Durch die gemeinsame Verwendung von Konzepten der Tableau-Bearbeitung und der Constraint Satisfaction wird eine bessere Performance erreicht als mit den bekannten Davis-Putnam-Algorithmen.