Software

Booleguru (Version 1, Experimental Version 2) is a logical polyglot, a multitool for propositional logic. You can use it to read logical formulas in many different languages, transform them in-memory, and serialize them to many (other) different formats. See the paper on version 1, a paper for version 2 will be published at a later date.

The second version, currently still under heavy development, features a new and improved data-structure to store formulas (right-threaded binary trees, representing n-ary logical operators in a tree with arbitrary depth) and first-class Python integration. The threadedness of the tree enables stack-less post-order traversal, which is important for evaluating functions and general efficiency of the tool. The tree also supports structure-sharing, using a new data structure we call Kitsune, after the mythical nine-tailed fox. A Kitsune always has one head and any number of tails, each tail referring to another Kitsune. The only time stacks are needed during traversal is when encountering such Kitsunes, as then the last Kitsune on the current trail has to be remembered.

F4NCGB [Pre-Print] is a highly efficient non-commutative Gröbner-basis computation engine based on an optimized F4 algorithm developed by Clemens Hofstadler and me. I contributed the core data-structures and technical optimizations. The software was merged into Oscar, a visionary new computer algebra system which combines the capabilities of four cornerstone systems: GAP, Polymake, Antic and Singular.

Paracooba is my Master's Thesis project that was exteded to also work with QBF and portfolios of solvers. It is a distributed SAT and QBF solver.

QuAPI adds assumption-based reasoning support to any given SAT or QBF solver binary by instrumenting their read() calls through LD_PRELOAD. It can be used as a standalone CLI tool or as a library for other solver authors.

prefiXtract extracts information from the prefix of a QDIMACS formula. This is very useful when doing competitions.

This is a project that originated from a seminar. It implements an easily extendable C-based exact cover solver, with support for colors and multiplicity. It implements Donald Knuth's Algorithm X, C, M, and C$. It is available on GitHub as both the source code and a web-based version. It is also available as a pre-compiled package on PyPI, thanks to the excellent CIBuildWheel.

pyQBF is an extension of pySAT that I've writte together with Mark Peyrer. It adds quantifier support to pySAT and embeds multiple QBF solvers and can directly execute them from a Python environment. It is also available on PyPI.

SIMDIMACS is an overly efficient DIMACS, QDIMACS, LRAT, and DRAT parser that is even more efficient than the parser included in Kissat. It accomplishes this using clever use of SIMD instructions to parse numbers, pioneered by Wojciech Muła.

Simsala is a collection of scripts useful for benchmarking software. It is optimized to be minimal and hackable, without introducing dependencies into the system, while still supporting running software on managed Slurm clusters.

Distrac is a distributed tracing program implemented in C++ that links different instances of a program together by causal dependencies of messages the instances exchange. It was developed during my Master's Thesis.

Before my studies, I was part of the HARPTech group, which was a group of five interested students who wanted to construct an autonomous rover. The autonomous did not work out, but we built a very nice six-wheeled rover nontheless. I did the software, which was fully event-based and supported sending events from a base-station to the rover platform.

My Bachelor's Thesis was then built on checking the steering kernel of this system, meaning if the wheels would react correctly to all given inputs. This was done by translating the Python code running on the rover into SMTLIB-2 formulas, which were then checked using SMT-solvers. The code for this is also on GitHub as RVerify.

KoradControl is a small utility program written in C++ with the Asio library to control Korad desktop DC power supplies, mainly the Korad KA005P. I firmly believe simplistic CLI tools have great value, so I wanted to try to be as primitive as possible, while providing more features than commonly used GUI tools.

RotelControl is a small utility to control a Rotel A12/A14 amplifier via its network port. This tool is useful to build a hotkey for controlling the volume of the amplifier and works well for that purpose.

My first game! It is old and I doubt it can be still be compiled easily, but it is online in its own repository. It was integrated into the Pigaco system, with which I tried incrementally built a Linux-based gaming console, including window-management and compositor.

The Pigaco project was meant to provide libraries to communicate with a shared memory input-controller that relays inputs from USB-conntected Arduinos to games as fast as possible. This worked really well and (looking back) it is amazing how far one can come with these techniques.

With Valve's Steam Deck being a great success, I believe the design direction of Pigaco was exactly right - although I was too inexperienced back then to see how far-reaching the involved technical resources were and how much would have to be invested for this system to work nicely. It was fun for demos though.

This project injects additional graphics over an OpenGL program, after injecting itself into its process using LD_PRELOAD. This was an interesting exercise and later led to the foundational knowledge required for QuAPI.

This improved Dwarf Fortress map compressor reads the old DF BMP files of maps and compresses them down into the proprietary format introduced by ShadowLord (code available on GitHub). The files are compatible with the web-based renderer of the DFMA. The project also includes a PHP-based map renderer, although it is not actively hosted to my knowledge.