NEUE VERSION: 'Kurs42_To_CNF'

[B. Bartsch]

Meine 1. Frage:
Ich habe die Anzahl der Schienen zunächst auf maximal 10 gesetzt. Es gibt aber eine Fachwahl, die 11 Schienen benötigt. Das Programm rechnet eifrig weiter, eine Lösung gibt es aber offensichtlich nicht. Gibt es keine scharfe Abbruchbedingung mehr wie bei dem alten Programm, wenn das Problem unlösbar ist?

Für das Programm ist das leider nicht so offensichtlich. Das probiert fleißig herum - obwohl es für uns Menschen sofort klar ist. Das liegt daran, dass das Programm alles in ganz kleine "atomare" Gleichungen (Klauseln) kodiert, das hat Vorteile, aber auch Nachteile. SAT-Solver haben generell ein Problem mit dem sogenannten "pigeon hole" - Prinzip (n Elemente ohne Dopplung auf n+1 Plätze verteilen).

[M. Plümper]

Evtl. wäre es daher sinnvoll dem SAT-Solver eine Vorabprüfung vorzuschalten, die bestimmte Kriterien ohne Gleichungen prüft.

[B. Bartsch]

Evtl. wäre es daher sinnvoll dem SAT-Solver eine Vorabprüfung vorzuschalten, die bestimmte Kriterien ohne Gleichungen prüft.

Ja, könnte man, aber ich mache das lieber nicht, es könnte fälschlicherweise Sachen verhindern wie: Nur eine Person mit 11 Wahlen und der Benutzer erlaubt 1 Umwahl, dann ist das Problem wieder lösbar.

[M. Plümper]

Hallo Herr Bartsch,

mit einer solchen Vorabprüfung meinte ich nicht, dass man die Blockung zum Lösen nicht an den Solver schickt. Vielmehr hatte ich an einen Hinweis an den User gedacht. Bspw: "Die Anzahl der Schienen ist für die Fachwahlen zu gering. Eine Blockung ohne Umwähler ist nicht möglich. Fortfahren?"

[B. Bartsch]

Vielmehr hatte ich an einen Hinweis an den User gedacht.

Finde ich gut ... anbei die neue Version.

- Neu: Visuelle Warnung wenn "Schienenanzahl < max. Fachwahlen".

[M. Plümper]

Das ging aber schnell. Danke.

[D.Jakel]

Die Qualtität der Lösungen ist im Vergleich zur Kurs42-Routine wirklich beeindruckend und die Lösung rasend schnell gefunden, sagenhaft!

[B. Bartsch]

Die Qualtität der Lösungen ist im Vergleich zur Kurs42-Routine wirklich beeindruckend und die Lösung rasend schnell gefunden, sagenhaft!

Das freut mich. Aus Interesse, könnten Sie das konkretisieren.

Schienenanzahl, Stufe, SchülerInnen in der Stufe, Umwähler vorher/nachher, Kursdifferenz vorher/nachher. Haben Sie von vorne rechnen lassen, oder haben Sie die "100%, 90%, 80%, ..." Buttons benutzt um eine vorhandene Lösung weiter zu optimieren?

[M. Plümper]

Hallo Herr Bartsch,

Eine Nachfrage: Werden die GK Werte (Umwähler und Differenz) auch auf die ZK angewendet? Zumindest habe ich den Eindruck.

Die Situation ist nämlich, dass durch Abwahlen zur Q2 bei den bestehenden GKs durchaus Differenzen von z. B. 8 SuS entstehen können. Wenn nun zum Einblockungen der ZKs alle Kurse und Teilnehmer bis auf die ZKs fixieren werden und man dann die Größendifferenz der GKs auf einen Wert unterhalb der aktuellen GK Differenzen setzt, gibt es sehr schnell ein UNSAT zurück (was logisch ist).

Damit erhält man aber unter Umständen keine optimierten ZKs zurück, sprich, auch wenn dort eine Differenz von 3 möglich wäre, wird vom Solver im obigen Beispiel auch 8 akzeptiert.

Oder kann man über Regeln hier eine Optimierung der ZKs erreichen?

[B. Bartsch]

Eine Nachfrage: Werden die GK Werte (Umwähler und Differenz) auch auf die ZK angewendet? Zumindest habe ich den Eindruck.

GK = Alles außer LK

Oder kann man über Regeln hier eine Optimierung der ZKs erreichen?

Sie können einer FachArt eine individuelle Kursdifferenz geben, dann wird die globale GK-Kursdifferenz ignoriert bzw. für diese Fachart überschrieben.