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

After a year of hard work, my colleagues at the FMV and I proudly present Paracooba to you! This neat program of ours is a fully automated cube-and-conquer SAT-Solver that automatically discovers other daemons in the network, connects to them and distributes your SAT-Solving efforts over the network. Without any other work required, it utilizes all available cores on a given machine and even solves multiple SAT problems at once on a cluster.

To better understand all of this, we wrote a paper and made a presentation. The paper will be published in the proceedings of the SAT2020 conference. The talk, slides, and a short 2min pitch are available here. The presentation is on YouTube too.

The full presentation hosted on my webspace (no, YouTube, you may not track my visitors…)
This presentation also won the Best Presentation Award at SAT2020!

I am looking forward to continue development over time and to hearing from you!

All the best,
Max

Partial Lunar Eclipse 2019-07-16

While going through my photographs I found a picture series titled “Partial Lunar Eclipse 2019”. Some pictures came out really neat and I wanted to share them with you! These pictures were made at the Keplerwarte Linz.

I forgot to upload them back then… seems like I have to go through some old albums to look for cool stuff 🙂

Pseudo Fractal made using C, Bash and FFMpeg

Small visualizations are always fun to create and watch, right? That’s why I decided last weekend to create a small video using a simple C program using some code to create BMP graphics found on the internet (thank you!). Then, I just used bash to create .. a few .. images and stitched them together using ffmpeg. This blog entry should document what exactly I have done, so if I am interested in this again some day in the future, I can just re-use the scripts, commands, and code I created here. But first, enjoy the video!

Creating the Images

The most important thing about this whole mini-project was creating the images themselves. I wrote a small program in C, that takes a parameter and then prints out one frame on standard output in BMP format. The C program is self-contained in one file and looks like this:

#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <math.h>

// https://gist.github.com/guohai/5848088

// for Linux platform, plz make sure the size of data type is correct for BMP
// spec. if you use this on Windows or other platforms, plz pay attention to
// this.
typedef int32_t LONG;
typedef uint8_t BYTE;
typedef uint32_t DWORD;
typedef uint16_t WORD;

// __attribute__((packed)) on non-Intel arch may cause some unexpected error,
// plz be informed.

typedef struct tagBITMAPFILEHEADER {
  WORD bfType;      // 2  /* Magic identifier */
  DWORD bfSize;     // 4  /* File size in bytes */
  WORD bfReserved1; // 2
  WORD bfReserved2; // 2
  DWORD bfOffBits;  // 4 /* Offset to image data, bytes */
} __attribute__((packed)) BITMAPFILEHEADER;

typedef struct tagBITMAPINFOHEADER {
  DWORD biSize;         // 4 /* Header size in bytes */
  LONG biWidth;         // 4 /* Width of image */
  LONG biHeight;        // 4 /* Height of image */
  WORD biPlanes;        // 2 /* Number of colour planes */
  WORD biBitCount;      // 2 /* Bits per pixel */
  DWORD biCompress;     // 4 /* Compression type */
  DWORD biSizeImage;    // 4 /* Image size in bytes */
  LONG biXPelsPerMeter; // 4
  LONG biYPelsPerMeter; // 4 /* Pixels per meter */
  DWORD biClrUsed;      // 4 /* Number of colours */
  DWORD biClrImportant; // 4 /* Important colours */
} __attribute__((packed)) BITMAPINFOHEADER;

typedef struct {
  BYTE b;
  BYTE g;
  BYTE r;
} RGB_data;

int bmp_generator(int width, int height, unsigned char *data) {
  BITMAPFILEHEADER bmp_head;
  BITMAPINFOHEADER bmp_info;
  int size = width * height * 3;

  bmp_head.bfType = 0x4D42; // 'BM'
  bmp_head.bfSize = size + sizeof(BITMAPFILEHEADER) +
                    sizeof(BITMAPINFOHEADER); // 24 + head + info no quad
  bmp_head.bfReserved1 = bmp_head.bfReserved2 = 0;
  bmp_head.bfOffBits = bmp_head.bfSize - size;
  // finish the initial of head

  bmp_info.biSize = 40;
  bmp_info.biWidth = width;
  bmp_info.biHeight = height;
  bmp_info.biPlanes = 1;
  bmp_info.biBitCount = 24; // bit(s) per pixel, 24 is true color
  bmp_info.biCompress = 0;
  bmp_info.biSizeImage = size;
  bmp_info.biXPelsPerMeter = 0;
  bmp_info.biYPelsPerMeter = 0;
  bmp_info.biClrUsed = 0;
  bmp_info.biClrImportant = 0;
  // finish the initial of infohead;

  // copy the data
  fwrite(&bmp_head, 1, sizeof(BITMAPFILEHEADER), stdout);
  fwrite(&bmp_info, 1, sizeof(BITMAPINFOHEADER), stdout);
  fwrite(data, 1, size, stdout);

  return 1;
}

double func_sins(double rx, double ry) { return sin(1 / rx) + sin(1 / ry); }

void setrgb(RGB_data *d, int w, int h, int x, int y, double scale) {
  d->b = (x / (double)w) * 255;
  d->g = (y / (double)w) * 255;
  d->r = func_sins(x / (double)w / M_PI / (1+scale), y / (double)h / M_PI / (1+scale));
}

int main(int argc, char **argv) {
  int i, j;
  const int w = 2048, h = 2048;

  double scale = 0;

  if(argc == 2) {
    scale = atof(argv[1]);
  }

  RGB_data *buffer = calloc(sizeof(RGB_data), w * h);

  for (i = 0; i < w; i++) {
    for (j = 0; j < h; j++) {
      setrgb(&buffer[i * h + j], w, h, j, i, scale);
    }
  }

  bmp_generator(w, h, (BYTE *)buffer);

  return EXIT_SUCCESS;
}

Using this program, I then created a script which just repeatedly calls frakt and pipes it into ffmpeg. Because build systems are boring, this script also compiles the program by itself. Here is the script:

#! /usr/bin/env bash

export LC_NUMERIC="en_US.UTF-8"

echo "Compile frakt.c"
gcc frakt.c -lm -o frakt;

echo "Start generation of movie..."

rm out.mp4;

{
    for i in $(seq 0.0 0.01 50); do
	./frakt $i 
    done
} | ffmpeg -f image2pipe -framerate 60 -i - -c:v libx264 -vf format=yuv420p out.mp4

This is then executed and voilà – the video is finished!

I hope you enjoyed this bit of recreational programming and maybe you can re-use a bit of the code. Have a nice day!

What Is My Target Audience? Or: German vs. English Content

After reading may too many blogs and speaking with other people, I was beginning to wonder about my target audience on this site. Am I writing to German speakers only or do I focus more on global (or technical) topics? This is no easy question to answer, since this site and its sibling maximaximal.com were originally conceived only in my native language. This stemmed from local social circles and the desire to connect with other people in my area.

Nowadays, the focus is shifting a bit: I want to connect with more people that are not only from my country, but also from Europe and the rest of the world. Limiting myself to only one language makes the content I produce far less accessible to these other audiences, which is (obviously) against my interest. When I’m writing about technical topics, language barriers should break down and only the topic and required knowledge for understanding the very thing I am writing about should be the limiting factors for my readership.

This is why I decided to change this site to be multilingual. English should be the second main language of my blog and not only a second class citizen for a limited amount of sites. I am translating the most important pages and new content will be divided into these two languages. Not everything has to be in English, but the following posts generally better fit into this new group. I hope my writing is of interest to more people this way and old readers still enjoy my blog.

To conclude – I am looking forward to hearing from you and I hope you will like the incoming content!

All the best,
Max