cnf

Class CNF

java.lang.Object

cnf.CNF

public class CNF
extends java.lang.Object

Methoden zur Konstruktion von aussagenlogischen Formeln sowie zum Aufruf eines SAT-Solvers.

Diese Klasse ist das gesamte oeffentliche Interface des Pakets cnf. Die anderen Klassen stellen kein oeffentliches Interface bereit.

Method Summary

Methods

Modifier and Type	Method and Description
static Formula	and(Formula f1, Formula f2) Erzeugt die Konjunktion zweier Formeln.
static Formula	and(java.util.List<Formula> fms) Erzeugt die Konjunktion einer Liste von Formeln.
static Formula	cnf(Formula f) Gibt eine zur uebergebenen Formel erfuellbarkeitsaequivalente Formel in CNF zurueck.
static java.lang.String	cnfDIMACS(Formula f) Gibt eine zur uebergebenen Formel erfuellbarkeitsaequivalente Formel in CNF als String im DIMACS zurueck.
static VarName	freshVarName() Erzeugt eine neue Variable.
static Formula	iff(Formula fm1, Formula fm2) Erzeugt die Biimplikation zweier Formeln.
static Formula	imp(Formula fm1, Formula fm2) Erzeugt die Implikation zweier Formeln.
static Formula	neg(Formula f) Erzeugt die Negation einer gegbenen Formel.
static Formula	or(Formula f1, Formula f2) Erzeugt die Disjunktion zweier Formeln.
static Formula	or(java.util.List<Formula> fms) Erzeugt die Disjunktion einer Liste von Formeln.
static void	reset() Setzt den Variablennamengenerator zurueck.
static java.util.Set<VarName>	satisfiable(Formula f) Wandelt die uebergebene Formel in eine erfuellbarkeitsaequivalente Formel in CNF um und ueberprueft sie mittels des SAT-Solvers SAT4j auf Erfuellbarkeit.
static Formula	var(VarName name) Erzeugt die Formel, die durch eine aussagenlogische Variable gegeben ist.
static Formula	xor(Formula fm1, Formula fm2) Erzeugt das exklusive Oder zweier Formeln.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

var

public static Formula var(VarName name)

Erzeugt die Formel, die durch eine aussagenlogische Variable gegeben ist.

Parameters:

name - Name der Variable

neg

public static Formula neg(Formula f)

Erzeugt die Negation einer gegbenen Formel.

and

public static Formula and(Formula f1,
          Formula f2)

Erzeugt die Konjunktion zweier Formeln.

and

public static Formula and(java.util.List<Formula> fms)

Erzeugt die Konjunktion einer Liste von Formeln.

or

public static Formula or(Formula f1,
         Formula f2)

Erzeugt die Disjunktion zweier Formeln.

or

public static Formula or(java.util.List<Formula> fms)

Erzeugt die Disjunktion einer Liste von Formeln.

imp

public static Formula imp(Formula fm1,
          Formula fm2)

Erzeugt die Implikation zweier Formeln.

Parameters:

fm1 - Formel

fm2 - Formel

Returns:

Formel "fm1 => fm2"

iff

public static Formula iff(Formula fm1,
          Formula fm2)

Erzeugt die Biimplikation zweier Formeln.

Parameters:

fm1 - Formel

fm2 - Formel

Returns:

Formel "fm1 <=> fm2"

xor

public static Formula xor(Formula fm1,
          Formula fm2)

Erzeugt das exklusive Oder zweier Formeln.

cnf

public static Formula cnf(Formula f)

Gibt eine zur uebergebenen Formel erfuellbarkeitsaequivalente Formel in CNF zurueck.

Diese Methode kann zum Anzeigen der CNF einer Formel benutzt werden: System.out.println(cnf(f)).

Parameters:

f - Formel

Returns:

Formel in CNF, welche zu f erfuellbarkeitsaequivalent ist.

cnfDIMACS

public static java.lang.String cnfDIMACS(Formula f)

Gibt eine zur uebergebenen Formel erfuellbarkeitsaequivalente Formel in CNF als String im DIMACS zurueck.

satisfiable

public static java.util.Set<VarName> satisfiable(Formula f)
                                          throws TimeoutException

Wandelt die uebergebene Formel in eine erfuellbarkeitsaequivalente Formel in CNF um und ueberprueft sie mittels des SAT-Solvers SAT4j auf Erfuellbarkeit. Zurueckgegeben wird die Menge der wahren Variablen in einer erfuellenden Belegung von oder null, wenn es keine solche gibt.

Parameters:

f - Formel

Returns:

Menge der Variablen, die in einer erfuellenden Belegung von f wahr sind; oder null wenn f unerfuellbar ist.

Throws:

TimeoutException

freshVarName

public static VarName freshVarName()

Erzeugt eine neue Variable.

reset

public static void reset()

Setzt den Variablennamengenerator zurueck. Nach einem reset() sollte keine Formel mehr benutzt werden, die davor erzeugt wurde.