Commit fbea7a8c authored by Amin Raslan's avatar Amin Raslan
Browse files

Replace hintergrundwissen.tex

parent 7f40101a
\section{Hintergrundwissen}
Programmiersprachen können in der Regel verschiedene Programmierparadigmen erlauben, wobei grob zwischen der \emph{imperativen} und der \emph{deklarativen} Programmierung unterschieden wird. Bei der imperativen Programmierung wird beschrieben, wie etwas berechnet werden soll. Der Programmierer gibt also eine Folge von Anweisungen (Befehlen) in einer bestimmten Reihenfolge vor, die dann festlegen, was der Computer tun soll. Prozedurale und objektorientierte Programmierung sind beispielhafte Programmierparadigmen, die dieses Prinzip verwenden. Im Gegensatz dazu wird bei der deklarativen Programmierung beschrieben, was berechnet werden soll. Der Programmierer versorgt den Computer also mit Informationen, welcher dann einen Lösungsraum aufbaut und versucht, eine Lösung zu finden. Funktionale und logische Programmierung sind beispielhafte Programmierparadigmen, die dieses Prinzip verwenden \cite{programmierparadigma}. Diese Arbeit beschäftigt sich grundsätzlich mit der logischen Programmierung. Die logische Programmierung wurde unter Anderem aus dem Versuch entwickelt, logische Theoreme mithilfe der Machine zu beweisen, wie zum Beispiel zu beweisen, dass ein Theorem wie $X \rightarrow Z$ aus den logischen Axiomen $X \rightarrow Y$ und $Y \rightarrow Z$ folgt. Es können aber auch Probleme in anderen Bereichen als Theoreme betrachten werden, wie arithmetische Aufgaben sowie Datenbanken \cite{logische_programmierung}. Logische Programmierung findet unter Anderem Einsatz in der künstlichen Intelligenz, Programmentwicklung, Datenbanken, Sprachverarbeitung, Computer Aided Desgin und Constraintprogrammierung \cite{einsatz_logischer_programmierung}, was das Thema dieser Arbeit ist.
\subsection{Prolog} %Backtracking
\subsection{Prolog}
Die logische Porgrammiersprache Prolog wurde vom französischen Informatiker Alain Colmerauer entwickelt und ist das Resultat eines Projektes, dessen Ziel es eigentlich war, mit der Machine direkt auf Französisch zu kommunizieren. Der Name Prolog wurde aus dem Französischen abgeleitet: \enquote{\textbf{Pro}grammation en \textbf{log}ique} \cite{geschichte_von_prolog} (Im Deutschen: Programmieren in Logik).
Prolog-Programme bestehen aus Fakten (atomare Aussagen) und Regeln, die vom Benutzer geschrieben werden und vom Prolog-Interpreter dann verwendet werden, um eine Lösung zu finden \cite{prolog}.
......@@ -19,7 +19,7 @@ grosselternteil(X, Z) :-
\label{bsp:prolog_bsp}
\end{beispiel}
In Beispiel~\ref{bsp:prolog_bsp} haben wir 2 Fakten in den ersten 2 Zeilen, die uns die Auskunft geben, dass Alena ein Elternteil von Christoph und Christoph ein Elternteil von Johannes ist. Weiterhin haben wir eine Regel in Zeile 4 (auch Prädikat genannt), die uns sagt, dass X ein Großelternteil von Z ist, wenn ein Y existiert, so dass X ein Elternteil von Y (Zeile 5) und Y ein Elternteil von Z ist (Zeile 6). Nun können wir Anfragen an das System stellen und es antwortet dann mit "yes", falls es eine Lösung gibt, oder "no", falls keine Lösung existiert. Wenn wir außerdem Anfragen mit Variablen stellen, dann liefert das System uns Ergebnisse, wenn es Lösungen gefunden hat:
In Beispiel~\ref{bsp:prolog_bsp} haben wir 2 Fakten in den ersten 2 Zeilen, die uns die Auskunft geben, dass Alena ein Elternteil von Christoph und Christoph ein Elternteil von Johannes ist. Weiterhin haben wir eine Regel in Zeile 4 (auch Prädikat genannt), die uns sagt, dass X ein Großelternteil von Z ist, wenn ein Y existiert, so dass X ein Elternteil von Y (Zeile 5) und Y ein Elternteil von Z ist (Zeile 6). Es ist zu beachten, dass die Fakten und Regeln klein- und die Variablen großgeschrieben werden. Nun können wir Anfragen an das System stellen und es antwortet dann mit "yes", falls es eine Lösung gibt, oder "no", falls keine Lösung existiert. Wenn wir außerdem Anfragen mit Variablen stellen, dann liefert das System uns Ergebnisse, wenn es Lösungen gefunden hat:
\begin{itemize}
\item Anfrage: elternteil(alena, christoph) \newline
......@@ -30,8 +30,12 @@ Antwort: no
Antwort: X = alena
\end{itemize}
Prolog basiert auf dem Prinzip der Resolution, in dem versucht wird, Lösungen durch Negieren und Widerlegen mit dem Resolutionsschritt
\begin{center}
$(a \vee b) \wedge (\neg b \vee c) \rightarrow a \vee c$
\end{center}
Prolog basiert auf dem Prinzip der Resolution, in dem versucht wird, Lösungen durch Negieren und Widerlegen zu finden. Prolog-Programme bestehen aus Horn-Klauseln. Eine Horn-Klausel ist eine Disjunktion von Literalen, wobei höchstens ein Literal positiv sein kann. Ein Literal ist eine positive oder negative atomare Aussage. Jede Regel der Form
zu finden. Prolog-Programme bestehen aus Horn-Klauseln. Eine Horn-Klausel ist eine Disjunktion von Literalen, wobei höchstens ein Literal positiv sein kann. Ein Literal ist eine positive oder negative atomare Aussage. Jede Regel der Form
\begin{center}
\emph{X $\to$ Y, Z}
\end{center}
......@@ -46,10 +50,14 @@ In Beispiel~\ref{bsp:prolog_bsp} haben wir 3 Horn-Klauseln:
\item elternteil(christoph, johannes)
\item grosselternteil(X, Z) $\lor$ $\neg$elternteil(X, Y) $\lor$ $\neg$elternteil(Y, Z)
\end{enumerate}
Ein weiteres Merkmal im Resolutionprinzip ist die Unifikation. Das ist der Prozess, zwei atomare Formeln mithilfe einer Substitution $\theta$ syntaktisch äquivalent zu machen \cite{prolog}.
Die Anfragen, die an ein Prolog-Programm geschickt werden, sind Disjunktionen von Literalen, wobei kein Literal positiv ist. Wenn eine Anfrage geschickt wird, dann wird von oben nach unten im Programm versucht, mithilfe von der Unifikation und der Resolution einen Widerspruch zu finden. Falls ein Widerspruch gefunden wird, dann existiert für diese Anfrage eine Lösung. Betrachten wir die Anfrage \emph{elternteil(alena, christoph)} an Programm~\ref{programm:prolog_bsp}. Zuerst wird diese Anfrage zu einer Disjunktion von negativen Literalen gemacht, nämlich \emph{$\neg$elternteil(alena, christoph)}. Dann fangen wir an, für die Formeln von oben nach unten im Programm zu prüfen, ob wir eine Lösung für unsere Anfrage finden können. Wir starten von oben, da Prolog-Programme Listen von Prädikaten sind. In diesen Listen wird von Anfang (also von oben) zum Ende gesucht. Wir fangen also mit der ersten atomaren Formel in Zeile 1 im Programm an, nämlich \emph{elternteil(alena, christoph)}, und versuchen, eine Substitution $\theta$ zu finden, so dass unsere Anfrage und diese erste atomare Formel syntaktisch identisch sind. Diese sind aber schon syntaktisch identisch. Also haben wir die Substitution $\theta = \emptyset$ gefunden. Der nächste Schritt ist eine Resolution zwischen ihnen. Damit erhalten wir
Die Anfragen, die vom Benutzer an ein Prolog-Programm geschickt werden, sind Disjunktionen von negativen Prädikaten. Wenn eine Anfrage geschickt wird, dann wird von oben nach unten im Programm versucht, mithilfe von der Unifikation und der Resolution einen Widerspruch zu finden. Falls ein Widerspruch gefunden wird, dann existiert für diese Anfrage eine Lösung. Wir starten von oben, da Prolog-Programme Listen von Prädikaten sind. In diesen Listen wird von Anfang (also von oben) zum Ende (also nach unten) gesucht.
Betrachten wir zum Beispiel die Anfrage \emph{elternteil(alena, christoph)} an Beispiel~\ref{bsp:prolog_bsp}. Zuerst wird diese Anfrage negiert. Wir erhalten also \emph{$\neg$elternteil(alena, christoph)}. Dann fangen wir an, für die Formeln von oben nach unten im Programm zu prüfen, ob wir eine Lösung für unsere Anfrage finden können. Wir fangen also mit der ersten atomaren Formel in Zeile 1 im Programm an, nämlich \emph{elternteil(alena, christoph)}, und versuchen, eine Substitution $\theta$ zu finden, so dass unsere Anfrage und diese erste atomare Formel syntaktisch identisch sind. Diese sind aber schon syntaktisch identisch. Also haben wir die Substitution $\theta = \emptyset$ gefunden. Der nächste Schritt ist eine Resolution zwischen ihnen.
Damit erhalten wir
\begin{center}
\emph{$\neg$elternteil(alena, christoph)} $\wedge$ \emph{elternteil(alena, christoph)} $\rightarrow$ $\Box$.
\end{center}
......@@ -65,17 +73,18 @@ Y is 1 + 2
In diesem Fall erhält die Variable Y den Wert 3. Wie hier zu sehen ist, steht auf der linken Seite von \emph{is} die Variable Y und auf der rechten Seite von \emph{is} Integer-Werte. Dies ist die einzige Anordnung mit \emph{is}. Das bedeutet, dass keine Argumente auf der rechten Seite von \emph{is} stehen können, die teilweise oder gar nicht initialisiert sind, wie in
\begin{center}
\textcolor{red}{! 3 is Y + 2 !}
\textcolor{red}{3 is Y + 2}
\end{center}
Constraint Logic Programming over Finite Domains (CLP(FD)) ist unter Anderem eine Erweiterung von der logischen Programmierung um arithmetische Constraints, die diese Prädikate ersetzen können. Wir können das Prädikat \emph{is/2} durch das arithmetische Constraint \emph{\#=/2} ersetzen. Dies funktioniert in allen Richtungen:
Diese Anfrage erzeugt eine Fehlermeldung. Constraint Logic Programming over Finite Domains (CLP(FD)) ist unter Anderem eine Erweiterung von der logischen Programmierung um arithmetische Constraints, die diese beschränkten Prädikate ersetzen können. Wir können das Prädikat \emph{is/2} durch das arithmetische Constraint \emph{\#=/2} ersetzen. Dies funktioniert in allen Richtungen:
\begin{center}
3 \#= Y + 2
\end{center}
hier erhalten die Antwort Y = 1.
CLP(FD)-Constraints ersetzen also arithmetische Prädikate auf niedriger Ebene (low-level arithmetic predicates). Jede Variable in CLP(FD) hat einen Domänenbereich. Anfangs entsprecehen diese Domänen der Menge aller Integer-Werte. CLP(FD)-Constraints wie \emph{\#=/2}, \emph{\#\slash=/2}, \emph{\#</2} und \emph{\#>/2} können die Domänen ihrer Argumente reduzieren (aber niemals erweitern). Außerdem können wir mithilfe von den Constraints \emph{in/2} und \emph{domain/3} Domänen von CLP(FD)-Variablen explizit angeben \cite{clpfd}.
hier erhalten die Antwort Y = 1. CLP(FD)-Constraints ersetzen also arithmetische Prädikate auf niedriger Ebene (low-level arithmetic predicates) und können in allen Richtungen funktionieren.
Jede Variable in CLP(FD) hat einen Domänenbereich. Anfangs entsprecehen diese Domänen der Menge aller Integer-Werte. CLP(FD)-Constraints wie \emph{\#=/2}, \emph{\#\slash=/2}, \emph{\#</2} und \emph{\#>/2} können die Domänen ihrer Argumente reduzieren (aber niemals erweitern). Außerdem können wir mithilfe von den Constraints \emph{in/2} und \emph{domain/3} Domänen von CLP(FD)-Variablen explizit angeben \cite{clpfd}.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
......@@ -97,6 +106,19 @@ Bis jetzt erhalten wir Domänen als Lösungen für unsere Variablen. Mit \emph{l
Es ist zu beachten, dass die Bibliothek \emph{clpfd} eingefügt werden soll (Zeile 1), damit auf die CLP(FD)-Constraints zugegriffen werden kann. Dies ist der Fall in jedem der 14 in CLP(FD) implementierten Modellen.
\subsubsection*{Coroutinen}
Zusätzlich zu Constraint Logic Programming können Coroutinen in Prolog verwendet, um die Anordnung eines Prädikats nach Wunsch zu ändern. Unter Anderem werden Block Declarations angeboten, die im Kapitel \emph{13.3 K Dominating Set} verwendet werden. Betrachten wir das Prädikat \emph{is\slash2} in Beispiel~\ref{bsp:coroutenen}. In diesem Beispiel wird das Prädikat \emph{sum\slash3} implementiert, der 2 Zahlen erhält und ihre Summe mithilfe von \emph{is} berechnet und zurückgibt. Vor diesem Prädikat implementieren wir einen Block, der blockiert, wenn das erste Argument im Prädikat eine Variable ist. Der Strich in der Blockdefinition bedeutet also, dass blockiert wird, wenn hier eine Variable kommt, und das Fragezeichen bedeutet, dass hier Variablen kommen können. Wenn wir das Prädikat nun mit \emph{sum(A, 2, B)} aufrufen, dann wird blockiert und wir erhalten keine Antwort. Wenn wir jedoch den Aufruf \emph{sum(A, 2, B), sum(1, 2, A)} haben, dann erhalten wir die Antwort \emph{A = 3, B = 5}. Ohne den Block würden wir wegen Zeile 3 im Beispiel immer eine Fehlermeldung erhalten, da die rechte Seite von \emph{is} eine Variable enthält, nämlich die Variable \emph{A}. Mit dem Block wird der Aufruf \emph{sum(A, 2, B)} blockiert und deswegen \emph{sum(1, 2, A)} zuerst ausgeführt. So erhält die Variable \emph{A} einen Wert, nämlich 3. Nun kann \emph{sum(A, 2, B)} beziehungsweise \emph{sum(3, 2, B)} ausgeführt werden.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
:- block sum(-, ?, ?).
sum(A, B, AB) :-
AB is A + B.
\end{minted}
\caption{Coroutenen: Ein Beispiel von Block Declarations}
\label{bsp:coroutenen}
\end{beispiel}
\subsection{MiniZinc}
MiniZinc ist eine Open-Source Sprache zur Spezifizierung von Constrained-Optimierungs- und Constrained-Entscheidungsproblemen über Integer und reelle Zahlen \cite{minizinc_introduction}.
......@@ -108,11 +130,9 @@ MiniZinc-Modelle können so ähnlich wie mathematische Formulierungen der Proble
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
var int: X;
var int: Y;
var 1..3: X;
var 1..3: Y;
constraint X >= 1 /\ X <= 3;
constraint Y >= 1 /\ Y <= 3;
constraint X < Y;
solve satisfy;
......@@ -121,36 +141,14 @@ solve satisfy;
\label{bsp:minizinc_bsp}
\end{beispiel}
In Beispiel~\ref{bsp:minizinc_bsp} haben wir die Implementierung von Beispiel~\ref{bsp:clpfd_bsp} in MiniZinc. Wir definieren wieder die 2 Variablen $X$ und $Y$, deren Werte Integer-Werte sind. Dann haben wir 3 Einschränkungen (Constraints), wobei die ersten 2 die Domänen von X und Y auf $[1,3]$ reduzieren. Dann sagen wir dem Computer mit \emph{solve satisfy}, dass wir eine Lösung suchen. Es gibt außerdem \emph{solve maximize X} beziehungsweise \emph{solve minimize X}, bei denen X maximiert beziehungsweise minimiert werden soll.
In MiniZinc ist es möglich, die Domänen von den Variablen in ihren Definitionen zu bestimmen. So wird das Modell kürzer und übersichtlicher, wie in Beispiel~\ref{bsp:domaenenbestimmung_in_variablendefinition} zu sehen ist.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
var 1..3: X;
var 1..3: Y;
In Beispiel~\ref{bsp:minizinc_bsp} haben wir die Implementierung von Beispiel~\ref{bsp:clpfd_bsp} in MiniZinc. Wir definieren wieder die 2 Variablen $X$ und $Y$, deren Werte im Bereich $[1,3]$ liegen. Dann implementieren wir die Einschränkung (das Constraint), dass $X < Y$ sein soll. Mit \emph{solve satisfy} wird dann nach möglichen Lösungen zu diesem Constraint gesucht. Zusätzlich zu \emph{solve satisfy} gibt es auch die Möglichkeiten \emph{solve maximize $Z$} und \emph{solve minimize $Z$}, bei denen die Variable $Z$ maximiert beziehungsweise minimiert werden soll. Es ist zu beachten, dass wir \emph{var} in den Definitionen von $X$ und $Y$ verwenden. Dies bedeutet, dass für $X$ und $Y$ nach Lösungen im gegebenen Bereich $[1,3]$ gesucht werden soll. Wenn wir \emph{var} nicht verwenden, dann müssen wir den Variablen $X$ und $Y$ feste Werte geben.
constraint X < Y;
solve satisfy;
\end{minted}
\caption{Domänenbestimmung in der Definition der Variable}
\label{bsp:domaenenbestimmung_in_variablendefinition}
\end{beispiel}
MiniZinc-Modelle werden sowohl in der MiniZincIDE als auc über SICStus-Prolog aufgerufen. In SICStus-Prolog werden dafür bestimmte Prädikate verwendet. Diese befinden sich in der Bibleothek \emph{zinc}. Das Prädikat \emph{mzn\_load\_file(+MznFile, +Options, -FznState)} erhält eine MiniZinc-Datei mit der Endung \emph{.mzn} mit weiteren Optionen und erzeugt eine äquivalente FlatZinc-Datei \emph{FznState}. Unter den Optionen sind \emph{parameters\slash1} und \emph{variables\slash1}. In \emph{parameters} können wir Parameter an die MiniZinc-Datei geben und mit \emph{variables} können wir Ausgaben von der Datei erhalten. Siehe Anhang~\ref{subsubsection:n_factorial_minizinc_sicstus} für ein Beispiel für den Aufruf vom MiniZinc-Modell \emph{N Factorial} über SICStus-Prolog. In der Übersetzung von MiniZinc in FlatZinc wird optimiert. Wegen der Optimierung können Variablen, die in MiniZinc definiert wurden, in FlatZinc weggelassen werden. Wir können diese Variablen aber beim Aufruf in SICStus-Prolog benötigen. Hier bietet sich die Option \emph{optimize(false} an, mit der dann nicht mehr optimiert wird und die Variablen deswegen nicht weggelassen werden (siehe Anhang~\ref{subsubsection:zebra_puzzle_minizinc_sicstus} für ein Beispiel im Modell \emph{Zebra Puzzle}) \cite{minizinc_sicstus}. Weiterhin wird auch das Prädikat \emph{fzn\_solve\slash1} verwendet. Dieses versucht, eine Lösung für die FlatZinc-Datei zu finden und sie dann anzuzeigen \cite{flatzinc_sicstus}.
\subsubsection*{FlatZinc}
Constraint-Solver arbeiten nicht direkt mit den MiniZinc-Modellen, sondern mit einer einfacheren Menge von MiniZinc, die FlatZinc genannt wird. MiniZinc-Modelle werden also in äquivalente FlatZinc-Modelle übersetzt.
Betrachten wir noch einmal das Beispiel von oben:
\begin{minted}[frame=single,linenos]{prolog}
var 1..3: X;
var 1..3: Y;
constraint X < Y;
solve satisfy;
\end{minted}
In diesem MiniZinc-Modell handelt es sich um lineare Constraints. Lineare Constraints haben die Form
Betrachten wir noch einmal das Beispiel~\ref{bsp:domaenenbestimmung_in_variablendefinition}. In diesem MiniZinc-Modell handelt es sich um lineare Constraints. Lineare Constraints haben die Form
\begin{center}
\begin{align*}
& = \\
......@@ -158,8 +156,9 @@ a_{1}x_{1} + ... + a_{n}x_{n} & \leq a_{0} \\
& <
\end{align*}
\end{center}
wobei $a_{i}$ Integer- oder Gleitkommakonstanten und $x_{i}$ Integer- oder Gleitkommavariablen sind. Der Übersetzer von MiniZinc nach FlatZinc versucht wiederum, einfachere äquivalente lineare Constraints zu erstellen \cite{FlatZinc}. Am Ende wird dieses MiniZinc-Modell in das folgende FlatZinc-Modell übersetzt:
wobei $a_{i}$ Integer- oder Gleitkommakonstanten und $x_{i}$ Integer- oder Gleitkommavariablen sind. Der Übersetzer von MiniZinc nach FlatZinc versucht wiederum, einfachere äquivalente lineare Constraints zu erstellen \cite{flatzinc}. Am Ende wird dieses MiniZinc-Modell in das FlatZinc-Modell wie in Beispiel~\ref{bsp:flatzinc_bsp} übersetzt.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
array [1..2] of int: X_INTRODUCED_0_ = [1,-1];
var 1..3: X:: output_var;
......@@ -167,11 +166,28 @@ var 1..3: Y:: output_var;
constraint int_lin_le(X_INTRODUCED_0_,[X,Y],-1);
solve satisfy;
\end{minted}
\caption{Das FlatZinc-Modell für das MiniZinc-Modell in Beispiel~\ref{bsp:minizinc_bsp}}
\label{bsp:flatzinc_bsp}
\end{beispiel}
int\_lin\_le ist ein eingebautes Prädikat in FlatZinc und funktioniert folgendermaßen:
\emph{int\_lin\_le} ist ein eingebautes Prädikat in FlatZinc und funktioniert folgendermaßen \cite{flatzinc_builtins}:
\begin{center}
int\_lin\_le(array [int] of int: array1, array[int] of var int: array2, int: a): \newline
$\sum$(array1[i] $\cdot$ array2[i]) $\leq$ a
\end{center}
In Beispiel~\ref{bsp:flatzin_bsp} ist Zeile 4 also gleich
\begin{center}
\begin{align*}
1 \cdot X + (-1) \cdot Y &\leq -1 \\
X + 1 &\leq Y \\
X &< Y
\end{align*}
\end{center}
In MiniZinc werden mehrere Solver verwendet, zum Beispiel Gecode, findMUS und Chuffed. Gecode 3.6.0 ist der Standard-Solver und wird in dieser Arbeit für alle MiniZinc-Modell verwendet.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment