import { JavaObject } from '../../../java/lang/JavaObject';
export declare abstract class SatSolverA extends JavaObject {
    static readonly RESULT_UNSATISFIABLE: number;
    static readonly RESULT_UNKNOWN: number;
    static readonly RESULT_SATISFIABLE: number;
    constructor();
    /**
     * Erzeugte eine neue Variable. Den zurückgegebenen Integer-Wert darf man nun in Klauseln (auch negiert)
     * benutzen. Eine Variable hat niemals den Wert 0, da dieser Wert nicht negiert werden kann.
     *
     * @return Die Nummer der neuen Variablen.
     */
    abstract createNewVar(): number;
    /**
     * Hinzufügen einer Klausel. Eine Klausel ist eine Menge von Variablen, die mit einem logischen ODER verknüpft
     * sind. Die Variablen dürfen negiert sein.<br>
     * {@code Beispiel: [-3, 8, 2] bedeutet (NOT x3) OR x8 OR x2}<br>
     * Die Menge aller Klauseln sind mit einem AND verknüpft.
     *
     * @param pVars Die Variablen (auch negiert) der Klausel mit den zuvor generierten Variablen. Ist das Array
     *              leer, wird es ignoriert.
     */
    abstract addClause(pVars: Array<number>): void;
    /**
     * Gibt den Wert TRUE oder FALSE der angefragten Variable zurück. Das Verhalten dieser Methode ergibt nur dann
     * Sinn, wenn der Solver mit SATISFIABLE nach Aufruf der Methode {@link #solve } geantwortet hat.
     *
     * @param pVar Die angefragte Variable (kann auch negativ sein, aber nicht 0).
     * @return TRUE, falls die angefragte Variable nach der Berechnnung TRUE ist.
     */
    abstract isVarTrue(pVar: number): boolean;
    /**
     * Startet die Berechnung für maximal {@code maxTimeMillis} Millisekunden und liefert einen der drei möglichen
     * Werte {@link #RESULT_SATISFIABLE}, {@link #RESULT_UNKNOWN} oder {@link #RESULT_UNSATISFIABLE}.
     *
     * @param maxTimeMillis Die maximale Berechnungszeit (in Millisekunden).
     *
     * @return Liefert einen der drei möglichen Werte {@link #RESULT_SATISFIABLE}, {@link #RESULT_UNKNOWN} oder
     *         {@link #RESULT_UNSATISFIABLE}.
     */
    abstract solve(maxTimeMillis: number): number;
    /**
     * Liefert die interne Anzahl an erzeugten Variablen.
     *
     * @return Die interne Anzahl an erzeugten Variablen.
     */
    abstract getVarCount(): number;
    /**
     * Liefert die interne Anzahl an erzeugten Klauseln.
     *
     * @return Die interne Anzahl an erzeugten Klauseln.
     */
    abstract getClauseCount(): number;
    isTranspiledInstanceOf(name: string): boolean;
}
export declare function cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolverA(obj: unknown): SatSolverA;