import { SatSolverA } from '../../../core/kursblockung/satsolver/SatSolverA';
import { LinkedCollection } from '../../../core/adt/collection/LinkedCollection';
export declare class SatSolverWrapper extends SatSolverA {
    private readonly _solver;
    private readonly varFALSE;
    private readonly varTRUE;
    /**
     * Erstellt eine Ebene über dem {@link SatSolverA}, um verschiedene Bedingungen/Constraints als Klauseln zu
     * codieren.
     *
     * @param solver Der Solver, der intern verwendet wird.
     */
    constructor(solver: SatSolverA);
    createNewVar(): number;
    addClause(pVars: Array<number>): void;
    isVarTrue(pVar: number): boolean;
    solve(maxTimeMillis: number): number;
    getVarCount(): number;
    getClauseCount(): number;
    /**
     * Liefert ein Array der Länge n mit neu erzeugten Variablennummern.
     *
     * @param n Die Länge des Arrays.
     *
     * @return Ein Array der Länge n mit neu erzeugten Variablennummern.
     */
    createNewVars(n: number): Array<number>;
    /**
     * Liefert eine Variable, die zuvor auf FALSE forciert wurde.
     *
     * @return Eine Variable, die zuvor auf FALSE forciert wurde.
     */
    getVarFALSE(): number;
    /**
     * Liefert eine Variable, die zuvor auf TRUE forciert wurde.
     *
     * @return Eine Variable, die zuvor auf TRUE forciert wurde.
     */
    getVarTRUE(): number;
    /**
     * Fügt eine Klausel der Größe 1 hinzu. Forciert damit die übergebene Variable auf TRUE.
     *
     * @param x Die Variable wird auf TRUE gesetzt.
     */
    c_1(x: number): void;
    /**
     * Fügt eine Klausel der Größe 2 hinzu. Forciert damit, dass mindestens eine der beiden Variablen TRUE ist,
     * letzlich @code{x + y >= 1}.
     *
     * @param x Die Variable x der Klausel (x OR y).
     * @param y Die Variable y der Klausel (x OR y).
     */
    c_2(x: number, y: number): void;
    /**
     * Fügt eine Klausel der Größe 3 hinzu. Forciert damit, dass mindestens eine der drei Variablen TRUE ist,
     * letzlich @code{x + y + z >= 1}.
     *
     * @param x Die Variable x der Klausel (x OR y OR z).
     * @param y Die Variable y der Klausel (x OR y OR z).
     * @param z Die Variable z der Klausel (x OR y OR z).
     */
    c_3(x: number, y: number, z: number): void;
    /**
     * Forciert, dass nicht beide Variablen TRUE sind, letzlich @code{x + y ≤ 1}.
     *
     * @param x Die Variable x der Klausel (-x OR -y).
     * @param y Die Variable y der Klausel (-x OR -y).
     */
    c_not_both(x: number, y: number): void;
    /**
     * Liefert die Variable z für die {@code z = x AND y} gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     *
     * @return Die Variable z für die {@code z = x AND y} gilt.
     */
    c_new_var_AND(x: number, y: number): number;
    /**
     * Forciert, dass genau {@code amount} Variablen des Arrays den Wert TRUE haben.
     *
     * @param pArray Das Variablenarray.
     * @param amount Die Anzahl an TRUEs in der Variablenliste.
     */
    c_exactly_GENERIC(pArray: Array<number>, amount: number): void;
    /**
     * Forciert, dass genau {@code amount} Variablen der Variablenliste den Wert TRUE haben.
     *
     * @param list   Die Variablenliste.
     * @param amount Die Anzahl an TRUEs in der Variablenliste.
     */
    c_exactly_GENERIC(list: LinkedCollection<Number>, amount: number): void;
    /**
     * Forciert, dass höchstens {@code maximum} Variablen der Variablenliste den Wert TRUE haben.
     *
     * @param list    Die Variablenliste.
     * @param maximum Die maximale Anzahl an TRUEs in der Variablenliste.
     */
    c_at_most_GENERIC(list: LinkedCollection<Number>, maximum: number): void;
    /**
     * Forciert, dass genau eine Variable der Liste TRUE ist. Falls die Liste leer ist, führt das zur direkten
     * Unlösbarkeit der Formel.
     *
     * @param list Genau eine der Variablen der Liste muss TRUE sein.
     */
    private c_exactly_one;
    /**
     * Forciert, dass {@code z = x OR y} gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     * @param z Variable der obigen Gleichung.
     */
    private c_z_equals_x_or_y;
    /**
     * Liefert die Variable z für die {@code z = x OR y} gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     *
     * @return Die Variable z für die {@code z = x OR y} gilt.
     */
    private c_new_var_OR;
    /**
     * Forciert, dass in der Liste maximal eine Variable TRUE ist. Die Ergebnisvariable ist eine OR-Verknüpfung
     * aller Variablen der Liste.
     *
     * @param list Forciert, dass maximal eine Variable der Liste TRUE ist.
     *
     * @return Die Ergebnisvariable ist eine OR-Verknüpfung aller Variablen der Liste.
     */
    private c_at_most_one_tree;
    private c_exactly_NETWORK;
    private c_at_most_NETWORK;
    private c_bitonic_sort;
    private c_fill_False_until_power_two;
    private c_bitonic_sort_power_two;
    private c_bitonic_sort_spiral;
    private c_bitonic_sort_difference;
    private c_bitonic_comparator;
    private static toList;
    c_unequal(x: number, y: number): void;
    c_equal(x: number, y: number): void;
    isTranspiledInstanceOf(name: string): boolean;
}
export declare function cast_de_nrw_schule_svws_core_kursblockung_satsolver_SatSolverWrapper(obj: unknown): SatSolverWrapper;