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): 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;