Logische Programmierung
Neulich stolperte ich mal wieder über eine Knobelaufgabe und fragte mich, ob es eigentlich einen „mathematischen“ Lösungsansatz gibt? Dazu folgendes Rätsel…
Geschenke im Advent
Die Kinder Anna, Ben, Clara und Daniel sind in einer Kindergartengruppe. Eigentlich ist die Gruppe viel größer, aber der Rest der Kinder ist den ganzen Dezember zu Hause mit Rüsselseuche. Während der Adventszeit erhält jedes Kind an einem Tag ein Geschenk. Da nur 4 Kinder übrig sind, gibt es dieses Jahr auch nur 4 Geschenke (Auto, Buch, Puzzle, Schokolade) an den 4 Tagen vor Weihnachten (Montag, Dienstag, Mittwoch, Donnerstag).
Anna bekommt ihr Geschenk nicht am Montag und nicht die Schokolade, da sie sowieso schon übergewichtig ist. Da Ben immer quängelt, bekommt er sein Geschenk einen Tag früher als das Kind, das das Puzzle erhält. Das Auto wird am Dienstag verschenkt. Das Buch wird einen Tag nach dem Auto verschenkt. Clara bekommt ihr Geschenk nach Ben.
An welchem Tag bekommt welches Kind welches Geschenk?
Naiver Lösungsansatz
Bis jetzt habe ich solche Knobelaufgaben immer mit „Denken“ aber ohne echte Strategie gelöst. Meine Vermutung ist, dass man doch die gesamten Bedingungen irgendwie mit Aussagenkalkür oder logischer Algebra darstellen können müsste und es dann sicher clevere Formeln gibt, um diese zu lösen?! So einfach scheint es dann aber doch nicht zu sein.
Eine längere Recherche führte mich dann in das Rabbit Hole Constraint-Satisfaction-Problem (CSP). Programme, die solch ein Problem lösen können, nennt man Solver. Ein Solver nutzt eine Kombination aus
- Lösungssuche und
- Schlussfolgerung,
um eine Lösung zu finden.
Am obigen Beispiel: Da das Auto am Dienstag verschenkt wird, kann man sofort alle anderen Lösungen streichen, an denen das Auto an einem anderen Tag verschenkt wird. Damit reduziert sich die Lösungssuche erheblich.
Anschließend fixiert der Solver einen Wert, etwa Anna bekommt ihr Geschenk am Montag, und probiert dann weiter, ob dies später zu einem Widerspruch führt. Falls ja, geht er schrittweise zurück und probiert andere Werte aus (d.h. typisches Backtracking).
Logische Programmierung mit MiniZinc
Natürlich gibt es auch passende Software und Programmiersprachen, um solche Probleme auszudrücken. Eine alte aber sehr bekannte Sprache ist Prolog. Da ich aber nicht alt sein will, habe ich stattdessen die Programmiersprache und Entwicklungsumgebung MiniZinc verwendet.
Im Download Paket ist sowohl die MiniZinc IDE, der zugehörige Compiler als auch eine Auswahl von Solvern enthalten. Hier zunächst der Programmcode für das Beispiel:
enum Kind = { Anna, Ben, Clara, Daniel };
enum Geschenk = { Auto, Buch, Puzzle, Schokolade };
enum Wochentag = { Montag, Dienstag, Mittwoch, Donnerstag };
array[Kind] of var Geschenk: geschenk_von;
array[Kind] of var Wochentag: tag_von;
% --- Bedingungen ---
% Da jedes Geschenk und jeder Tag nur einmal vorkommt:
include "alldifferent.mzn";
constraint alldifferent(geschenk_von);
constraint alldifferent(tag_von);
% Anna bekommt ihr Geschenk nicht am Montag und nicht die Schokolade.
constraint geschenk_von[Anna] != Schokolade;
constraint tag_von[Anna] != Montag;
% Ben bekommt sein Geschenk einen Tag früher als das Kind, das das Puzzle erhält.
var Kind: puzzle_kind;
constraint geschenk_von[puzzle_kind] = Puzzle;
constraint enum2int(tag_von[Ben]) + 1 = enum2int(tag_von[puzzle_kind]);
% Das Auto wird am Dienstag verschenkt.
var Kind: malbuch_kind;
constraint geschenk_von[malbuch_kind] = Auto;
constraint tag_von[malbuch_kind] = Dienstag;
% Das Buch wird einen Tag nach dem Auto verschenkt.
var Kind: buch_kind;
constraint geschenk_von[buch_kind] = Buch;
constraint tag_von[buch_kind] = Mittwoch;
% Clara bekommt ihr Geschenk nach Ben.
constraint enum2int(tag_von[Clara]) > enum2int(tag_von[Ben]);
% Lösen und Ausgeben
solve satisfy;
output [ "\(k): \(geschenk_von[k]) am \(tag_von[k])\n" | k in Kind ];
Code-Sprache: Prolog (prolog)
Der Compiler überführt diesen MiniZinc Code in eine einfachere Darstellung namens FlatZinc. Dieses Format können dann verschiedene Solver verarbeiten.
In Zeile 1 bis 3 definiere ich die Welt bzw. Begriffsmengen, mit denen ich arbeiten möchte. Für mich sind die Begriffe Kind, Geschenk und Wochentag mit ihren jeweiligen Ausprägungen wichtig.
Danach folgen die Entscheidungsvariablen in den Zeilen 5 und 6. Ich benötige eine Entscheidung für
- welches Kind welches Geschenk bekommt und
- an welchem Tag welches Kind ein Geschenk bekommt.
Dann folgt die Liste der Bedingungen. Die letzten beiden Zeilen rufen den Solver auf und geben die gefundenen Lösungen aus.
Falls der geneigte Leser selbst noch knobbeln möchte, dann nicht weiter scrollen!
Die Lösung für das Rätsel
- Anna: Auto am Dienstag
- Ben: Buch am Mittwoch
- Clara: Puzzle am Donnerstag
- Daniel: Schokolade am Montag