Als nächstes lösen wir Formeln mit Divide and Conquer. Die Strategie ist unten angebildet: Wir halbieren die Formel rekursiv, bis wir einzelne Klauseln erreichen. Für jede Klausel ermitteln wir die Menge der Belegungen die die Klausel erfüllen. Diese Belegungen werden kombiniert indem wir jeweils die Schnittmenge bilden, solange bis nur die Belegungen übrig bleiben die alle Klauseln erfüllen und somit die Formel lösen:
- Implementieren Sie zunächst die Hilfsmethode solutionsForClause(). Diese soll - gegeben eine Klausel - sämtliche Belegungen zurückgeben die die Klausel erfüllen. Das Ergebnis ist dementsprechend ein short[][]: ein Array, das mehrere Belegungen enthält. Jede dieser Belegungen ist wieder ein Array bestehend aus -1 und 1.
- Tipp: Eine gute Strategie hierfür ist es, die Zahlen von $0$ bis $2^n-1$ (bei $n$ Variablen) hochzuzählen, und die Bits jeder Zahl als Belegung zu interpretieren. Von den resultierenden Belegungen speichern Sie nur jene, die die Klausel erfüllen.
- Implementieren Sie dann solveDivideAndConquer() - als Inspiration kann der Code für Mergesort dienen. Das Gesamtergebnis Ihres Verfahrens ist eine Menge von Belegungen (short[][]), nicht wie bei Greedy eine einzige Belegung (short[]).
- Falls Ihr Verfahren keine Lösung findet, soll ein leeres Array (new short[][] {}) zurückgegeben werden.
- Wie immer ist es erlaubt, Hilfsmethoden hinzuzufügen.
- Tipp: Mit Arrays.equals() lässt sich prüfen ob Arrays vom Typ short[] identisch sind.
- Ihre Implementierung soll die Eingabe-Formel nicht modifizieren.
package de.hsrm.ads;
import java.util.Arrays;
public class LogicSolverDivideAndConquer {
static boolean satisfies(short[] assignment, short[] clause) {
for (int i=0; i<clause.length; ++i)
if(assignment[i]*clause[i]==1)
return true;
return false;
}
// Bei Bedarf können Sie hierhin andere
// satisfies() / satisfiable() - Methoden
// aus LogicSolverGreedy kopieren.
static short[][] solutionsForClause(short[] clause) {
// FIXME
}
static short[][] solveDivideAndConquer(short[][] formula) {
// FIXME
}
}
Subato
