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

import { SatSolverA } from '../../../core/kursblockung/satsolver/SatSolverA';
export declare class SatSolver3 extends SatSolverA {
    private static readonly MAX_LEARNED_CLAUSE_SIZE;
    private heap;
    private vSize;
    private vArrayPos;
    private vArrayNeg;
    private cSize;
    private learnClauseMin;
    /**
     * Konstruktor.
     */
    constructor();
    isVarTrue(pVar: number): boolean;
    createNewVar(): number;
    addClause(pVars: Array<number>): void;
    /**
     * Fügt der Datenstruktur eine 1-CNF-Klausel hinzu.
     *
     * @param x Das 1. Literal (Variablennummer) der Klausel.
     */
    private addClause1;
    /**
     * 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.
     */
    private addClause2;
    /**
     * 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.
     */
    private addClause3;
    getVarCount(): number;
    getClauseCount(): number;
    solve(pMaxTimeMillis: number): number;
    private learnClause;
    private simplify;
    private static fill;
    /**
     * Setzt die Variable {@code varP} auf TRUE und aktualisiert die gesamte Datenstruktur entsprechend.
     *
     * @param varP Die Variable, die auf TRUE gesetzt wird.
     */
    private unitpropagation;
    /**
     * 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.
     */
    private unitpropagation_undo;
    /**
     * 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}.
     */
    private unitpropagationHelper;
    /**
     * Liefert das zugehörige Variablenobjekt.
     *
     * @param pNr Der Variablennummer.
     *
     * @return Das zugehörige Variablenobjekt.
     */
    private getVarOf;
    isTranspiledInstanceOf(name: string): boolean;
}
export declare function cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolver3(obj: unknown): SatSolver3;