Buchtipp: “Darum nerven Japaner”


Darum nerven Japaner Buchcover

Fig. 1. “Darum nerven Japaner – Der ungeschminkte Wahnsinn des japanischen Alltags”

Der Autor Christoph Neumann erklärt erst im Nachwort wie er dazu kam dieses Buch zu schreiben. ここがヘンだよ日本人 (laut dem Autor mit “Die spinnen, die Japaner!” frei nach Asterix & Obelix zu übersetzen) ist eine populäre japanische TV-Sendung, in der er auftrat. Dort diskutieren die Anwesenden die Gewohnheiten der Japaner und hinterfragen deren Sinnhaftigkeit. Als Spin-Off dieser Auftritte schrieb er das Buch, welches zu einem der bekanntesten seines Genres wurde.

Als Kenntnisse greift er damit auf seine Erfahrungen als Deutscher mit längerem Auslandsaufenthalt in Japan zurück. Er illustriert japanische Eigenheiten anhand seiner Erfahrungen und schreckt nicht davor zurück sie mit harten Worten in krassen Gegensatz zu europäischen Gewohnheiten zu setzen. Die diskutierten Themen illustrieren sich in den 19 Kapiteln des Buchs:

  1. Vorwort: Dürfen Japaner nerven?
  2. Regeln: Das Volk will belehrt werden
  3. Schuhe: Das elfte Gebot: “Du sollst deine Schuhe ausziehen”
  4. Essen: Die mit dem Bauch denken…
  5. Schwimmbad: Japan im Schnelldurchschwimm
  6. Radfahren: Radfahren schwer gemacht
  7. Mafia: Verbrecher, die keine sind
  8. Warnungen: Achten Sie darauf, darauf zu achten!
  9. Verhütung: Pille killen und Föten töten
  10. Körpersprache: Das Gegenteil von Anmut
  11. Yamanote: Mehr als nur eine S-Bahn-Linie
  12. Spass: Kein Spass an der Freud
  13. Schlafen: Bett? Nein, danke!
  14. Diebstahl: Mein Geld, dein Geld – Geld ist für uns alle da
  15. Gleichheit: Reich wie Scheich und dennoch gleich?
  16. Fremdsprachen: Englisch hassen lernen
  17. Urlaub: Die Suche nach dem Vertrauten in der Fremde
  18. Müll: Parolen statt Mülleimer
  19. Big Brothers: Ist Gott eine japanische Firma?
  20. Flirt: Die Sau rauslassen, aber ordentlich

Ein netter gedanklicher 2-Tages Ausflug in den japanischen Alltag!

Buchtipp: “Darum nerven Japaner”

Time management, an analysis

This semester I consciously decided to reduce my number of courses I take. As far as academic work is concerned I need to focus on finishing the first and second semester and finish my master thesis. I reduced the amount of work in associations, I do not take some law course (oh, that’s been some while!) and I don’t take any courses of higher semester.

I wanted to discuss the amount of time I want to invest into something. I fixed holes in my schedule and organized remaining time. I have several categories and every category as a minimum amount of time I invest per week. Good opportunity to document that for future reference:

  • I consider 16 hours per day productive. So I have 8 hours of sleep per day.
  • I invest 42.5 hours per week in attending lectures, tutorials, meetings, visiting the Aikido dojo and quality time.
  • 69.5 hours are left. How do I use them?

There are 10 categories:

project:
programs I want to release, watch tutorials/videos, publishing content
university:
old courses I need to finish (exams, submissions)
A2:
course Analysis 2 and everything related
LA2:
course Linear Algebra 2 and everything related
FOM:
course Foundations of Mathematics
master thesis:
releasing subprojects for my master thesis, writing thesis document
JAP:
course Japanese Language and everything related
日本語:
learning Japanese on my own (especially Aikido & math)
日本:
exchange student year organization
GLT16:
upcoming Grazer Linuxtage – graphics work

And how much time do I invest into each category at minimum?
This sums up to 34 hours and I have 69.5 hours available, so this is flexible on purpose.
But it gives a relative measure for future reference:

project 3 hours per week
university 4 hours per week
A2 5 hours per week
LA2 4 hours per week
FOM 1 hours per week
master thesis 8 hours per week
JAP 3 hours per week
日本語 3 hours per week
日本 2 hours per week
GLT16 1 hours per week
Time management, an analysis

Boston Key Party: Graph 3-coloring with SAT solvers

The Boston Key Party was held between 4th and 6th of March 2016. A few colleagues of mine attended this event and asked for help with one particular problem:

Given a graph with 683 vertices and 1253 edges. Assign one of three colors to each vertex. No edge must connect two vertices of the same color.

Graph 3-coloring is a classic example of an NP-complete problem. So a SAT solver might be suitable for it as far as more efficient algorithms are not known.

Let’s solve this problem with an approach similar to an implementation I use in my master thesis: Generate the CNF using python, let a SAT solver do the hard work and parse the solver’s result back to python and print the assignment of colors to vertices.

The boolean logic is really simple: Every vertex gets assigned three boolean variables. We add the following constraints:

  • Only one of three variables can be true.
  • For every edge (s, t) we look up the corresponding colors for s and t: r1,g1,b1 and r2,g2,b2. We claim not both r1 and r2 can be true. Not both g1 and g2 can be true. Not both b1 and b2 can be true.

In code it looks like this:

def oneof3(w, a, b, c):
    w.add_clause(a, b, c)
    w.add_clause(-a, -b, c)
    w.add_clause(-a, b, -c)
    w.add_clause(a, -b, -c)
    w.add_clause(-a, -b, -c)

def notboth(w, a, b):
    w.add_clause(-a, -b)

