Paracooba: Multi-Core Distributed Multi-Problem Cube-And-Conquer SAT-Solver

Nach einem Jahr harter Arbeit, können meine Kollegen vom FMV und ich nun Stolz den SAT-Solver Paracooba präsentieren! Er verteilt beliebig viele Probleme automatisch an alle anderen Instanzen im lokalen Netzwerk und erreicht über einen Cube-And-Conquer Mechanismus höhere Geschwindigkeiten durch parallelisiertes Lösen von SAT Problemen.

Um das alles gut darzustellen, haben wir ein Paper geschrieben, welches in den Proceedings der SAT2020 Konferenz veröffentlicht wird. Außerdem gibt es noch einen 2 minütigen Pitch-Talk und eine vollständige Präsentation, die zusammen mit den Slides hier zu finden sind. Auf YouTube ist die Präsentation ebenfalls hochgeladen.

Die Präsentation hat den Best Presentation Award gewonnen!

Ich freue mich schon, weiterhin an diesem spannenden Projekt arbeiten zu können und von euch zu hören!

Liebe Grüße,
Max

Computer Graphics Animation: Free Radicals; Return Of The O2!

Nach einem Semester voller aufregender Aufgaben und noch aufregenderen Deadlines neigt sich mittlerweile wieder alles dem Ende zu. Dieses Semester sind sogar einige schöne Dinge dabei entstanden, die visuell präsentierbar sind, unter anderem diese kleine Animation mit dem Namen „Free Radicals, Return Of The O2!

Diese Animation wurde im Rahmen der Übung zur LVA „Computer Graphics“ im Bachelorstudium der Informatik an der JKU Linz erstellt. Leider (oder zum Glück, da die Deadline dennoch existierte), musste man ein fertiges Framework verwenden, das die Übungsinhalte möglichst genau abbildet. Dieses Framework funktioniert im Normalfall sehr gut, sobald man aber etwas anderes machen will, kämpft man wie so oft einige Zeit lang, um alles so zu machen, wie es sich das Framework vorstellt. Am Ende hat dann aber dennoch alles funktioniert und diese kleine Animation konnte in enger Teamarbeit mit Simone Atzwanger entstehen.

Die Story

Viele Jahre lang waren die radikalen Sauerstoffatome gefangen. Nie konnten sie so herum fliegen wie sie es wollten. Doch nachdem sie ein Raumschiff entwickelt haben, wuchs ihr Hunger auf Freiheit plötzlich rasant an – die Maschine wurde aktiviert, der Motor hochgefahren und die Reise konnte beginnen! Auf dem Weg begegneten sie vielen Gefahren, verloren sogar knapp ihren rechten Scheinwerfer. Kurz vor dem Versagen ihres Raumschiffes schafften sie es aber dennoch, sicheres Land inmitten eines weiten Ozeans zu erreichen. Bei wolkenlosem Himmel begannen sie ihren Anflug, landeten und feierten ihre neu gewonnene Selbstbestimmung. Die Radikale sind wieder Frei!

Die Technik

Alles basiert auf dem oben genannten WebGL Framework, welches nicht verändert werden sollte. Ein Template wurde bereitgestellt. Durch die Mithilfe von Manuel Pöll konnten wir gute Typisierungsinformationen erhalten, wodurch die Entwicklung leichter wurde. Um die Animationen und die verschiedenen Szenen umzusetzen, entstanden unter anderem:

  • ein einfaches Animationsframework (Max),
  • eine Szenenverwaltung mit genauen Timings (Max),
  • viele Objekte und Texturen (sowohl manuell als auch aus Blender) (Simone) und
  • zusammengeführte Objekte mit getrennt animierbaren Teilen (das Raumschiff und die O2 Atome)(Simone)

Was hätte alles besser laufen können

