Subato

(Algorithmen und Datenstrukturen SS 2021)

Exercise Sheet 7

Abgabe 1: Aussagenlogik

Due Date: 2021-05-30 23:59:00.0

Organisatorische Hinweise

Dieses Übungsblatt ist Ihre erste bewertete Abgabe. Bis zu 12 Punkte sind zu erreichen. Beachten Sie die Hinweise im Einführungsvideo. Weitere Hinweise:

  • Spätester Abgabetermin ist Sonntag, der 30.05., um 23:59 Uhr.
  • In den Praktika (24.05.-28.05.) werden die Aufgaben besprochen und Sie können Verständnisfragen stellen.
  • Jedes Team lädt seine Abgabe in Subato hoch und schickt vor der Deadline eine Info-Mail an die folgenden Adressen (es reicht eine Mail je Team):
  • Diese Mail enthält:
    • die Namen sämtlicher Team-Mitglieder
    • die Praktikumsgruppe in der Sie teilnehmen
    • den Subato-Account, unter dem Ihre Abgabe hochgeladen wurde (es reicht ein Account).
  • Bei Nicht-Einhaltung dieser Formalien behalten wir uns Punktabzüge vor.

Beachten Sie außerdem noch einmal folgende Hinweise:

  • Verwenden Sie bei den Programmieraufgaben generell nur Grundtypen und Felder. Andere Datenstrukturen (ArrayList o.ä.) sind nicht erlaubt.
  • Finden Sie sich zu Zweier-Teams zusammen. Ein Dreier-Team pro Praktikumsgruppe ist in Abstimmung mit der/dem Praktikumeleiter(in) erlaubt. Einzelabgaben werden nicht akzeptiert. Falls Sie noch keine Partnerin / keinen Partner haben, verweise ich auf Praktika und Foren. 
  • Ihr Team sollte die Aufgaben selbstständig lösen. Es erfolgt eine Plagiatsprüfung. Sollte abgeschrieben werden, droht die Wertung der Studienleistung als "Täuschungsversuch". Auch ein gemeinsames Team-übergreifendes Erarbeiten der Lösung und anschließendes Abgeben der (quasi-)identischer Lösungen wird als Plagiat gewertet.

Einführung

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
};
Hinweis: Sie können generell annehmen, dass eine Formel mindestens eine Klausel und mindestens eine Variable besitzt.
 

 

  • Exercise 1 LogicSolverGreedy
    LogicSolverGreedy
  • Exercise 2 LogicSolverDivideAndConquer
    LogicSolverDivideAndConquer
  • Exercise 3 LogicSolverBacktracking
    LogicSolverBacktracking
  • Exercise 4 LogicSolver: Theorie
    Analysieren Sie die Komplexität ihrer Verfahren.