de.svws_nrw.core.adt.sat.SatInput

public final class SatInput extends Object

Diese Klasse definiert eine aussagenlogische Formel in konjunktiver Normalform (CNF). Die Formel besteht aus einer Menge von Klauseln, welche mit einem logischen UND verbunden sind. Jede Klausel beinhaltet booleschen Variablen (auch negiert), welche mit einem logischen ODER verbunden sind.
Ein sogenannter SAT-Solver erhält diese Formel als Eingabe und sucht nach einer Belegung der Variablen, so dass jede Klausel erfüllt (also TRUE) ist.

Konstruktorübersicht

Konstruktoren

Konstruktor

Beschreibung

SatInput()

Erzeugt eine neues Objekt.
Methodenübersicht

Modifizierer und Typ

Methode

Beschreibung

void

add_clause(@NotNull Integer @NotNull [] pVars)

Hinzufügen einer Klausel.

void

add_clause_1(int x)

Fügt eine Klausel der Größe 1 hinzu.

void

add_clause_2(int x, int y)

Fügt eine Klausel der Größe 2 hinzu.

void

add_clause_3(int x, int y, int z)

Fügt eine Klausel der Größe 3 hinzu.

void

add_clause_and_variables(@NotNull Integer @NotNull [] pVars)

Fügt eine Klausel hinzu.

void

add_clause_equal(int x, int y)

Forciert, dass beide Variablen gleich sind.

void

add_clause_exactly(@jakarta.validation.constraints.NotNull int[] pArray, int pAmount)

Forciert, dass genau pAmount Variablen des Arrays den Wert TRUE haben.

void

add_clause_exactly(@NotNull LinkedCollection<Integer> pList, int pAmount)

Forciert, dass genau pAmount Variablen der Variablenliste den Wert TRUE haben.

void

add_clause_exactly_in_column(@jakarta.validation.constraints.NotNull int @NotNull [] @NotNull [] pData, int pCol, int pAmount)

Forciert, dass genau pAmount Variablen der Matrix pData in Spalte pCol den Wert TRUE haben.

void

add_clause_exactly_in_row(@jakarta.validation.constraints.NotNull int @NotNull [] @NotNull [] pData, int pRow, int pAmount)

Forciert, dass genau pAmount Variablen der Matrix pData in Zeile pRow den Wert TRUE haben.

void

add_clause_not_both(int x, int y)

Forciert, dass nicht beide Variablen TRUE sind.

void

add_clause_unequal(int x, int y)

Forciert, dass beide Variablen ungleich sind.

int

create_var()

Erzeugte eine neue Variable.

int

create_var_AND(int x, int y)

Liefert die neu erzeugte Variable z für die 'z = x AND y' gilt.

int

create_var_at_most_one_tree(@NotNull LinkedCollection<Integer> pList)

Forciert, dass in der Liste maximal eine Variable TRUE ist.

int

create_var_OR(int x, int y)

Liefert die neu erzeugte Variable z für die 'z = x OR y' gilt.

@jakarta.validation.constraints.NotNull int[]

create_vars1D(int n)

Erzeugt mehrere Variablen auf einmal und liefert ein Array mit diesen zurück.

@jakarta.validation.constraints.NotNull int[] @NotNull []

create_vars2D(int rows, int cols)

Erzeugt mehrere Variablen auf einmal und liefert ein Array mit diesen zurück.

@NotNull List<Integer @NotNull []>

getClauses()

Liefert die Menge aller Klauseln.

@NotNull String

getDimacsHeader()

Liefert den Header des DIMACs Formats.

int

getVarCount()

Liefert die interne Anzahl an erzeugten Variablen.

int

getVarFALSE()

Liefert eine Variable, die zuvor auf FALSE forciert wurde.

int

getVarTRUE()

Liefert eine Variable, die zuvor auf TRUE forciert wurde.

boolean

isValidSolution(@jakarta.validation.constraints.NotNull int @NotNull [] solution)

Überprüft, ob die übergebene Lösung valide ist.

@NotNull String

toString()

Von Klasse geerbte Methoden java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Konstruktordetails

SatInput

public SatInput()

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:

     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}

Methodendetails
- toString
  
  @NotNull public @NotNull String toString()
  
  Setzt außer Kraft:
  
  toString in Klasse Object
- getVarTRUE
  
  public int getVarTRUE()
  
  Liefert eine Variable, die zuvor auf TRUE forciert wurde.
  
  Gibt zurück:
  
  Eine Variable, die zuvor auf TRUE forciert wurde.