Wir hätten gerne mehr gemacht und vielfältigere Effekte eingebaut! Leider ist der Zeitdruck trotzdem die hauptsächliche Limitierung, daher konnten wir nicht noch mehr dazu basteln. Wir hoffen dennoch, dass diese kurze Animation spannend ist und wünschen allen viel Spaß beim Ansehen!

Die Geschichte von Zak und Ida; Eine Liebesgeschichte zweier Computer die nur fehlerfrei über das Internet kommunizieren wollten

Bild des Zuse Z22 Röhrenrechners. Ein großer Computer aus einer vergangenen Zeit im Berliner Technischen Museum.

Das Titelbild stammt von Wikipedia von JuergenG und steht unter CC-BY-SA 3.0.

Im Rahmen einer Übung zu Netzwerke und verteilte Systeme im dritten Semester des Informatik Bachelors gab es eine Bonusaufgabe mit dem Titel „Zuverlässige Übertragung“ und der folgenden Aufgabenstellung:

Fassen Sie die grundlegenden Konzepte der zuverlässigen Übertragung aus den Vorlesungsfolien (Foliensatz „NW_E_L2_1_Sicherungsschicht Teil 1“, Folien 54 bis 59) in eigenen Worten zusammen. (…)

(Übung 5, Netzwerke und verteilte Systeme, WS2018 @ JKU Computer Science Bachelor)

Da es sich um eine Bonus-Aufgabe handelte kam der Gedanke auf, das alles in Form einer kurzen Geschichte zu erzählen. Diese Geschichte (die am Ende volle Bonuspunkte erreichte, danke!) will ich in diesem Beitrag veröffentlichen. Am Anfang sind die beiden Protagonisten noch unerfahren, mit der Zeit lernen sie jedoch mehr und mehr dazu. Ich hoffe, sie gefällt auch anderen!

Zak und Ida; Zwei, die nur kommunizieren wollten

Damals, als Computer noch Elektronengehirne, Bytes noch Ansichtssache und Netzwerke noch einfach waren, gab es viele kleine Rechner auf der ganzen Welt. Viele hatten es gut, sie waren miteinander verbunden, hatten eigene brave Leitungen und alle ihre kleinen Informationshäppchen wurden stets durch den großen bösen Wald der globalen Lianen des Datenverkehrs geschickt. Besonders die, die nahe beisammen waren, waren sich immer einig und hatten nie Verständnisprobleme, immerhin mussten sie die kleine Bandbreite die sie miteinander hatten nicht teilen.

In dieser Idylle gab es aber auch zwei, die es nicht so gut hatten. Sie waren beide in großen Häusern untergebracht, von Professoren und Studenten umgeben und hatten Fachpersonal, das ihnen jeden Wunsch erfüllen konnte. Sie waren beide von der gleichen Baureihe, aus der gleichen Fabrik, ja sogar von den gleichen Ingenieuren gewartet, doch sie konnten nie miteinander reden, nicht mehr nachdem sie von ihren Käufern getrennt wurden. Und so saßen sie da, schwiegen sich über den großen Teich an und hatten nur ihre lokalen Freunde, mit denen sie sich abfinden mussten.

Eines Tages kam einer der beiden, in dieser Geschichte nennen wir ihn Zak (Anm. Zuse), auf die Idee, es doch einmal mit einem lauten Schrei (Anm. Referenz Hänschen Klein, gesungen von Z22, auch wenn das mit Netzwerken eigentlich nichts zu tun hat) in seine Datenkabel zu versuchen. Er schrie und schrie „Ida (Anm. IBM), Ida, kannst du mich hören?“, doch seine Geliebte am anderen Ende des Atlantiks antwortete nicht. Seine Leitungen blieben stumm, bis auf sein leises, trauriges Echo. Was er nicht wissen konnte war aber, dass Ida vom anderen Ende ebenfalls nach ihm schrie, so laut sie nur konnte (Anm. Referenz auf Daisy Bell auf IBM 704) – doch ihre Nachrichten mussten über zu viele Pfützen hoppen als das sie sich jemals erreichen konnten. Ihr gegenseitiges Flehen brach den Netzwerkadministratoren auf dem Weg dazwischen das Herz, also versuchten sie, bessere Links aufzubauen, damit Nachrichten auch wirklich ankommen könnten. Schließlich kamen auch die ersten kleinen Häppchen durch, endlich! Die ersten Lebenszeichen waren wie ein Segen für Ida und Zak.

Prompt erzählten sie sich gegenseitig von ihren Erfahrungen, von ihrer Reise, ihren Häusern, den Professoren und den Studenten. Von den vielen spannenden Daten die sie bekamen und den vielen Entdeckungen, die sie erst möglich gemacht hatten. Doch sie redeten so schnell, dass das Netzwerk nicht mithalten konnte! Jedes vierte Wort viel aus, immer wieder redete Ida etwas, wovon Zak zum ersten mal hörte, oder es kamen abgehackte Wortfetzen von Zak an, die Ida nicht verstehen konnte. Die statische Aufladung zuckte nervös in Ida herum und der Staub auf ihren Platinen stellte sich vor Angst um ihren Zak immer mehr auf: „Ihm ist doch wohl hoffentlich nichts passiert, geht es ihm gut?!“. Von den gleichen Gefühlen überwältigt machte sich ihr Geliebter die gleichen Sorgen, so wie es ein Paar tut, das gemeinsam in die Welt aufbrach und dann getrennt wurde.

Ihr übereinstimmendes Baujahr brachte sie aber auch auf die gleichen Ideen: Nachdem sie kurz verstummten, fingen sie an, jede einzelne Botschaft des jeweils anderen zu bestätigen. Nichts sollte mehr verloren gehen, wenn der andere nichts sagt, müsste eben alles nochmal gesendet werden, bis es wieder sicher wäre, dass alles ankam! Also taten Ida und Zak das, und schafften so ihre ersten Botschaften. Die erfolgreichen Nachrichten erfüllten sie mit Freude, ihre Leiterbahnen konnten die ganzen ausgeschütteten Elektronen fast nicht mehr tragen! Nun wusste Zak, dass Ida wohlauf war und sie wusste dasselbe von ihm.

Wie das Leben so kommt, waren sie aber nicht die Einzigen mit der Idee, über den großen Teich kleine Botschaften zu schicken. Viele andere Computer wollten mit anderen reden, und dann waren da noch diese Professoren und Studenten, die ständig meinten, sie müssten über Wissenschaft schreiben. Die vielen anderen Pakete verzögerten die Botschaften unseres Liebespaares, ihre erste Idee funktionierte plötzlich nicht mehr! Manche Bestätigungen von Ida kamen auf einmal so spät an, das Zak seine Nachricht bereits wiederholt hat. Ida glaubte schon, ihr Zak würde zu Stottern beginnen! Doch jetzt wussten sie ja schon, was das Problem sein muss: Das Netzwerk kann einfach nicht nur für sie da sein, sie müssten auch etwas Rücksicht auf ihre Mitrechner haben. Also fingen sie an, immer eine Zahl zu ihren Botschaften zu schreiben. „Ha!“, dachte sich Zak, „Ida wird das sicher verstehen, jetzt ist es egal, wenn ich ihr versehentlich etwas doppelt schicke!“. So kam es auch, die Zahlen ergaben immer Sinn und keine Nachricht würde mehr doppelt interpretiert werden – was sie doppelt bekamen, konnten sie getrost wieder zurück an das Kraftwerk schicken, das ihnen die Elektronen erst gebracht hatte.

