Motivation des Algorithmus: Der Algorithmus markiert alle Variablen, die zwangsläufigerweise mit wahr belegt werden müssen (nämlich zuerst die Variablen in den Klauseln, die nur aus einem positiven Literal bestehen, und danach in den Klauseln, die eine Implikation darstellen und bei denen die Variablen auf der linken Seite der Implikation schon...