Dieses Übungsblatt ist Ihre erste bewertete Abgabe. Bis zu 12 Punkte sind zu erreichen. Beachten Sie die Hinweise im Einführungsvideo. Weitere Hinweise:
Beachten Sie außerdem noch einmal folgende Hinweise:
Wir entwickeln in diesem Übungsblatt verschiedene Programme, die - gegeben eine aussagenlogische Formel - eine Belegung der booleschen Variablen (z.B. X1,X2,X3,X4) finden, so dass die Formel wahr wird. Die zu lösende Formel sei in konjunktiver Normalform (KNF) gegeben, z.B. so:
Eine Formel in KNF wird wahr, wenn alle ihre Klauseln wahr werden. Eine Klausel wird wahr, wenn mindestens eines ihrer Literale wahr wird.
Unser Ziel ist es, eine Belegung der Variablen (hier, X1,...,X4) zu finden, so dass die Formel wahr wird. Im Beispiel wäre eine Lösung z.B. X1=X2=X3=X4=TRUE. Wir repräsentieren eine (Teil-)Belegung der N Variablen einer Formel als ein N-elementiges Array, das jeder Variablen den Wert 1 (=TRUE), -1 (=FALSE) oder 0 (= NOCH NICHT BELEGT) zuweist. Im folgenden Beispiel wäre X1 = X2 = TRUE, X3 = FALSE, und X4 noch nicht belegt.
short[] assignment = new short[] { 1, 1, -1, 0};
Es sei K die Anzahl der Klauseln in der Formel (im obigen Beispiel 3) und N die Anzahl der Variablen (im obigen Beispiel 4). Wir repräsentieren eine Formel als ein zweidimensionales (K,N)-elementiges Array. Jede Zeile entspricht einer Klausel. Der Wert an Stelle (k,n) gibt an, ob Variable n in Klausel k positiv vorkommt (=1), negiert vorkommt (=-1) oder garnicht vorkommt (=0). Beispiel für die obige Formel:
short[][] formula = new short[][] {
{ 1, -1, 0, 0 }, // Klausel 1: X1 v -X2
{ 0, 1, -1, 0 }, // Klausel 2: -X3 v X2
{ 0, 0, 0, 1 } // Klausel 3: X4
};