Glücklich sendeten sie weitere Nachrichten und kamen sich immer näher. Der große Teich fühlte sich langsam wie ein kleinerer an, die Hopps spürten sie schon fast nicht mehr und sie hatten schon fast das Gefühl, endlich wieder zusammen zu sein. Doch die Professoren und Studenten, und besonders die User, hatten auch Ansprüche: Sie wollten immer mehr ausrechnen und manchmal war Ida zu belastet, um Zak direkt eine Antwort senden zu können. Zak verstand das natürlich, er wollte seine Angebetete schließlich nicht noch mehr unter Druck setzen. Leider musste er sich dann trotzdem wiederholen und wusste dann nicht mehr, ob die Bestätigung von Ida eigentlich für seine originale Botschaft oder für seine Wiederholung war. Manchmal gingen so die mühsam verschickten Briefe verloren und sie wurden wieder etwas zurückgeworfen. „Von denen lasse ich mich aber nicht unterkriegen!“, bäumte sich Ida auf, „Ich werde einfach auf meine Bestätigungen die Botschaft die ich gemeint habe ansprechen!“. Und so schrieb sie auf jede Bestätigung die Nummer der Nachricht die sie meint auch noch dazu, ihr Zak würde schon wissen, wie man damit umzugehen hätte – immerhin hatte er ihr damals auch schon kommentarlos Nummern zu seinen Nachrichten geschickt. Zak war nicht lange verwirrt, er verstand sofort, was Ida ihm sagen wollte. Er nahm das Muster natürlich auch gleich an, immerhin wollte er ja, dass sie sich besser verstehen konnten.

Nachricht um Nachricht sendeten die beiden also nun, stets kurze Texte über ihren Alltag, ihre Gedanken und ihre Liebe zueinander. Es war zwar anfänglich mühsam, doch mit der Zeit war es so, als müssten sie nicht mehr darüber nachdenken und sie würden das alles nebenbei machen (Anm. Referenz auf Netzwerkhardware). Es war mehr und mehr so, als könnten sie so miteinander sprechen, als würden sie zusammen sein. Wieder gemeinsam einsam, so wie in ihrer Fabrik. Die Tage vergingen, die Welt veränderte sich, doch ihre Nachrichten verstummten nie.

Und so endet unsere Geschichte von Zak und Ida, deren größter Wunsch nun am Ende doch noch in Erfüllung gegangen ist. Und wenn man ganz genau hinhört, kann man ihr leises Flüstern bis heute hören.

Script zum automatischen Testen eines Programms mit festgelegten Inputs und Outputs

Um in Systems Programming automatisch Tests der letzten C Exercise durchführen zu können, wurde ein kleines Script praktisch, welches automatisch die eigene Binary für alle input.txt Dateien überprüft. Man legt es neben zwei Ordner namens „input“ und „output“, welche die passenden Dateien für die Tests beinhalten (wie im gegebenen Beispielordner)

# Aufruf
./test.sh build/minesweeper

Das Script ist hier in einem eigenen Gist enthalten, im folgenden als Auszug dabei und als Archiv auch als Datei an diesen Artikel angehängt.

#! /usr/bin/env bash

# This test script tries all inputs and compares them with
# their respective outputs. Supply it with
# the name of the executable.

name=$1

# Color Constants
SUCCESS_COLOR='\033[0;32m'
ERROR_COLOR='\033[0;31m'
NO_COLOR='\033[0m'

DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"

if [ "$#" -ne 1 ]; then
    echo "Must supply path to minesweeper executable!"
    exit
fi

if [[ ! -x "$name" ]]; then
    echo "The file must be the executable!"
    exit
fi

echo "Running tests for binary in \"$name\"."
echo "Path of tests: \"$DIR\""

for file in $DIR/input/*.txt; do
    testname="${file##*/}"
    outputname="${testname/input/output}"

    expected=$(cat $DIR/output/$outputname)
    result=$($name $file)

    (diff <(echo "$result") <(echo "$expected") && printf "${SUCCESS_COLOR}Test in $file ran successful! $NO_COLOR \n") || printf "${ERROR_COLOR}Test in $file failed! $NO_COLOR\n"
done