- getVarFALSE
  
  public int getVarFALSE()
  
  Liefert eine Variable, die zuvor auf FALSE forciert wurde.
  
  Gibt zurück:
  
  Eine Variable, die zuvor auf FALSE forciert wurde.
- getVarCount
  
  public int getVarCount()
  
  Liefert die interne Anzahl an erzeugten Variablen.
  
  Gibt zurück:
  
  Die interne Anzahl an erzeugten Variablen.
- getClauses
  
  @NotNull public @NotNull List<Integer @NotNull []> getClauses()
  
  Liefert die Menge aller Klauseln.
  
  Gibt zurück:
  
  die Menge aller Klauseln.
- getDimacsHeader
  
  @NotNull public @NotNull String getDimacsHeader()
  
  Liefert den Header des DIMACs Formats. Diese zeigt die Variablen- und Klauselanzahl.
  
  Gibt zurück:
  
  den Header des DIMACs Formats. Diese zeigt die Variablen- und Klauselanzahl.
- create_var
  
  public int create_var()
  
  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.
  
  Gibt zurück:
  
  Die Nummer der neuen Variablen.
- create_vars1D
  
  @NotNull public @jakarta.validation.constraints.NotNull int[] create_vars1D(int n)
  
  Erzeugt mehrere Variablen auf einmal und liefert ein Array mit diesen zurück.
  Siehe auch: create_var()
  
  Parameter:
  
  n - die Anzahl an zu erzeugenden Variablen.
  
  Gibt zurück:
  
  ein Array mit den neuen Variablen.
- create_vars2D
  
  @NotNull public @jakarta.validation.constraints.NotNull int[] @NotNull [] create_vars2D(int rows, int cols)
  
  Erzeugt mehrere Variablen auf einmal und liefert ein Array mit diesen zurück.
  Siehe auch: create_var()
  
  Parameter:
  
  rows - die Anzahl an Zeilen eines 2D-Arrays.
  
  cols - die Anzahl an Spalten eines 2D-Arrays.
  
  Gibt zurück:
  
  ein Array mit den neuen Variablen.
- create_var_AND
  
  public int create_var_AND(int x, int y)
  
  Liefert die neu erzeugte Variable z für die 'z = x AND y' gilt.
  
  Parameter:
  
  x - Variable der obigen Gleichung.
  
  y - Variable der obigen Gleichung.
  
  Gibt zurück:
  
  die neu erzeugte Variable z für die 'z = x AND y' gilt.
- create_var_OR
  
  public int create_var_OR(int x, int y)
  
  Liefert die neu erzeugte Variable z für die 'z = x OR y' gilt.
  
  Parameter:
  
  x - Variable der obigen Gleichung.
  
  y - Variable der obigen Gleichung.
  
  Gibt zurück:
  
  die neu erzeugte Variable z für die 'z = x OR y' gilt.
- create_var_at_most_one_tree
  
  public int create_var_at_most_one_tree(@NotNull @NotNull LinkedCollection<Integer> pList)
  
  Forciert, dass in der Liste maximal eine Variable TRUE ist. Die Ergebnisvariable ist eine OR-Verknüpfung aller Variablen der Liste.
  
  Parameter:
  
  pList - Forciert, dass maximal eine Variable der Liste TRUE ist.
  
  Gibt zurück:
  
  Die Ergebnisvariable ist eine OR-Verknüpfung aller Variablen der Liste.
- add_clause
  
  public void add_clause(@NotNull @NotNull Integer @NotNull [] pVars) throws DeveloperNotificationException
  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.
  
  Das Array [-3, 8, 2] wird als (NOT x3) OR x8 OR x2 interpretiert.
  Die Menge aller Klauseln sind mit einem AND verknüpft.
  Parameter:
  
  pVars - Die Variablen (auch negiert) der Klausel mit den zuvor generierten Variablen.
  
  Löst aus:
  
  DeveloperNotificationException - falls die angegebenen Variablen ungültig sind.
- add_clause_and_variables
  
  public void add_clause_and_variables(@NotNull @NotNull Integer @NotNull [] pVars) throws DeveloperNotificationException
  
  Fügt eine Klausel hinzu. Falls die Variablen noch nicht existieren, werden sie erzeugt.
  
  Parameter:
  
  pVars - Die Variablen (auch negiert) der Klausel.
  
  Löst aus:
  
  DeveloperNotificationException - falls die Klausel leer ist, oder eine Variable 0 ist.
- add_clause_1
  
  public void add_clause_1(int x)
  
  Fügt eine Klausel der Größe 1 hinzu. Forciert damit die übergebene Variable auf TRUE.
  
  Parameter:
  
  x - Die Variable wird auf TRUE gesetzt.
