Logical
Wenn ich mit dem Zug fahre vergeht die Zeit am schnellsten wenn ich versuche Rätsel zu lösen. Dann investiere ich mein Geld in den P. M. Logik Trainer1, nehme mir sehr viel vor und es endet meist damit, dass das erste Rätsel mich so lang beschäftigt dass ich zu keinem Weiteren komme. Manchmal sind die Rätsel auch so schwierig, dass ich keine Lösung finde. Also bleibt das gekaufte Heft immer zum größten Teil unausgefüllt. Weihnachten 2023 packte mich der Ehrgeiz und ich wollte in einer ruhigen Stunde, ein sogenanntes Logical lösen, das zuvor auf einer Zugfahrt ungelöst blieb. Doch obwohl Weihnachten ein Fest der Liebe ist, wurde es ob dieses Logicals beinahe ein Fest des Hasses, denn es wollte sich nicht lösen lassen obwohl ich bereits mehr als 10 Minuten investiert hatte.
Es ungelöst zu lassen war keine Option. Also musste ich mit dem schweren Werkzeug ran. Ich kramte in meinem Gedächtnis und in meinen Ordnern um mich an die Tools zu erinnern mit denen ich im Studium zu tun hatte. Spoileralarm: Diese Tools brachten mich nicht zum Erfolg – dafür durfte ich was neues lernen!
Das Problem
Das zu lösende Problem sieht folgendermaßen aus: Es werden beliebige Wörter, in diesem Fall Namen von Bands genannt. Jedes Wort ist einer Zahl zugeordnet. Diese Zahl bezeichnet die Summe der Buchstabenwerte. Also z. B. wissen wir laut nebenstehender Tabelle, dass A + C + D + C = 45
. Ziel ist es, die Buchstabenwerte herauszufinden. Die einzigen bekannten Informationen sind:
- Die Summe der Buchstaben jedes Wortes
- Jedem Buchstaben ist genau eine Zahl zwischen 1 und 26 zugeordnet.
- Zwei Buchstaben haben nie dieselbe Zahl – also es werden für 26 Buchstaben alle Zahlen von 1-26 zugeordnet.
Normalerweise beginnt man nun damit bei Wörtern die es einem leicht machen einzelne Buchstabenwerte zu identifizieren. Das können möglichst kurze Wörter sein, oder auch Wörter mit besonders niedrigen Buchstabensummen. Oft gibt es dazu eine Einstiegshilfe, in Form eines Hinweises, welches Wort sich besonders gut eignet.
Die Suche
Das klingt alles sehr mühsam – und ok, wenn man es dann gelöst hat stellt sich eine gewisse Zufriedenheit ein. Aber auf dem Weg dorthin erlebt man zahlreiche Frustrationen. Ich weiß nicht wie es euch geht, aber in meiner Freizeit lasse ich mich ungern frustrieren. Man will aber das Problem ja auch nicht ungelöst im Heft lassen. Wobei das wirkliche Problem ja nicht der “Ungelöst” Status des Problems ist, sondern vielmehr dass man es probiert hat um dann zu dem Schluss zu kommen es “aus persönlichen Gründen” doch nicht zu lösen. Das Problem wird zum Problem. Es prangt regelrecht wie ein frisch errichtetes Denkmal des eigenen Scheiterns. Selbst wenn das Heft geschlossen auf dem Tisch liegt, dringt es hindurch und erinnert uns an das eigene Unvermögen. Die Denkmalhaftigkeit hat sich inzwischen auch auf das gesamte Heft übertragen und droht omnipräsent zu werden und uns bis ins Mark zu erschüttern. Daher bleibt uns nur eine Option: Unseren gottverdammten Job zu tun und das Rätsel zu lösen auch wenn wir uns dafür (ein bissi) mit Python auseinandersetzen müssen.
Ich begann damit, in altem Wissen zu kramen aus längst vergangenen Tagen, als ich mich (im Studium) noch mit Dingen wie Integer Programming beschäftigen durfte. Das war unterhaltsam. Die Tools schienen mächtig, als könnten sie alle Probleme der Welt lösen wenn man ihnen nur genügend Zeit ließe. Ich googlete nach den neuesten Informationen zu SCIP und ZIMPL. Das war die erste Station. Und es war keine gute Station. Auf der Achterbahnfahrt durch den kleinen Optimierungs-Horrorladen gab es noch einige weitere Stationen wie z. B. das ompr
package, das mir einfach bei meinem Problem nicht helfen konnte. Ich bin sicher, dass es viele Menschen gibt die dieses Package mit Freude verwenden, wo es gute Ergebnisse liefert und alle glücklich macht. Doch “Ungleich” Bedingungen werden von diesen Software Paketen allen gleichermaßen gehasst.
Um einmal im Detail darzustellen wonach man eigentlich sucht, definieren wir im nächsten Abschnitt die Nebenbedingungen.
Buchstabensumme
Die erste Nebenbedingung ist die offensichtlichste, da sie explizit gegeben ist. Wie schon oben beschrieben ist jeweils die Summe der Buchstabe der einzelnen Wörter gegeben. Man kann sich das ganze auch als eine Matrix vorstellen: Jede Spalte stellt einen Buchstaben dar (wie unten in der \(n \times l\) Matrix). Die erste Spalte steht für den Buchstaben a die zweite Spalte für b und so weiter. Beim ersten Wort ACDC sehen wir eine 1 in der ersten Spalte (A), eine 2 in der dritten Spalte (C) und wieder eine 1 in der vierten Spalte (D) \(\rightarrow\) zusammen ACDC2. Jede Zeile stellt ein Wort, in diesem konkreten Fall eine Band dar. D. h. wir haben n Wörter und l Buchstaben3. Multipliziert wird diese Matrix mit einem Vektor \(\vec{\theta}\). Dieser beinhalten das was man wissen will: die Werte der einzelnen Buchstaben. \(\theta_a\) ist der Wert den Buchtabe a hat. Die Werte kennen wir nicht. Das ultimative Ziel ist es sie zu ermitteln. Wenn wir die \(n \times l\) Matrix mit \(\vec{\theta}\) multiplizieren, muss die vorgegeben Summe rauskommen. Das sind genau die Summen die im Logical vorgegeben sind: Für ACDC z. B. 45. Das schaut alles mega kompliziert aus. Das ist aber noch die netteste Nebenbedngung. Die kann ich auch an SCIP
und Freunde verfüttern. Aber die kommende Nebenbedingung ist schon schwieriger umzusetzen4.
\[\begin{align} \begin{bmatrix} 1 & 0 & 2 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 1 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 1 & 0 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 0 & 0 & 0 & 1 & 3 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 1 & 0 & 0 & 1 & 1 & 0 & 0 & 0 & 2 & 0 & \ldots \\ \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \\ \end{bmatrix} _{n \times l} \times \quad \begin{bmatrix} \theta_a \\ \theta_b \\ \theta_c \\ \theta_d \\ \theta_e \\ \vdots \end{bmatrix}_{l \times 1} = \quad \begin{bmatrix} 45 \\ 52 \\ 62 \\ 27 \\ 82 \\ \vdots \end{bmatrix}_{l \times 1} \end{align}\]
Verschiedene Elemente
Wenn man sich obenstehende Tabelle ansieht, dann merkt man, dass man 26 Buchstaben hat, aber nur 20 Nebenbedingungen. Daher kann das nicht alles sein. Es darf nicht alles sein, wenn wir das hier lösen wollen. Die implizite Nebenbedingung ist, dass jeder Buchstabe eine eigene Zahl zwischen 1 und 26 bekommen soll. Keine zwei Elemente dürfen ident sein. Also etwas formeller angeschrieben sieht das ca. so aus:
\[\begin{align} 1 \leq \theta_i \leq 26, & \quad i = a, b, \ldots, z, \\ \theta_i \neq \theta_j, & \quad \forall i, j \in \{a, b, \ldots, z\}, i \neq j. \end{align}\]
Diese Art von Nebenbedingungen sind nicht einfach zu implementieren wenn versucht sie mit den zuvor erwähnten Tools zu lösen. Nach viel Herumprobieren, schlaflosen Nächten und kurz vor dem Meltdown half mir der sanfter Hinweis eines guten Freundes: Es war eine Sackgasse und ich musste irgendwas mit Python machen. Es traf mich mitten ins Herz. Musste ich wirklich Python verwenden? Er schickte mir seine Lösung und empfahl mir die Google OR-Tools zu verwenden wenn ich das Problem lösen will.
Also begann ich mit Python und den OR-Tools.
OR-Tools
Der Witz ist, dass sich dieses Problem mit Constraint Optimization sehr effizient lösen lässt. In unserem Beispiel haben wir nicht mal eine Zielfunktion. Wir wollen einfach eine Lösung die alle Nebenbedingungen erfüllt, und gehen davon aus, dass es nur eine Lösung gibt \(\rightarrow\) fertig. Hier ist ein einfacheres Beispiel dazu. Dem Solver von ortools
mitzuteilen, dass jeder Buchstabe einer anderen Zahl zugeordnet werden soll, ist besonders einfach und ist unten im Python Code Block zu sehen: model.AddAllDifferent(intvars)
. Das ist alles. Keine Tricks, keine Schleife die alle Variabenpaare ungleich setzen muss, einfach dieses Statement und der shit happened einfach so, als wäre es das einfachste der Welt. Das Ganze hab ich in 2 Funktionen gegossen. Wer sich diese im Detail ansehen will, bittesehr – einfach unfolden:
Show the code
from ortools.sat.python import cp_model
import pandas as pd
import numpy as np
import string
import os
## Funktion um die Matrix zu erstellen
def create_letter_matrix(word_sum):
#word_sum = pd.read_excel(word_sum_file)
# es wird eine lettermatrix erstellt.
# zeilen sind die NB, spalten sind die Buchstaben
= word_sum.shape[0]
anz_zeilen = np.zeros((anz_zeilen,26),dtype=int)
letter_matrix
# letter zu pos. DataFrame
= pd.DataFrame({
letter_pos 'position': range(0, 26),
'buchstaben': list(string.ascii_lowercase)
})
# matrix befuellen
= word_sum["words"].apply(lambda x: x.replace(" ", "").lower()).tolist()
woerter for zei, val in enumerate(woerter):
for i, letval in enumerate(val):
= letter_pos[letter_pos["buchstaben"] == letval]["position"]
pos_spalte if not pos_spalte.empty: # das kam von chatGPT
0]] += int(1)
letter_matrix[zei,pos_spalte.iloc[
return letter_matrix
## Funktion um das Ganze zu solven
def solve_logical(word_sum_file = "word_sum_input.csv", outfile = "loesung.csv"):
# word sum - hier sind die wörter plus die summen drinnen!
#word_pd = pd.read_excel(word_sum_file)
= pd.read_csv(word_sum_file)
word_pd = word_pd["letter_sum"].tolist()
wordsum = list(string.ascii_lowercase)
letters
# eine matrix wird erstellt, wie haeufig jeder buchstabe in einem wort vorkommt
= create_letter_matrix(word_sum = word_pd)
letter_matrix
# optimieren
= cp_model.CpModel()
model
= np.array([])
intvars for i, val in enumerate(letters):
= np.append(intvars, model.NewIntVar(1, 26, val))
intvars
# alle muessen unterschiedlich sein
model.AddAllDifferent(intvars)
# nebenbedingungen - summe der buchstaben der woerter als matrixmultiplikation
= letter_matrix @ intvars
res_sum
for i, val in enumerate(res_sum):
== wordsum[i])
model.Add(val
= cp_model.CpSolver()
solver = solver.Solve(model)
status
# rausspeichern
= []
res_dat for i in intvars:
res_dat.append(solver.Value(i))
= pd.DataFrame({'Buchstabe': letters, 'value': res_dat})
loesung
= {"Loesung": [loesung.columns.tolist()] + loesung.values.tolist()}
data
loesung.to_csv(outfile)
return data
Nicht jeder hat jetzt vielleicht die Lust Python zu installieren bzw. die notwendigen Packages, will aber trotzdem das Beispiel ausprobieren bzw. sein eigenes Logical lösen. Dazu kommen wir im nächsten Abschnitt!
Die Lösung
Um das Problem zu lösen brauchen wir mal ein Inputfile.
Dann brauchen wir 2 Funktionen:
- Eine Funktion die aus den Wörtern eine Matrix macht wie oben gezeigt
- Eine Funktion die die Nebenbedingungen formuliert und die Lösung errechnet
Das alles soll “Out of the box” funktionieren – daher verwenden wir ein, genau für diesen Zweck erstelltes, Docker Image. Es beinhaltet die Python Funktionen und kann wie folgt aufgerufen werden. Wichtig ist, dass Docker am Computer installiert ist!
Terminal
# eventuell muss vor jeden Befehl ein sudo
# pull image
docker pull seebaer/logical-python
# check: es sollte das gerade gepullte image aufgelistet sein
docker image ls
# word_sum_input.csv wird an docker übergeben
docker run -v /home/USER/logical:/data seebaer/logical-python python logical_python_functions.py --word_sum_file /data/word_sum_input.csv --outfile /data/result.csv
Was passiert hier?
- Es wird ein Docker image von Docker Hub gezogen (
docker pull ...
). Dieses Image wurde speziell für diesen Zweck gebaut. Es beinhaltet ein minimales Linux, Python und die Python Funktionen die notwendig sind um das Problem zu lösen. - Wenn das Image am Computer ist (Kontrolle mit:
docker image ls
) kann man es laufen lassen.docker run
lässt das gerade gezogene image laufen (seebaer/logical-python
)-v /home/USER/logical:/data
mounted mein Verzeichnis/home/USER/logical
(in diesem Verzeichnis muss sich die Datei:word_sum_input.csv
befinden!!) in das Verzeichnis des docker container/data
.- Ausgeführt wird das Skript das sich im Container befindet:
python logical_python_functions.py
- Input ist eben das .csv file:
--word_sum_file /data/word_sum_input.csv
das in/data
liegt, also bei uns in/home/USER/logical
5 - Wohin soll der Output gespeichert werden und wie soll der output heißen? Das wird hier angegeben:
--outfile /data/loesung_docker.csv
Damit wurde das Problem gelöst. Der Output ist ein .csv mit den Buchstaben und den jeweiligen Werten wie in der Tabelle nebenan zu sehen ist. Im Hintergrund erklingt fröhliche Schlussmusik. Es hat lang gedauert. Es wäre wohl schneller gewesen hätte ich es per Hand gelöst. Dafür hab kann nun jeder in Zukunft Probleme dieser Art im Handumdrehen lösen: Dank Python und Docker.
Optimierungsergebnis vom Optimierungserlebnis
Footnotes
Ich werde (leider) nicht gesponsert von P. M.!↩︎
Oder ACCD – beim Summieren ist die Reihenfolge ja völlig egal.↩︎
Das sind immer 26 Buchstaben. Also könnte man auch 26 schreiben. Aber mit l schaut es viel cooler aus.↩︎
Vor allem wenn man eben ein Tool verwendet, das man eigentlich für ein solches Problem nicht verwenden sollte.↩︎
Oder in einem anderen beliebigen Verzeichnis!↩︎