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

Modifier and Type	Method and Description
static Formula	and(Formula... fms) Erzeugt die Konjunktion einer Liste von Formeln.
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	ff() Erzeugt die immer falsche Formel.
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... fms) Erzeugt die Disjunktion einer Liste von Formeln.
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 java.util.Map<java.lang.Object,java.lang.Boolean>	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	tt() Erzeugt die immer wahre Formel.
static Formula	var(java.lang.Object name) Erzeugt die Formel, die durch eine aussagenlogische Variable gegeben ist.
static java.util.Map<java.lang.Integer,java.lang.Object>	writeDIMACS(java.io.OutputStream os, Formula f) Wendet die Tseitin-Transformation an und schreibt das Ergebnis im DIMACS-Format in den os.
static Formula	xor(Formula fm1, Formula fm2) Erzeugt das exklusive Oder zweier Formeln.

Methods inherited from class java.lang.Object

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

Method Detail

var

public static Formula var(java.lang.Object name)

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

Parameters:

name - Name der Variable

tt

public static Formula tt()

Erzeugt die immer wahre Formel.

ff

public static Formula ff()

Erzeugt die immer falsche Formel.

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.

and

public static Formula and(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.

or

public static Formula or(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.

writeDIMACS

public static java.util.Map<java.lang.Integer,java.lang.Object> writeDIMACS(java.io.OutputStream os,
                                                                            Formula f)
                                                                     throws java.io.IOException

Wendet die Tseitin-Transformation an und schreibt das Ergebnis im DIMACS-Format in den os. Zurueckgegeben wird eine Map, welche die Zahlen im DIMACS-Text den Variablen in f zuordnet.

Throws:

java.io.IOException

satisfiable

public static java.util.Map<java.lang.Object,java.lang.Boolean> 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 eine erfuellende 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