- add_clause_2
  
  public void add_clause_2(int x, int y)
  
  Fügt eine Klausel der Größe 2 hinzu. Forciert damit, dass mindestens eine der beiden Variablen TRUE ist.
  
  Parameter:
  
  x - Die Variable x der Klausel (x OR y).
  
  y - Die Variable y der Klausel (x OR y).
- add_clause_3
  
  public void add_clause_3(int x, int y, int z)
  
  Fügt eine Klausel der Größe 3 hinzu. Forciert damit, dass mindestens eine der drei Variablen TRUE ist.
  
  Parameter:
  
  x - Die Variable x der Klausel (x OR y OR z).
  
  y - Die Variable y der Klausel (x OR y OR z).
  
  z - Die Variable z der Klausel (x OR y OR z).
- add_clause_not_both
  
  public void add_clause_not_both(int x, int y)
  
  Forciert, dass nicht beide Variablen TRUE sind.
  
  Parameter:
  
  x - Die Variable x der Klausel (-x OR -y).
  
  y - Die Variable y der Klausel (-x OR -y).
- add_clause_equal
  
  public void add_clause_equal(int x, int y)
  
  Forciert, dass beide Variablen gleich sind.
  
  Parameter:
  
  x - Die Variable x der Bedingung (x = y).
  
  y - Die Variable y der Bedingung (x = y).
- add_clause_unequal
  
  public void add_clause_unequal(int x, int y)
  
  Forciert, dass beide Variablen ungleich sind.
  
  Parameter:
  
  x - Die Variable x der Bedingung (x != y).
  
  y - Die Variable y der Bedingung (x != y).
- add_clause_exactly
  
  public void add_clause_exactly(@NotNull @jakarta.validation.constraints.NotNull int[] pArray, int pAmount)
  
  Forciert, dass genau pAmount Variablen des Arrays den Wert TRUE haben.
  
  Parameter:
  
  pArray - Das Array der Variablen.
  
  pAmount - Die Anzahl an TRUEs in der Variablenliste.
- add_clause_exactly
  
  public void add_clause_exactly(@NotNull @NotNull LinkedCollection<Integer> pList, int pAmount)
  
  Forciert, dass genau pAmount Variablen der Variablenliste den Wert TRUE haben.
  
  Parameter:
  
  pList - Die Variablenliste.
  
  pAmount - Die Anzahl an TRUEs in der Variablenliste.
- add_clause_exactly_in_row
  
  public void add_clause_exactly_in_row(@NotNull @jakarta.validation.constraints.NotNull int @NotNull [] @NotNull [] pData, int pRow, int pAmount)
  
  Forciert, dass genau pAmount Variablen der Matrix pData in Zeile pRow den Wert TRUE haben.
  
  Parameter:
  
  pData - Die Matrix.
  
  pRow - Die Zeile der Matrix.
  
  pAmount - Die Anzahl an TRUEs.
- add_clause_exactly_in_column
  
  public void add_clause_exactly_in_column(@NotNull @jakarta.validation.constraints.NotNull int @NotNull [] @NotNull [] pData, int pCol, int pAmount)
  
  Forciert, dass genau pAmount Variablen der Matrix pData in Spalte pCol den Wert TRUE haben.
  
  Parameter:
  
  pData - Die Matrix.
  
  pCol - Die Spalte der Matrix.
  
  pAmount - Die Anzahl an TRUEs.
- isValidSolution
  
  public boolean isValidSolution(@NotNull @jakarta.validation.constraints.NotNull int @NotNull [] solution)
  
  Überprüft, ob die übergebene Lösung valide ist.
  
  Parameter:
  
  solution - Die übergebene Lösung.
  
  Gibt zurück:
  
  TRUE, falls die Lösung alle Klauseln des Inputs erfüllt.

Klasse SatInput

Konstruktorübersicht

Methodenübersicht

Von Klasse geerbte Methoden java.lang.Object

Konstruktordetails

SatInput

Methodendetails

toString

getVarTRUE

getVarFALSE

getVarCount

getClauses

getDimacsHeader

create_var

create_vars1D

create_vars2D

create_var_AND

create_var_OR

create_var_at_most_one_tree

add_clause

add_clause_and_variables

add_clause_1

add_clause_2

add_clause_3

add_clause_not_both

add_clause_equal

add_clause_unequal

add_clause_exactly

add_clause_exactly

add_clause_exactly_in_row

add_clause_exactly_in_column

isValidSolution