import { JavaObject } from '../../../java/lang/JavaObject';
import { LinkedCollection } from '../../../core/adt/collection/LinkedCollection';
import type { List } from '../../../java/util/List';
import { Class } from '../../../java/lang/Class';
export declare class SatInput extends JavaObject {
    /**
     * Die aktuelle Anzahl an Variablen.
     */
    private _nVars;
    /**
     * Eine Variable, die mit Hilfe einer Klausel auf TRUE forciert wird und somit eine Konstante ist.
     */
    private _varTRUE;
    /**
     * Eine Variable, die mit Hilfe einer Klausel auf FALSE forciert wird und somit eine Konstante ist.
     */
    private _varFALSE;
    /**
     * Die aktuelle Anzahl an Variablen.
     */
    private readonly _clauses;
    /**
     * Erzeugt eine neues Objekt. Anschließend lassen sich Variablen erzeugen und Klauseln hinzufügen.
     * Möchte man die Formel f = (x1 OR x2 OR NOT x3) AND (NOT x2 OR x3) AND (x5) kodieren, so funktioniert das so:  <br>
     * <pre>
     *     SatFormula f = new SatFormula();
     *     int x1 = f.createNewVar();
     *     int x2 = f.createNewVar();
     *     int x3 = f.createNewVar();
     *     f.createNewVar(); // not used
     *     int x5 = f.createNewVar();
     *
     *     f.addClause(new int[] {x1, x2, -x3}); // adds {1, 2, -3}
     *     f.addClause(new int[] {-x2, x3});     // adds {-2, 3}
     *     f.addClause(new int[] {x5});          // adds {5}
     * </pre>
     */
    constructor();
    toString(): string;
    /**
     * Liefert eine Variable, die zuvor auf TRUE forciert wurde.
     *
     * @return Eine Variable, die zuvor auf TRUE forciert wurde.
     */
    getVarTRUE(): number;
    /**
     * Liefert eine Variable, die zuvor auf FALSE forciert wurde.
     *
     * @return Eine Variable, die zuvor auf FALSE forciert wurde.
     */
    getVarFALSE(): number;
    /**
     * Liefert die interne Anzahl an erzeugten Variablen.
     *
     * @return Die interne Anzahl an erzeugten Variablen.
     */
    getVarCount(): number;
    /**
     * Liefert die Menge aller Klauseln.
     *
     * @return die Menge aller Klauseln.
     */
    getClauses(): List<Array<number>>;
    /**
     * Liefert den Header des DIMACs Formats. Diese zeigt die Variablen- und Klauselanzahl.
     *
     * @return den Header des DIMACs Formats. Diese zeigt die Variablen- und Klauselanzahl.
     */
    getDimacsHeader(): string;
    /**
     * 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. Ebenso darf
     * eine Variable nicht 0 sein, da im DIMACS CNF FORMAT das Symbol 0 zum Kodieren eines Zeilenendes benutzt wird.
     *
     * @return Die Nummer der neuen Variablen.
     */
    create_var(): number;
    /**
     * Erzeugt mehrere Variablen auf einmal und liefert ein Array mit diesen zurück. <br>
     * Siehe auch: {@link SatInput#create_var()}
     *
     * @param n die Anzahl an zu erzeugenden Variablen.
     *
     * @return ein Array mit den neuen Variablen.
     */
    create_vars1D(n: number): Array<number>;
    /**
     * Erzeugt mehrere Variablen auf einmal und liefert ein Array mit diesen zurück. <br>
     * Siehe auch: {@link SatInput#create_var()}
     *
     * @param rows die Anzahl an Zeilen eines 2D-Arrays.
     * @param cols die Anzahl an Spalten eines 2D-Arrays.
     *
     * @return ein Array mit den neuen Variablen.
     */
    create_vars2D(rows: number, cols: number): Array<Array<number>>;
    /**
     * Liefert die neu erzeugte Variable z für die 'z = x AND y' gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     *
     * @return die neu erzeugte Variable z für die 'z = x AND y' gilt.
     */
    create_var_AND(x: number, y: number): number;
    /**
     * Liefert die neu erzeugte Variable z für die 'z = x OR y' gilt.
     *
     * @param x Variable der obigen Gleichung.
     * @param y Variable der obigen Gleichung.
     *
     * @return die neu erzeugte Variable z für die 'z = x OR y' gilt.
     */
    create_var_OR(x: number, y: number): number;
    /**
     * Forciert, dass in der Liste maximal eine Variable TRUE ist.
     * Die Ergebnisvariable ist eine OR-Verknüpfung aller Variablen der Liste.
     *
     * @param pList Forciert, dass maximal eine Variable der Liste TRUE ist.
     *
     * @return Die Ergebnisvariable ist eine OR-Verknüpfung aller Variablen der Liste.
     */
    create_var_at_most_one_tree(pList: LinkedCollection<number>): number;
    /**
     * Hinzufügen einer Klausel. Eine Klausel ist eine nicht leere Menge von Variablen,
     * die mit einem logischen ODER verknüpft sind. Die Variablen dürfen negiert sein. <br>
     * <pre>
     * Das Array [-3, 8, 2]
     * wird als  (NOT x3) OR x8 OR x2 interpretiert.
     * </pre>
     * Die Menge aller Klauseln sind mit einem AND verknüpft.
     *
     * @param pVars Die Variablen (auch negiert) der Klausel mit den zuvor generierten Variablen.
     *
     * @throws DeveloperNotificationException falls die angegebenen Variablen ungültig sind.
     */
    add_clause(pVars: Array<number>): void;
    /**
     * Fügt eine Klausel hinzu. Falls die Variablen noch nicht existieren, werden sie erzeugt.
     *
     * @param pVars Die Variablen (auch negiert) der Klausel.
     *
     * @throws DeveloperNotificationException falls die Klausel leer ist, oder eine Variable 0 ist.
     */
    add_clause_and_variables(pVars: Array<number>): void;
    /**
     * Fügt eine Klausel der Größe 1 hinzu. Forciert damit die übergebene Variable auf TRUE.
     *
     * @param x Die Variable wird auf TRUE gesetzt.
     */
    add_clause_1(x: number): void;
    /**
     * Fügt eine Klausel der Größe 2 hinzu. Forciert damit, dass mindestens eine der beiden Variablen TRUE ist.
     *
     * @param x Die Variable x der Klausel (x OR y).
     * @param y Die Variable y der Klausel (x OR y).
     */
    add_clause_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.
     *
     * @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).
     */
    add_clause_3(x: number, y: number, z: number): void;
    /**
     * Forciert, dass nicht beide Variablen TRUE sind.
     *
     * @param x Die Variable x der Klausel (-x OR -y).
     * @param y Die Variable y der Klausel (-x OR -y).
     */
    add_clause_not_both(x: number, y: number): void;
    /**
     * Forciert, dass beide Variablen gleich sind.
     *
     * @param x Die Variable x der Bedingung (x = y).
     * @param y Die Variable y der Bedingung (x = y).
     */
    add_clause_equal(x: number, y: number): void;
    /**
     * Forciert, dass beide Variablen ungleich sind.
     *
     * @param x Die Variable x der Bedingung (x != y).
     * @param y Die Variable y der Bedingung (x != y).
     */
    add_clause_unequal(x: number, y: number): void;
    /**
     * Forciert, dass genau {@code pAmount} Variablen des Arrays den Wert TRUE haben.
     *
     * @param pArray  Das Array der Variablen.
     * @param pAmount Die Anzahl an TRUEs in der Variablenliste.
     */
    add_clause_exactly(pArray: Array<number>, pAmount: number): void;
    /**
     * Forciert, dass genau {@code pAmount} Variablen der Variablenliste den Wert TRUE haben.
     *
     * @param pList   Die Variablenliste.
     * @param pAmount Die Anzahl an TRUEs in der Variablenliste.
     */
    add_clause_exactly(pList: LinkedCollection<number>, pAmount: number): void;
    /**
     * Forciert, dass genau {@code pAmount} Variablen der Matrix {@code pData} in Zeile {@code pRow} den Wert TRUE haben.
     *
     * @param pData   Die Matrix.
     * @param pRow    Die Zeile der Matrix.
     * @param pAmount Die Anzahl an TRUEs.
     */
    add_clause_exactly_in_row(pData: Array<Array<number>>, pRow: number, pAmount: number): void;
    /**
     * Forciert, dass genau {@code pAmount} Variablen der Matrix {@code pData} in Spalte {@code pCol} den Wert TRUE haben.
     *
     * @param pData   Die Matrix.
     * @param pCol    Die Spalte der Matrix.
     * @param pAmount Die Anzahl an TRUEs.
     */
    add_clause_exactly_in_column(pData: Array<Array<number>>, pCol: number, pAmount: number): void;
    /**
     * Forciert, dass genau eine Variable der Liste TRUE ist. <br>
     * Falls die Liste leer ist, führt das zur direkten Unlösbarkeit der Formel.
     *
     * @param pList Menge an Variablen von denen genau eine TRUE sein soll.
     */
    private add_clause_exactly_one;
    private _bitonic_exactly;
    private _bitonic_sort;
    private _bitonic_fill_FALSE_until_power_two;
    private _bitonic_sort_power_two;
    private _bitonic_sort_spiral;
    private _bitonic_sort_difference;
    private _bitonic_comparator;
    /**
     * Überprüft, ob die übergebene Lösung valide ist.
     *
     * @param solution Die übergebene Lösung.
     * @return TRUE, falls die Lösung alle Klauseln des Inputs erfüllt.
     */
    isValidSolution(solution: Array<number>): boolean;
    transpilerCanonicalName(): string;
    isTranspiledInstanceOf(name: string): boolean;
    static class: Class<SatInput>;
}
export declare function cast_de_svws_nrw_core_adt_sat_SatInput(obj: unknown): SatInput;
//# sourceMappingURL=SatInput.d.ts.map