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

Replace hintergrundwissen.tex

parent 3b459f70
\section{Hintergrundwissen}
\label{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.
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}. In dieser Arbeit wird die logische Programmierung gebraucht. Die logische Programmierung wurde unter Anderem aus dem Versuch entwickelt, logische Theoreme mithilfe der Maschine zu beweisen. Zum Beispiel zu beweisen, dass $X \rightarrow Z$ aus den logischen Axiomen $X \rightarrow Y$ und $Y \rightarrow Z$ folgt. Es können aber auch Probleme aus anderen Bereichen als Theoreme betrachten werden, wie arithmetische Aufgaben und 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}
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).
Die logische Programmiersprache Prolog wurde vom französischen Informatiker Alain Colmerauer entwickelt und ist das Resultat eines Projektes, dessen Ziel es eigentlich war, mit der Maschine 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}.
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}.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
......@@ -20,7 +20,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). 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:
In Beispiel~\ref{bsp:prolog_bsp} haben wir zwei Fakten in den ersten zwei 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, sodass X ein Elternteil von Y (Zeile 5) und Y ein Elternteil von Z ist (Zeile 6). Es ist zu beachten, dass die Namen der Fakten und der Regeln kleingeschrieben und die Variablennamen dagegen großgeschrieben werden. Nun können wir Anfragen an das System stellen. 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 für diese Variablen, falls es Lösungen gefunden hat:
\begin{itemize}
\item Anfrage: elternteil(alena, christoph) \newline
......@@ -31,20 +31,7 @@ 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}
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}
entspricht der Horn-Klausel
\begin{center}
\emph{X $\lor$ $\neg$Y $\lor$ $\neg$ Z}.
\end{center}
In Beispiel~\ref{bsp:prolog_bsp} haben wir 3 Horn-Klauseln:
Prolog basiert auf dem Prinzip der Resolution, in dem Horn-Klauseln gebraucht werden. 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 Prolog-Regel der Form \emph{X :- Y, Z}entspricht der Horn-Klausel \emph{X $\lor$ $\neg$Y $\lor$ $\neg$ Z}. In Beispiel~\ref{bsp:prolog_bsp} haben wir zum Beispiel drei Horn-Klauseln:
\begin{enumerate}
\item elternteil(alena, christoph)
......@@ -52,40 +39,17 @@ In Beispiel~\ref{bsp:prolog_bsp} haben wir 3 Horn-Klauseln:
\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}.
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 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.
Anfragen, die vom Benutzer an einen Prolog-Interpreter geschickt werden, werden negiert. Dann wird versucht, mittels Resolution zu einem Widerspruch zu führen, sodass die initiale Anfrage bewiesen ist. Wenn eine Anfrage also an den Prolog-Interpreter geschickt wird, 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 im Programm zu suchen, 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}
Somit haben wir einen Widerspruch gefunden. Die Antwort auf die Anfrage \emph{elternteil(alena, christoph)} ist also \emph{true}. Würden wir für die Anfrage keinen Widerspruch mit den Formeln im Programm finden, so ist die Antwort \emph{False}.
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, sodass 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 \emph{$\neg$elternteil(alena, christoph)} $\wedge$ \emph{elternteil(alena, christoph)} $\Rightarrow$ $\Box$. Somit haben wir einen Widerspruch gefunden. Die Antwort auf die Anfrage \emph{elternteil(alena, christoph)} ist also \emph{true}. Würden wir für die Anfrage keinen Widerspruch mit den Formeln im Programm finden, so ist die Antwort \emph{false}.
\subsubsection{CLP(FD)}
In Prolog gibt es eingebaute Prädikate für Integer-Werte wie \emph{is/2}, \emph{</2}, \emph{>/2} und \emph{=:=/2}. Diese Prädikate sind beschränkt. Betrachten wir zum Beispiel das Prädikat \emph{is/2}. Damit wird einer Variable ein Wert zugewiesen:
\begin{center}
Y is 1 + 2
\end{center}
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}
\end{center}
In Prolog gibt es eingebaute Prädikate für Integer-Werte wie \emph{is/2}, \emph{</2}, \emph{>/2} und \emph{=:=/2}. Diese Prädikate sind beschränkt. Betrachten wir zum Beispiel das Prädikat \emph{is/2}. Damit wird einer Variable ein Wert zugewiesen, zum Beispiel $Y$ is $1 + 2$. In diesem Fall erhält die Variable $Y$ den Wert $3$. Wie es zu sehen ist, steht auf der linken Seite von \emph{is} eine Variable (in diesem Beispiel die Variable $Y$) und auf der rechten Seite von \emph{is} arithmetische Ausdrücke (in diesem Beispiel $1 + 2$). Dies ist die einzige Anordnung von \emph{is}. Das bedeutet, dass keine Argumente auf der rechten Seite von \emph{is} erlaubt sind, die teilweise oder gar nicht initialisiert sind, wie zum Beispiel in $3$ is Y $+ 2$. Diese Anfrage erzeugt einen Fehler, da $Y$ auf der rechten Seite von $is$ nicht initialisiert ist. 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 also das Prädikat \emph{is/2} durch ein arithmetisches Constraint ersetzen, in diesem Fall \emph{\#=/2}, das in allen Richtungen funktioniert, wie zum Beispiel in
$3$ \#= $Y + 2$. Hier erhalten wir 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.
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) 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}.
Jede Variable in CLP(FD) hat einen Domänenbereich. Anfangs entsprechen 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,18 +61,18 @@ first_clpfd_model(X,Y) :-
X #< Y,
labeling([], [X,Y]).
\end{minted}
\caption{Ein CLP(FD)-Beispiel}
\caption{Ein erstes Modell in CLP(FD)}
\label{bsp:clpfd_bsp}
\end{beispiel}
In Beispiel~\ref{bsp:clpfd_bsp} definieren wir 2 Variablen $X$ und $Y$. Diesen Variablen wird mithilfe von \emph{in/2} der Bereich $[1,3]$ zugewiesen. Mit $X$ $\#<$ $Y$ wird der Bereich von $X$ auf $[1,2]$ und der Bereich von $Y$ auf $[2,3]$ reduziert, da es gelten soll, dass $X$ kleiner als $Y$ ist.
In Beispiel~\ref{bsp:clpfd_bsp} definieren wir zwei Variablen $X$ und $Y$. Diesen Variablen wird mithilfe von \emph{in/2} die Domäne $[1,3]$ zugewiesen. Mit $X$ $\#<$ $Y$ wird die Domäne von $X$ auf $[1,2]$ und die Domäne von $Y$ auf $[2,3]$ reduziert, da es gelten soll, dass $X$ kleiner als $Y$ ist.
Bis jetzt erhalten wir Domänen als Lösungen für unsere Variablen. Mit \emph{labeling} können dann einzelne Lösungen generiert werden, nämlich $X = 1$, $Y = 2$ oder $X = 1$, $Y = 3$ oder $X = 2$ und $Y = 3$.
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.
Es ist zu beachten, dass die Bibliothek \emph{clpfd} eingefügt werden soll, damit auf die CLP(FD)-Constraints zugegriffen werden kann, wie in Beispiel~\ref{bsp:clpfd_bsp} zu sehen ist. Weiterhin ist es zu beachten, dass CLP(FD) auf 59 Bits beschränkt ist.
\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.
Zusätzlich zu Constraint Logic Programming können auch Coroutinen in Prolog verwendet werden, um die Ausführung eines Prädikats zu verzögern, bis vorher definierte Argumente keine Variablen mehr sind. Unter Anderem werden Blockdeklarationen angeboten, die in Kapitel~\ref{subsection:kapitel_3_minimales_k_dominating_set} (\emph{Minimales K Dominating Set}) verwendet werden. In Beispiel~\ref{bsp:block_deklarationen} wird das Prädikat \emph{sum\slash3} implementiert, das zwei Zahlen erhält und ihre Summe mithilfe von \emph{is} berechnet und zurückgibt. Vor diesem Prädikat wird eine Blockdeklaration implementiert, die die Ausführung blockiert, wenn das erste Argument im Prädikat \emph{sum\slash3} eine Variable ist. Der Strich in der Blockdefinition bedeutet also, dass die Ausführung blockiert werden soll, wenn eine Variable kommt, und das Fragezeichen bedeutet, dass Variablen erluabt sind. Wenn wir das Prädikat nun mit \emph{sum(A, 2, B)} aufrufen, dann wird die Ausführung 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 die Blockdeklaration würden wir wegen \emph{is} in Zeile 3 im Beispiel immer eine Fehlermeldung erhalten, da die rechte Seite von \emph{is} die Variable $A$ enthält. Mit der Blockdeklaration 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 jetzt \emph{sum(3, 2, B)}) ausgeführt werden.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
......@@ -116,16 +80,16 @@ Zusätzlich zu Constraint Logic Programming können Coroutinen in Prolog verwend
sum(A, B, AB) :-
AB is A + B.
\end{minted}
\caption{Coroutenen: Ein Beispiel von Block Declarations}
\label{bsp:coroutenen}
\caption{Ein Beispiel von Blockdeklarationen}
\label{bsp:block_deklarationen}
\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}.
MiniZinc ist eine Open-Source Sprache zur Spezifizierung von Constraint-Optimierungs- und Constraint-Entscheidungsproblemen über Integer und reelle Zahlen \cite{minizinc_introduction}.
Bei Constrained-Entscheidungsproblemen wird geschaut, ob eine Lösung für bestimme Variablen existiert, die gegebene Constraints erfüllt. Zum Beispiel haben wir die Variablen $x,y \in \mathbb{R}$ und die Constraints $x \in [1,3]$, $y = 2$ und $x > y$. In diesem Fall existiert eine Lösung: $x = 3$, $y = 2$. Würden wir jedoch $y$ auf beispielsweise $5$ setzen, dann würde keine Lösung mehr existieren, da $x > y$ dann nicht mehr erfüllt werden könnte.
Bei Constraint-Entscheidungsproblemen wird geschaut, ob eine Lösung für bestimme Variablen existiert, die gegebene Constraints erfüllt. Zum Beispiel haben wir die Variablen $x,y \in \mathbb{N}$ und die Constraints $x \in [1,3]$, $y = 2$ und $x > y$. In diesem Fall existiert eine Lösung, nämlich $x = 3$, $y = 2$. Würden wir jedoch $y$ auf beispielsweise $5$ setzen, dann würde keine Lösung mehr existieren, da $x > y$ dann nicht mehr erfüllt werden könnte.
Andererseits wird bei Constrained-Optimierungsproblemen nach einer Lösung für bestimmte Variablen mit Rücksicht auf gegebene Constraints gesucht, wobei diese Lösung maximiert beziehungsweise minimiert werden soll \cite{constrained_optimization}. Wir betrachten beispielsweise die Variablen $x,y \in \mathbb{R}$, wobei die Summe $x + y$ maximiert werden soll und wir folgende Constraints haben: $x \in [1,3]$, $y \in [1,4]$ und $x > y$. Die Lösung ist dann: $x = 3$, $y = 2$.
Andererseits wird bei Constraint-Optimierungsproblemen nach einer Lösung für bestimmte Variablen mit Rücksicht auf gegebene Constraints gesucht, wobei diese Lösung maximiert beziehungsweise minimiert werden soll \cite{constrained_optimization}. Wir betrachten beispielsweise die Variablen $x,y \in \mathbb{N}$, wobei die Summe $x + y$ maximiert werden soll und wir folgende Constraints haben: $x \in [1,3]$, $y \in [1,4]$ und $x > y$. Die Lösung ist dann $x = 3$, $y = 2$.
MiniZinc-Modelle können so ähnlich wie mathematische Formulierungen der Probleme geschrieben werden, da MiniZinc bekannte mathematische Notationen wie Existenzquantor, Allquantor und Summenzeichen auf eigene Weise zur Verfügung stellt. Außerdem stellt MiniZinc auch logische Verknüpfungen wie Konjunktion, Disjunktion, Implikation, Äquivalenz und auch if-then-else-Anweisungen zur Verfügung \cite{minizinc_introduction}.
......@@ -138,32 +102,16 @@ constraint X < Y;
solve satisfy;
\end{minted}
\caption{Ein MiniZinc-Beispiel}
\caption{Ein erstes Modell in MiniZinc}
\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 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.
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}.
In MiniZinc muss nicht wie in Prolog auf Groß- und Kleinschreibung geachtet werden, da Variablen in MiniZinc durch \emph{var} kennzeichnet werden. Da wir jedoch die MiniZinc-Modelle über SICStus-Prolog durch Prädikate, die großgeschriebene Variablen als Parameter übergeben bekommen, aufrufen wollen, müssen die Variablennamen in den MiniZinc-Modellen kleingeschrieben werden. Sonst kann der Prolog-Interpreter, zum Beispiel im folgenden Prädikat, nicht zwischen den Variablen unterscheiden:
\begin{minted}[frame=single,linenos]{prolog}
:- use_module(library(zinc)).
n_factorial_minizinc(N, Factorial) :-
mzn_load_file('n_factorial.mzn',
[parameters([N=N]),variables([Factorial=Factorial])],
FznState),
fzn_solve(FznState).
\end{minted}
Deswegen sind die Deklarationen in MiniZinc-N-Factorial sowie in allen anderen MiniZinc-Modellen kleingeschrieben, wie in Anhang~\ref{appendix:implementierungen_clpfd_und_minizinc} zu sehen ist.
In Beispiel~\ref{bsp:minizinc_bsp} ist die Implementierung von Beispiel~\ref{bsp:clpfd_bsp} in MiniZinc zu finden. Wir definieren wieder die zwei Variablen $X$ und $Y$, deren Werte im Bereich $[1,3]$ liegen. Dann wird die Einschränkung (das Constraint) implementiert, dass $X < Y$ sein soll. Mit \emph{solve satisfy} wird dann nach möglichen Lösungen für dieses 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 $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$ vor dem Ausführen des Programms feste Werte zuweisen.
\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~\ref{bsp:domaenenbestimmung_in_variablendefinition}. In diesem MiniZinc-Modell handelt es sich um lineare Constraints. Lineare Constraints haben die Form
Betrachten wir noch einmal Beispiel~\ref{bsp:minizinc_bsp}. In diesem MiniZinc-Modell handelt es sich um lineare Constraints. Lineare Constraints haben die Form
\begin{center}
\begin{align*}
& = \\
......@@ -171,7 +119,7 @@ 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 FlatZinc-Modell wie in Beispiel~\ref{bsp:flatzinc_bsp} ü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 in Beispiel~\ref{bsp:flatzinc_bsp} übersetzt.
\begin{beispiel}
\begin{minted}[frame=single,linenos]{prolog}
......@@ -192,17 +140,13 @@ int\_lin\_le(array [int] of int: array1, array[int] of var int: array2, int: a):
$\sum$(array1[i] $\cdot$ array2[i]) $\leq$ a
\end{center}
In Beispiel~\ref{bsp:flatzin_bsp} ist Zeile 4 also gleich
In Beispiel~\ref{bsp:flatzinc_bsp} ist Zeile 4 also gleich $1 \cdot X + (-1) \cdot Y \leq -1 \Leftrightarrow X + 1 \leq Y \Leftrightarrow X < Y$.
\begin{center}
\begin{align*}
1 \cdot X + (-1) \cdot Y &\leq -1 \\
X + 1 &\leq Y \\
X &< Y
\end{align*}
\end{center}
Für MiniZinc gibt es mehrere Solver zur Verfügung wie Gecode, findMUS und Chuffed. In dieser Arbeit wird der Solver Gecode 3.6.0 für alle MiniZinc-Modelle verwendet.
MiniZinc-Modelle können zum Beispiel über die MiniZincIDE oder über SICStus-Prolog gelöst werden. In SICStus-Prolog werden dafür bestimmte Prädikate verwendet. Diese befinden sich in der Bibliothek \emph{zinc}. Das Prädikat \emph{mzn\_load\_file(+MznFile, +Options, -FznState)} erhält eine MiniZinc-Datei mit der Endung \emph{.mzn} und weitere Optionen und erzeugt eine äquivalente FlatZinc-Datei \emph{FznState}. Unter den Optionen sind \emph{parameters\slash1} und \emph{variables\slash1} zu finden. In \emph{parameters\slash1} können wir Parameter an die MiniZinc-Datei geben und mit \emph{variables\slash1} können wir Ausgaben von der FlatZinc-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 nach FlatZinc wird optional der generierte Code optimiert. Wegen der Optimierung können Variablen, die in MiniZinc definiert wurden, in FlatZinc weggelassen werden. Unter Umständen benötigen wir diese Variablen aber in SICStus-Prolog. Hier bietet sich die Option \emph{optimize(false)} an, mit der dann nicht mehr optimiert wird und die Variablen deswegen nicht weggelassen werden \cite{minizinc_sicstus} (siehe Anhang~\ref{subsubsection:zebra_puzzle_minizinc_sicstus} für ein Beispiel im Modell \emph{Zebra Puzzle}). 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}.
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.
In MiniZinc muss nicht wie in Prolog auf Groß- und Kleinschreibung geachtet werden, weil Variablen in MiniZinc, für die nach Lösungen gesucht werden soll, durch \emph{var} kennzeichnet werden. Da wir jedoch die MiniZinc-Modelle über SICStus-Prolog durch Prolog-Prädikate aufrufen wollen, die großgeschriebene Variablen als Parameter übergeben bekommen, müssen die Variablennamen in den MiniZinc-Modellen kleingeschrieben werden. Sonst kann der Prolog-Interpreter nicht erkennen, welche Variablen zu MiniZinc und welche zum Prädikat in SICStus-Prolog gehören. Deswegen sind die Deklarationen in allen anderen MiniZinc-Modellen, die im Rahmen dieser Arbeit implementiert wurden, kleingeschrieben, wie in Anhang~\ref{appendix:implementierungen_clpfd_und_minizinc} zu sehen ist.
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