def add_constraints(graph, w):
    # constraints for colors of one vertex
    for v, (red, green, blue) in graph.vertices.items():
        oneof3(w, red, green, blue)

    # constraint for edges
    for (src, dst) in graph.edges:
        r1, g1, b1 = graph.vertices[src]
        r2, g2, b2 = graph.vertices[dst]
        notboth(w, r1, r2)
        notboth(w, g1, g2)
        notboth(w, b1, b2)

The final source code looked like this (you need to adjust the path to the SAT solver executable; you should use lingeling):

#!/usr/bin/env python3

import re
import os
import sys
import logging
import tempfile
import itertools
import subprocess


# the output format is expected to be compatible with lingeling
SATSOLVER_EXECUTABLE = '/opt/lingeling-bal-2293bef-151109/lingeling'
SATSOLVER_TIMEOUT = None  # or specify an integer in seconds
VERTICES = 683


class Graph:
    def __init__(self, nb_vertices):
        self.edges = set()
        self.nb_vertices = nb_vertices
        self.vertices = {k: (3 * k + 1, 3 * k + 2, 3 * k + 3)
                         for k in range(nb_vertices)}

    def read_edges(self, filepath: str):
        """Read edges from a file containing '{src} {dest}' lines"""
        with open(filepath) as fd:
            for line in fd:
                if line.startswith('#'):
                    continue
                src, dst = [int(v) for v in line.split()]
                assert 0 <= src < self.nb_vertices \
                    and 0 <= dst < self.nb_vertices, "vertex number invalid"
                self.edges.add((src, dst))

    def get_assignment(self, model: set):
        """Given a set of positive or negative boolean variables,
        return a dictionary assigning 1, 2 or 3 to every vertex
        """
        ass = {}
        for v, (r, g, b) in self.vertices.items():
            assert (r in model) ^ (g in model) ^ (b in model)
            assert (r not in model) | (g not in model) | (b not in model)
            ass[v] = {r in model: 1, g in model: 2, b in model: 3}[True]
        return ass


# storage/writer for CNF data

class CnfStorage:
    def __init__(self, fd):
        self.fd = fd
        self.clauses = set()
        self.nbvars = 0

    def add_clause(self, *ints):
        self.nbvars = max(self.nbvars, max([abs(v) for v in ints]))
        self.clauses.add(tuple(ints))

    def finish(self):
        self.fd.write('p cnf {} {}\n'.format(self.nbvars, len(self.clauses)))
        for clause in self.clauses:
            self.fd.write(' '.join([str(i) for i in clause]) + ' 0\n')
            self.fd.flush()


# CNF primitives
#   Related: http://lukas-prokop.at/tools/truthtable/

def oneof3(w, a, b, c):
    w.add_clause(a, b, c)
    w.add_clause(-a, -b, c)
    w.add_clause(-a, b, -c)
    w.add_clause(a, -b, -c)
    w.add_clause(-a, -b, -c)


def notboth(w, a, b):
    w.add_clause(-a, -b)


def add_constraints(graph, w):
    # constraints for colors of one vertex
    for v, (red, green, blue) in graph.vertices.items():
        oneof3(w, red, green, blue)

    # constraint for edges
    for (src, dst) in graph.edges:
        r1, g1, b1 = graph.vertices[src]
        r2, g2, b2 = graph.vertices[dst]
        notboth(w, r1, r2)
        notboth(w, g1, g2)
        notboth(w, b1, b2)


# run the SAT solver

def run_solver(filepath):
    """Run SAT solver as subprocess. Return stdout"""
    proc = subprocess.Popen(
        [SATSOLVER_EXECUTABLE, filepath],
        stdout=subprocess.PIPE, stderr=subprocess.PIPE)

    try:
        outs, errs = proc.communicate(timeout=SATSOLVER_TIMEOUT)
        out = outs.decode('ascii')
    except subprocess.TimeoutExpired:
        proc.kill()
        outs, errs = proc.communicate()
        out = errs.decode('ascii')

    if proc.returncode == 20:
        raise RuntimeError('SAT solver returned UNSATisfiability')
    if proc.returncode != 10:
        errmsg = 'SAT solver returned error code {}: {}'
        raise RuntimeError(errmsg.format(proc.returncode, errs))
    return out


def interpret_output(out):
    """Read a model (set of positive/negative integers) from stdout"""
    model = []
    logging.debug(out)

    something = False
    for line in out.splitlines():
        if line.startswith("v "):
            matches = map(int, re.findall(" (-?\d+)", line))
            something = True
            for match in matches:
                if match == 0:
                    # trailing zero
                    continue
                assert -match not in model
                model.append(match)

    if not something:
        raise RuntimeError("Model empty - most likely the SAT solver " +
                           "output is incompatible with lingeling")

    return tuple(model)


if __name__ == '__main__':
    if len(sys.argv) != 2:
        print('usage: ./graph-3-coloring.py <edges.txt>')
        sys.exit(1)

    fd, filepath = tempfile.mkstemp(prefix='graph-3-coloring')

    try:
        # generate graph
        graph = Graph(VERTICES)
        graph.read_edges(sys.argv[1])
        logging.info("{} read".format(sys.argv[1]))

        # store CNF
        w = CnfStorage(os.fdopen(fd, mode='w', encoding='ascii'))
        add_constraints(graph, w)
        w.finish()
        logging.info("Finished generating CNF file")

        # run SAT solver
        out = run_solver(filepath)
        model = interpret_output(out)
        assignment = graph.get_assignment(model)

        # print result
        for vertex, color in assignment.items():
            print('{}: {}'.format(vertex, color))
    finally:
        os.unlink(filepath)

And how long did it take to run it? 0.9 seconds 😎
Thank you lingeling!

Boston Key Party: Graph 3-coloring with SAT solvers