LogicSolver mit Greedy-Algorithmus
Implementieren Sie zunächst die Hilfsmethoden satisfies(...). und satisfiable(...),:
- satisfies(short[] assignment, short[] clause) liefert genau dann true zurück wenn die Belegung assignment die Klausel clause erfüllt.
- satisfies(short[] assignment, short[][] formula) liefert genau dann true zurück wenn alle Klauseln der Formel erfüllt sind.
- satisfiable(short[] assignment, short[] clause) liefert genau dann true zurück wenn die Belegung die Klausel bereits erfüllt, oder man durch Setzen einer noch nicht belegten Variablen die Klausel erfüllen könnte.
- satisfiable(short[] assignment, short[][] formula) liefert genau dann true wenn das Klausel-satisfiable() (s.o.) für alle Klauseln true zurückliefert (Achtung: Auch $X_1 \wedge \neg X_1$ wäre somit ggfs. satisfiable).
Diese Hilfsmethoden können später nützlich sein um festzustellen ob Ihr Algorithmus bereits eine (Teil-)lösung gefunden hat (satisfies()) oder ob man abbrechen kann, weil keine Lösung mehr erzielt werden kann (!satisfiable()).
Implementieren Sie dann die Methode solveGreedy(), die (gegeben eine aussagenlogische Formel) eine Belegung findet, die die Formel wahr macht.
- Verwenden Sie ein einfaches Greedy-Verfahren, das die Klauseln von oben nach unten durchläuft. Für jede Klausel (soweit diese noch nicht erfüllt ist) gehen Sie die Variablen von links nach rechts durch und belegen die erstbeste Variable, so dass die Klausel erfüllt wird.
- Falls Ihr Verfahren keine Lösung findet, soll die Ergebnis-Belegung ausschließlich Nullen enthalten.
- Ihre Implementierung soll die Eingabe-Formel nicht modifizieren.
package de.hsrm.ads;
public class LogicSolverGreedy {
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;
}
static boolean satisfies(short[] assignment, short[][] formula) {
// FIXME
}
static boolean satisfiable(short[] assignment, short[] clause) {
// FIXME
}
static boolean satisfiable(short[] assignment, short[][] formula) {
// FIXME
}
static short[] solveGreedy(short[][] formula) {
// FIXME
}
}
Subato
