ts-api/dist/core/kursblockung/satsolver/SatSolver3.js

"use strict";
Object.defineProperty(exports, "__esModule", { value: true });
exports.cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolver3 = exports.SatSolver3 = void 0;
const AVLSet_1 = require("../../../core/adt/set/AVLSet");
const Variable_1 = require("../../../core/kursblockung/satsolver/Variable");
const SatSolverA_1 = require("../../../core/kursblockung/satsolver/SatSolverA");
const NullPointerException_1 = require("../../../java/lang/NullPointerException");
const LinkedCollection_1 = require("../../../core/adt/collection/LinkedCollection");
const Clause_1 = require("../../../core/kursblockung/satsolver/Clause");
const Arrays_1 = require("../../../java/util/Arrays");
const Heap_1 = require("../../../core/kursblockung/satsolver/Heap");
const System_1 = require("../../../java/lang/System");
class SatSolver3 extends SatSolverA_1.SatSolverA {
    static MAX_LEARNED_CLAUSE_SIZE = 3;
    heap;
    vSize = 0;
    vArrayPos;
    vArrayNeg;
    cSize = 0;
    learnClauseMin = 0;
    /**
     * Konstruktor.
     */
    constructor() {
        super();
        this.heap = new Heap_1.Heap();
        this.vSize = 0;
        this.cSize = 0;
        this.vArrayPos = Array(1).fill(null);
        this.vArrayNeg = Array(1).fill(null);
    }
    isVarTrue(pVar) {
        let v = this.getVarOf(pVar);
        return v.index === -1;
    }
    createNewVar() {
        this.vSize++;
        if (this.vSize >= this.vArrayPos.length) {
            let newSize = this.vSize * 2;
            this.vArrayPos = Arrays_1.Arrays.copyOf(this.vArrayPos, newSize);
            this.vArrayNeg = Arrays_1.Arrays.copyOf(this.vArrayNeg, newSize);
        }
        let vPos = new Variable_1.Variable(+this.vSize);
        let vNeg = new Variable_1.Variable(-this.vSize);
        vPos.negation = vNeg;
        vNeg.negation = vPos;
        this.vArrayPos[this.vSize] = vPos;
        this.vArrayNeg[this.vSize] = vNeg;
        this.heap.insert(vPos);
        this.heap.insert(vNeg);
        return this.vSize;
    }
    addClause(pVars) {
        if (pVars.length === 0) {
            console.log(JSON.stringify("WARNUNG: Leere Klausel bei SatSolver.addClause(int[] pVars)!"));
            return;
        }
        let set = new AVLSet_1.AVLSet();
        for (let v of pVars) {
            if (set.contains(-v)) {
                return;
            }
            set.add(v);
        }
        let list = new LinkedCollection_1.LinkedCollection();
        while (!set.isEmpty()) {
            list.addLast(set.pollFirst());
        }
        while (list.size() > 3) {
            let x = list.removeFirst().valueOf();
            let y = list.removeFirst().valueOf();
            let z = this.createNewVar();
            list.addLast(z);
            this.addClause2(-x, z);
            this.addClause2(-y, z);
            this.addClause3(x, y, -z);
        }
        if (list.size() === 3) {
            this.addClause3(list.removeFirst().valueOf(), list.removeFirst().valueOf(), list.removeFirst().valueOf());
        }
        if (list.size() === 2) {
            this.addClause2(list.removeFirst().valueOf(), list.removeFirst().valueOf());
        }
        if (list.size() === 1) {
            this.addClause1(list.removeFirst().valueOf());
        }
    }
    /**
     * Fügt der Datenstruktur eine 1-CNF-Klausel hinzu.
     *
     * @param x Das 1. Literal (Variablennummer) der Klausel.
     */
    addClause1(x) {
        let varX = this.getVarOf(x);
        if (varX.negation === null)
            throw new NullPointerException_1.NullPointerException();
        this.heap.remove(varX);
        this.heap.remove(varX.negation);
        let c = new Clause_1.Clause(varX);
        this.cSize++;
        varX.clauses.addLast(c);
        varX.statSatFree[c.sat][c.free]++;
        this.heap.insert(varX);
        this.heap.insert(varX.negation);
    }
    /**
     * Fügt der Datenstruktur eine 2-CNF-Klausel hinzu.
     *
     * @param x Das 1. Literal (Variablennummer) der Klausel.
     * @param y Das 2. Literal (Variablennummer) der Klausel.
     */
    addClause2(x, y) {
        let varX = this.getVarOf(x);
        let varY = this.getVarOf(y);
        if ((varX.negation === null) || (varY.negation === null))
            throw new NullPointerException_1.NullPointerException();
        this.heap.remove(varX);
        this.heap.remove(varY);
        this.heap.remove(varX.negation);
        this.heap.remove(varY.negation);
        let c = new Clause_1.Clause(varX, varY);
        this.cSize++;
        varX.clauses.addLast(c);
        varX.statSatFree[c.sat][c.free]++;
        varX.neighbours.addLast(varY);
        varY.clauses.addLast(c);
        varY.statSatFree[c.sat][c.free]++;
        varY.neighbours.addLast(varX);
        this.heap.insert(varX);
        this.heap.insert(varY);
        this.heap.insert(varX.negation);
        this.heap.insert(varY.negation);
    }
    /**
     * Fügt der Datenstruktur eine 3-CNF-Klausel hinzu.
     *
     * @param x Das 1. Literal (Variablennummer) der Klausel.
     * @param y Das 2. Literal (Variablennummer) der Klausel.
     * @param z Das 3. Literal (Variablennummer) der Klausel.
     */
    addClause3(x, y, z) {
        let varX = this.getVarOf(x);
        let varY = this.getVarOf(y);
        let varZ = this.getVarOf(z);
        if ((varX.negation === null) || (varY.negation === null) || (varZ.negation === null))
            throw new NullPointerException_1.NullPointerException();
        this.heap.remove(varX);
        this.heap.remove(varY);
        this.heap.remove(varZ);
        this.heap.remove(varX.negation);
        this.heap.remove(varY.negation);
        this.heap.remove(varZ.negation);
        let c = new Clause_1.Clause(varX, varY, varZ);
        this.cSize++;
        varX.clauses.addLast(c);
        varX.statSatFree[c.sat][c.free]++;
        varX.neighbours.addLast(varY);
        varX.neighbours.addLast(varZ);
        varY.clauses.addLast(c);
        varY.statSatFree[c.sat][c.free]++;
        varY.neighbours.addLast(varX);
        varY.neighbours.addLast(varZ);
        varZ.clauses.addLast(c);
        varZ.statSatFree[c.sat][c.free]++;
        varZ.neighbours.addLast(varX);
        varZ.neighbours.addLast(varY);
        this.heap.insert(varX);
        this.heap.insert(varY);
        this.heap.insert(varZ);
        this.heap.insert(varX.negation);
        this.heap.insert(varY.negation);
        this.heap.insert(varZ.negation);
    }
    getVarCount() {
        return this.vSize;
    }
    getClauseCount() {
        return this.cSize;
    }
    solve(pMaxTimeMillis) {
        let timeStart = System_1.System.currentTimeMillis();
        let backtrackV = Array(this.vSize).fill(null);
        let backtrackLearn = Array(SatSolver3.MAX_LEARNED_CLAUSE_SIZE).fill(null);
        let backtrackB = Array(this.vSize).fill(false);
        let index = 0;
        let max = 1;
        let countDown = 0;
        this.learnClauseMin = SatSolver3.MAX_LEARNED_CLAUSE_SIZE + 1;
        let maxIndex = 0;
        while ((index >= 0) && !this.heap.isEmpty()) {
            if (index > maxIndex) {
                maxIndex = index;
            }
            if (countDown === 0) {
                for (let i = index; i >= 0; i--) {
                    if (backtrackV[i] !== null) {
                        this.unitpropagation_undo((0, Variable_1.cast_de_nrw_schule_svws_core_kursblockung_satsolver_Variable)(backtrackV[i]));
                    }
                    backtrackV[i] = null;
                    backtrackB[i] = false;
                }
                index = 0;
                if ((this.learnClauseMin >= 1) && (this.learnClauseMin <= SatSolver3.MAX_LEARNED_CLAUSE_SIZE)) {
                    let clause = Array(this.learnClauseMin).fill(0);
                    for (let i = 0; i < clause.length; i++) {
                        clause[i] = -backtrackLearn[i].nr;
                    }
                    this.addClause(clause);
                }
                let result = this.simplify();
                if (result !== SatSolverA_1.SatSolverA.RESULT_UNKNOWN) {
                    return result;
                }
                max = max + 1 + Math.trunc(max / 2);
                countDown = max;
                this.learnClauseMin = SatSolver3.MAX_LEARNED_CLAUSE_SIZE + 1;
                if (System_1.System.currentTimeMillis() - timeStart > pMaxTimeMillis) {
                    return SatSolverA_1.SatSolverA.RESULT_UNKNOWN;
                }
                continue;
            }
            countDown--;
            let varP = backtrackV[index];
            if ((varP !== null) && (backtrackB[index])) {
                this.unitpropagation_undo(varP);
                backtrackV[index] = null;
                backtrackB[index] = false;
                this.learnClause(backtrackV, backtrackLearn, index);
                index--;
                continue;
            }
            if (varP === null) {
                varP = this.heap.top();
                if (!varP.isUnsat()) {
                    backtrackV[index] = varP;
                    this.unitpropagation(varP);
                    index++;
                    continue;
                }
            }
            else {
                this.unitpropagation_undo(varP);
            }
            if (varP.negation === null)
                throw new NullPointerException_1.NullPointerException();
            varP = varP.negation;
            if (varP.isUnsat()) {
                backtrackV[index] = null;
                this.learnClause(backtrackV, backtrackLearn, index);
                index--;
                continue;
            }
            backtrackV[index] = varP;
            backtrackB[index] = true;
            this.unitpropagation(varP);
            index++;
            continue;
        }
        return this.heap.isEmpty() ? SatSolverA_1.SatSolverA.RESULT_SATISFIABLE : SatSolverA_1.SatSolverA.RESULT_UNSATISFIABLE;
    }
    learnClause(backtrackV, backtrackLearn, size) {
        if (size < 1) {
            return;
        }
        if (size >= this.learnClauseMin) {
            return;
        }
        this.learnClauseMin = size;
        for (let i = 0; i < size; i++) {
            backtrackLearn[i] = backtrackV[i];
        }
    }
    simplify() {
        let count1 = 0;
        let changed = true;
        while (changed) {
            changed = false;
            for (let nr = 1; nr <= this.vSize; nr++) {
                let varP = this.vArrayPos[nr];
                if (varP.index < 0) {
                    continue;
                }
                if (varP.statSatFree[0][0] > 0) {
                    return SatSolverA_1.SatSolverA.RESULT_UNSATISFIABLE;
                }
                if (varP.negation === null)
                    throw new NullPointerException_1.NullPointerException();
                if (varP.negation.statSatFree[0][0] > 0) {
                    return SatSolverA_1.SatSolverA.RESULT_UNSATISFIABLE;
                }
                if ((varP.statSatFree[0][1] > 0) && (varP.negation.statSatFree[0][1] > 0)) {
                    return SatSolverA_1.SatSolverA.RESULT_UNSATISFIABLE;
                }
                if (varP.statSatFree[0][1] > 0) {
                    this.unitpropagation(varP);
                    count1++;
                    changed = true;
                    continue;
                }
                if (varP.negation.statSatFree[0][1] > 0) {
                    this.unitpropagation(varP.negation);
                    count1++;
                    changed = true;
                    continue;
                }
                if (varP.getClauseOccurences() === 0) {
                    this.unitpropagation(varP.negation);
                    count1++;
                    changed = true;
                    continue;
                }
                if (varP.negation.getClauseOccurences() === 0) {
                    this.unitpropagation(varP);
                    count1++;
                    changed = true;
                    continue;
                }
            }
        }
        return SatSolverA_1.SatSolverA.RESULT_UNKNOWN;
    }
    static fill(index) {
        let s = "";
        for (let i = 0; i < index; i++) {
            s = s.valueOf() + "    ";
        }
        return s;
    }
    /**
     * Setzt die Variable {@code varP} auf TRUE und aktualisiert die gesamte Datenstruktur entsprechend.
     *
     * @param varP Die Variable, die auf TRUE gesetzt wird.
     */
    unitpropagation(varP) {
        let varN = varP.negation;
        if (varN === null)
            throw new NullPointerException_1.NullPointerException();
        this.heap.remove(varP);
        this.heap.remove(varN);
        varP.index = -1;
        varN.index = -2;
        this.unitpropagationHelper(varP.clauses, +1, -1);
        this.unitpropagationHelper(varN.clauses, +0, -1);
    }
    /**
     * Setzt die Variable {@code varP} von TRUE auf FREI und aktualisiert die gesamte Datenstruktur entsprechend.
     *
     * @param varP Die Variable, die von TRUE auf FREI gesetzt wird.
     */
    unitpropagation_undo(varP) {
        let varN = varP.negation;
        if (varN === null)
            throw new NullPointerException_1.NullPointerException();
        this.unitpropagationHelper(varP.clauses, -1, +1);
        this.unitpropagationHelper(varN.clauses, +0, +1);
        this.heap.insert(varP);
        this.heap.insert(varN);
    }
    /**
     * Eine Hilsmethode, die alle Klauseln der Liste aktualisiert.
     *
     * @param clauses    Alle zu informmierenden Klausel.
     * @param pDeltaSat  Die Veränderung der erfüllten Klauseln, relativ zum 1. Index im 2D-Array
     *                   {@link Variable#statSatFree}.
     * @param pDeltaFree Die Veränderung der freien Variablen, relativ zum 2. Index im 2D-Array
     *                   {@link Variable#statSatFree}.
     */
    unitpropagationHelper(clauses, pDeltaSat, pDeltaFree) {
        for (let c of clauses) {
            let sat1 = c.sat;
            let free1 = c.free;
            let sat2 = sat1 + pDeltaSat;
            let free2 = free1 + pDeltaFree;
            for (let v of c.variables) {
                v.statSatFree[sat1][free1]--;
                v.statSatFree[sat2][free2]++;
                this.heap.update(v);
            }
            c.sat = sat2;
            c.free = free2;
        }
    }
    /**
     * Liefert das zugehörige Variablenobjekt.
     *
     * @param pNr Der Variablennummer.
     *
     * @return Das zugehörige Variablenobjekt.
     */
    getVarOf(pNr) {
        return (pNr > 0) ? this.vArrayPos[pNr] : this.vArrayNeg[-pNr];
    }
    isTranspiledInstanceOf(name) {
        return ['de.nrw.schule.svws.core.kursblockung.satsolver.SatSolverA', 'de.nrw.schule.svws.core.kursblockung.satsolver.SatSolver3'].includes(name);
    }
}
exports.SatSolver3 = SatSolver3;
function cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolver3(obj) {
    return obj;
}
exports.cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolver3 = cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolver3;
//# sourceMappingURL=SatSolver3.js.map