123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180 |
- "use strict";
- Object.defineProperty(exports, "__esModule", { value: true });
- exports.cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver = exports.KursblockungAlgorithmusKSatSolver = void 0;
- const SatSolver3_1 = require("../../core/kursblockung/satsolver/SatSolver3");
- const HashMap_1 = require("../../java/util/HashMap");
- const SatSolverWrapper_1 = require("../../core/kursblockung/satsolver/SatSolverWrapper");
- const LinkedCollection_1 = require("../../core/adt/collection/LinkedCollection");
- const System_1 = require("../../java/lang/System");
- const SatSolverA_1 = require("../../core/kursblockung/satsolver/SatSolverA");
- const NullPointerException_1 = require("../../java/lang/NullPointerException");
- const KursblockungAlgorithmusK_1 = require("../../core/kursblockung/KursblockungAlgorithmusK");
- class KursblockungAlgorithmusKSatSolver extends KursblockungAlgorithmusK_1.KursblockungAlgorithmusK {
- kurseAlle;
- schuelerAlle;
- maxNichtWaehler = 0;
- /**
- * Im Konstruktor kann die Klasse die jeweiligen Datenstrukturen aufbauen. Kurse
- * dürfen in diese Methode noch nicht auf Schienen verteilt werden.
- *
- * @param logger Logger für Benutzerhinweise, Warnungen und Fehler.
- * @param dynDat Die dynamischen Blockungsdaten.
- */
- constructor(logger, dynDat) {
- super(logger, dynDat);
- this.kurseAlle = dynDat.gibKurseAlle();
- this.schuelerAlle = this.dynDaten.gibSchuelerArray(false);
- this.maxNichtWaehler = 10;
- }
- berechne(pMaxTimeMillis) {
- if (this.dynDaten.gibKurseDieFreiSindAnzahl() === 0) {
- return;
- }
- let timeStart = System_1.System.currentTimeMillis();
- this.dynDaten.aktionSchuelerAusAllenKursenEntfernen();
- this.dynDaten.aktionKurseFreieZufaelligVerteilen();
- this.dynDaten.aktionZustandSpeichernK();
- let difNichtWaehler = 1;
- while (System_1.System.currentTimeMillis() - timeStart < pMaxTimeMillis) {
- let result = this.berechneSchritt(pMaxTimeMillis);
- if (result === SatSolverA_1.SatSolverA.RESULT_UNKNOWN) {
- return;
- }
- if (result === SatSolverA_1.SatSolverA.RESULT_SATISFIABLE) {
- this.maxNichtWaehler = Math.max(this.maxNichtWaehler - difNichtWaehler, 0);
- continue;
- }
- this.maxNichtWaehler++;
- difNichtWaehler = 0;
- }
- }
- /**
- * Erzeugt eine Formel in konjuntiver Normalform (CNF) und übergibt sie dem
- * SAT-Solver. Der Solver versucht die Formel innerhalb des Zeitlimits zu lösen.
- * Falls er es nicht schafft, dann wurde zuvor eine zufällige Kursverteilung
- * definiert. #
- *
- * @param pMaxTimeMillis Die maximale Blockungszeit in Millisekunde.
- *
- * @return Liefert eines der drei möglichen Ergebnisse
- * {@link SatSolverA#RESULT_SATISFIABLE oder SatSolverI#RESULT_UNKNOWN
- * oder SatSolverI#RESULT_UNSATISFIABLE. }
- */
- berechneSchritt(pMaxTimeMillis) {
- let ssw = new SatSolverWrapper_1.SatSolverWrapper(new SatSolver3_1.SatSolver3());
- let nSchienen = this.dynDaten.gibSchienenAnzahl();
- let mapKursSchiene = new HashMap_1.HashMap();
- for (let kurs of this.kurseAlle) {
- let schienen = Array(nSchienen).fill(0);
- for (let s = 0; s < nSchienen; s++) {
- schienen[s] = kurs.gibIstSchieneFixiert(s) ? ssw.getVarTRUE() : kurs.gibIstSchieneGesperrt(s) ? ssw.getVarFALSE() : ssw.createNewVar();
- }
- mapKursSchiene.put(kurs, schienen);
- }
- let mapSchuelerFachartNichtwahl = new HashMap_1.HashMap();
- let mapSchuelerIstInKurs = new HashMap_1.HashMap();
- let listNichtwahlen = new LinkedCollection_1.LinkedCollection();
- for (let schueler of this.schuelerAlle) {
- mapSchuelerFachartNichtwahl.put(schueler, new HashMap_1.HashMap());
- mapSchuelerIstInKurs.put(schueler, new HashMap_1.HashMap());
- for (let fachart of schueler.gibFacharten()) {
- let varNichtwahlen = ssw.createNewVar();
- let mapFachartNichtwahl = mapSchuelerFachartNichtwahl.get(schueler);
- if (mapFachartNichtwahl === null)
- throw new NullPointerException_1.NullPointerException();
- mapFachartNichtwahl.put(fachart, varNichtwahlen);
- listNichtwahlen.add(varNichtwahlen);
- for (let kurs of fachart.gibKurse()) {
- let varKurs = ssw.createNewVar();
- let mapIstInKurs = mapSchuelerIstInKurs.get(schueler);
- if (mapIstInKurs === null)
- throw new NullPointerException_1.NullPointerException();
- mapIstInKurs.put(kurs, varKurs);
- }
- }
- }
- for (let kurs of this.kurseAlle) {
- let list = new LinkedCollection_1.LinkedCollection();
- let schienen = mapKursSchiene.get(kurs);
- if (schienen === null)
- throw new NullPointerException_1.NullPointerException();
- for (let s = 0; s < nSchienen; s++) {
- list.add(schienen[s]);
- }
- let amount = kurs.gibSchienenAnzahl();
- ssw.c_exactly_GENERIC(list, amount);
- }
- for (let schueler of this.schuelerAlle) {
- for (let fachart of schueler.gibFacharten()) {
- let list = new LinkedCollection_1.LinkedCollection();
- for (let kurs of fachart.gibKurse()) {
- let mapIstInKurs = mapSchuelerIstInKurs.get(schueler);
- if (mapIstInKurs === null)
- throw new NullPointerException_1.NullPointerException();
- let varKurs = mapIstInKurs.get(kurs);
- if (varKurs === null)
- throw new NullPointerException_1.NullPointerException();
- list.add(varKurs);
- }
- ssw.c_exactly_GENERIC(list, 1);
- }
- }
- for (let schueler of this.schuelerAlle) {
- let mapIstInKurs = mapSchuelerIstInKurs.get(schueler);
- if (mapIstInKurs === null)
- throw new NullPointerException_1.NullPointerException();
- for (let fachart1 of schueler.gibFacharten()) {
- for (let fachart2 of schueler.gibFacharten()) {
- if (fachart1.gibNr() < fachart2.gibNr()) {
- for (let kurs1 of fachart1.gibKurse()) {
- for (let kurs2 of fachart2.gibKurse()) {
- let var1 = mapIstInKurs.get(kurs1);
- let var2 = mapIstInKurs.get(kurs2);
- if ((var1 === null) || (var2 === null))
- throw new NullPointerException_1.NullPointerException();
- let x = ssw.c_new_var_AND(var1.valueOf(), var2.valueOf());
- for (let s = 0; s < nSchienen; s++) {
- let schienenKurs1 = mapKursSchiene.get(kurs1);
- let schienenKurs2 = mapKursSchiene.get(kurs2);
- if ((schienenKurs1 === null) || (schienenKurs2 === null))
- throw new NullPointerException_1.NullPointerException();
- let var3 = schienenKurs1[s];
- let var4 = schienenKurs2[s];
- ssw.c_3(-x, -var3, -var4);
- }
- }
- }
- }
- }
- }
- }
- console.log(JSON.stringify("V=" + ssw.getVarCount() + ", C=" + ssw.getClauseCount()));
- let satresult = ssw.solve(pMaxTimeMillis);
- if (satresult !== SatSolverA_1.SatSolverA.RESULT_SATISFIABLE) {
- return satresult;
- }
- this.dynDaten.aktionSchuelerAusAllenKursenEntfernen();
- for (let kurs of this.kurseAlle) {
- let schienen = new LinkedCollection_1.LinkedCollection();
- for (let s = 0; s < nSchienen; s++) {
- let schienenKurs = mapKursSchiene.get(kurs);
- if (schienenKurs === null)
- throw new NullPointerException_1.NullPointerException();
- if (ssw.isVarTrue(schienenKurs[s])) {
- schienen.add(s);
- }
- }
- kurs.aktionVerteileAufSchienen(schienen);
- }
- return satresult;
- }
- isTranspiledInstanceOf(name) {
- return ['de.nrw.schule.svws.core.kursblockung.KursblockungAlgorithmusKSatSolver', 'de.nrw.schule.svws.core.kursblockung.KursblockungAlgorithmusK'].includes(name);
- }
- }
- exports.KursblockungAlgorithmusKSatSolver = KursblockungAlgorithmusKSatSolver;
- function cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver(obj) {
- return obj;
- }
- exports.cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver = cast_de_nrw_schule_svws_core_kursblockung_KursblockungAlgorithmusKSatSolver;
- //# sourceMappingURL=KursblockungAlgorithmusKSatSolver.js.map
|