4. Installing Rocket Chat with own MongoDB instance on a Raspberry Pi B

   I was tasked with installing Rocket.Chat on a raspberry pi. Currently I have a PiB and a Pi3 that are not tasked with anything. Since I expect myself having other plans for the Pi3, I chose to try installing Rocket.Chat on the PiB.

   ---

   First we start with installing raspbian on our pi. The light edition should do it. Do not forget to resize the root partition (using fdisk or parted) if you're using the light edition since it is not so easy to do from inside the raspbian system.

   But let's say we have a fresh raspbian installation and start from there.

   ---

   First we have to install all dependencies. Those are Node.js, MongoDB and graphicsmagick. Graphigsmagick we will install through the repository while we will build node, to get the latest and greatest version, ourselves.

   Starting with node, we download the latest node source code and unpack it wget https://nodejs.org/dist/v5.9.1/node-v5.9.1.tar.gz && tar -xzf node-v5.9.1.tar.gz. We now can just cd in there (cd node-v5.9.1) and build and install it (./configure && make && sudo make install). This will take quite some time. This might even take a few hours. After the configure step, you can make > makelog & and then disown in order to leave that session alone and even close it. But don't forget to sudo make install once it's done.

   In the meantime, if we have multiple terminal sessions or another ssh session, we can start installing the other stuff. graphicsmagick we can install with sudo apt-get install graphicsmagick. No problem there.

   MongoDB is a little bit more complex. They do not supply packages for our system, so we need to compile it ourselves as well. But this needs much more memory than our Pi has, so we need to add some swap memory as well.

   I had a spare 1GB usb stick lying around so I formatted this drive to swap (with gparted), plugged it into my Pi and enabled it for swapping with sudo swapon /dev/sda1. With more than 1Gb of swap, we are good to go (from what I've seen, the build process peaks at about 800MB of memory).

   Now we need to install scons with sudo apt-get install scons. We download and extract the latest source release from the mongodb download page (in my case, this was 3.2.4) with wget https://fastdl.mongodb.org/src/mongodb-src-r3.2.4.tar.gz && tar -xzf mongodb-src-r3.2.4.tar.gz The build process is not so hard, it just takes time. Once we cd ed into the source folder, we can start building the database server with scons. For me, this took slightly less than 30 hours so putting this one in the background as well and then going for a long walk, then a sleep, and then for a long walk again, might be good idea.

   After this is done, we install MongoDB with sudo scons install. This will, again, take a some time.

   If you've put all the stuff in the background, you can, once in a while, log in and check with top, whether your Pi is still doing something.

   ---

   I tried building MongoDB myself, before opting for the packages provided. During this exercise, I learned something, that makes me a bit wary.

   MongoDB's build process does not work with the source from github. The configure process fails with a source archive from github while the one from the download page, which should be identical, fails. This is quite an issue. Also, I couldn't find a MongoDB bugtracker linked anywhere from github or the MongoDB homepage. This leads me to believe that MongoDB is not really interested in the open source community and fostering an open infrastructure. Rocket.Chat is built upon MongoDB but I won't be using MongoDB for any of my projects.

   ---

5. Solving Tatham's Puzzles - Signpost (backtracking)

   I've started writing solvers for games of Simon Tatham's Portable Puzzle Collection. Those Problems can usually be reduced to some NP-complete problem. This is quite a fun exercise.

   

   Unsolved Signpost Puzzle

   We will be continuing with the puzzle "Signpost", which is a variant of Hamiltonian paths in a directed graph where, for some fields or nodes, the position within the path is given.

   The goal of the puzzle is to connect the Node "1" to some node, which is then node "2" in the direction the arrow points to. All numbers need to be connected to their successor until all nodes have a single unique number from "1" to (in this example) "25".

   We will be solving this problem in two different ways, both with the help of the programming language Python. But first of all we'll need to convert a puzzle into a machine readable format. Luckily, Signpost has an easy and accessible format. The problem instance from the image is the instance 5x5:1cceefcfggeeccghcac3e12hch10ah25a. It starts off with the size of the problem and then a list of letters that show the directions of the arrow where a is north or 12 o'clock and all other letters go clockwise with h being north-west. A letter can be prefixed by a number which is the hint for that node. That node's number is fixed. The cells or nodes are defined line by line from the top left to the bottom right.

   Problems don't need to start with 1 or end with the last number. The start and the end of the path can be anywhere but puzzles generated with the ends at opposite corner look nicer.

   First we define what our data looks like. We implement a simple form of directed graph that we define as a set of nodes and their successors. From that we derive following definition:

   class Node(object):
       hint = None
       following = frozenset()
   
       def __init__(self, direction):
           self.direction = direction
   

   We don't want to use any of that code in a library or something something so we don't do anything fancy here and we use the simplest class definition that comes to mind.

   ---

   

   ^(?P<size_x>\d+)x(?P<size_y>\d+)$

   

   (?P<defn>\d*[a-h])

   Now we go on to parsing the problem. The parsing function should get the problem as a string and return a 3-tuple containing width and height of the problem as well as a mapping of positions within the grid to ``Node`` instances.

   Onto actually parsing. We can split at the colon and then regular expressions to the rescue. The size definition has the form ^(?P<size_x>\d+)x(?P<size_y>\d+)$ while a single node definition has the form (?P<defn>\d*[a-h]). As we can see, the digits are optional but we need to greedily accept them. All non-overlapping occurences in order will be our cell definitions.

   In code we, again, do nothing too too fancy:

   def parse(puzzle_str):
       directions = {
           'a': (0,-1), 'b': (1,-1), 'c': (1,0), 'd': (1,1),
           'e': (0,1),  'f': (-1,1), 'g': (-1,0),'h': (-1,-1)
       }
   
       size, _, definition = puzzle_str.partition(':')
       r_size = re.compile(r"^(?P<size_x>\d+)x(?P<size_y>\d+)$")
       r_defn = re.compile(r"(?P<defn>\d*[a-h])")
       size_t = tuple(map(int, r_size.match(size).groups()))
       w, h = size_t
       nodes = {}
       for n, m in enumerate(r_defn.finditer(definition)):
           pos = (n % w, n // w)
           nodes[pos] = Node(directions[m.group(0)[-1:]])
           hint = m.group(0)[:-1]
           if hint:
               nodes[pos].hint = int(hint)
       return w, h, nodes
   

   And we also need to fill in the successor Nodes. This is no problem at all.

   w, h, nodes = parse(sys.argv[1])
   from itertools import product
   for x, y in product(range(w), range(h)):
       this_node = nodes[(x,y)]
       dx, dy = this_node.direction
       x, y = x + dx, y + dy
       while x >= 0 and x < w and y >= 0 and y < h:
           this_node.following = this_node.following | frozenset([nodes[x,y]])
           x, y = x + dx, y + dy
   

   ---

   And now on to actually solving this thing. The idea is, that we slowly build a list of Nodes that is our solution. The first element is the Node with the hint "1" and we iterate through all nodes that follow that Node and do not have a hint that is other than "2", and so on. And of course, the Node that we add to the solution is not allowed to have already been part of the solution and if there is a node with that hint, it should be this exact one. If we find such a conflict in our solution, we reject that solution and return to an earlier partial solution.

   Instead of using recursion, we build a queue of partial solutions until we get a complete solution. This is functionally identical to restarting a solver function with partial solutions of increasing size. In that case, the call stack manages the backtracking. But we'll do it with a queue this time. We build the queue so that every element in the list is either

   1. a partial solution (beginning from 1) without conflicts
   2. a partial solution (beginning from 1) where the last element is in some conflict
   3. a complete solution

   For case 1, we remove the partial solution that has the length n and add all partial solutions of length n+1 by iterating through all successor Nodes that have not yet been part of the partial solution. For case 2, we reject that partial solution. For case 3, we immediately return that solution and are finished.

   def solve_dhc(nodes):
       # get the Node that has hint 1
       first = next(iter(n for n in nodes.values() if n.hint == 1))
       # get the set of all hints, so it is easier to check for conflicts
       hints = frozenset(n.hint for n in nodes.values() if n.hint is not None)
       from collections import deque
       q = deque([[first]]) # initializing queue
       while q:
           curr = q.pop()
           idx = len(curr)
           if (idx in hints or curr[-1].hint is not None) and curr[-1].hint != idx:
               continue # case 2
           if idx == len(nodes):
               return curr # case 3
           for _next in curr[-1].following: # case 1
               if _next not in curr:
                   q.append(curr + [_next])
   

   This algorithm terminates because we always remove one element from the queue of some length n and possibly add a large but finite amount of elements of length n+1 and the algorithm terminates when we have an element in the queue of some possibly large but finite length.

   Sidenote: if you use popleft instead of pop you get a breadth-first search instead the depth-first search, that is implemented here. Add to the right and pop from the right for depth-first and add to the right and pop from the left for breadth-first. Since every proper solution has the exact same length/depth (that we know and never go further anyways), searching depth-first is strictly better than breadth-first.

   ---

   And given a solution, we still have to print it. That's the easy part.

   dhc = solve_dhc(nodes)
   
   fill = len(str(w*h))
   for l in range(h):
       for c in range(w):
           node = nodes[(c,l)]
           print(str(dhc.index(node) + 1).rjust(fill), end=" ")
       print("")
   

   ---

   

   Solved Puzzle

   And there's the solution for our puzzle.

   $ python3 signpost_dhc.py 5x5:1cceefcfggeeccghcac3e12hch10ah25a
    1 20  9  2 21
   23 14 13 22 24
   15  5  7  6  8
   18 19 11  3 12
   16 17 10  4 25
   

   ---

6. My computer science course of Jan 2016

   As I told before, in January I have been teaching a class preparing for an exam in theoretical computer science master's students.

   There were little over 20 people in attendance and it was a nice experience I wouldn't mind repeating. During the evaluation process (I hope to get access to the official evaluation dataset) I got almost only high marks in all categories which I'm rather proud of.

   I was a bit baffled when I asked for a list of well-known set operations and stared into blank faces but one never knows if it is shyness or missing knowledge keeping the answer from being given. I'd like it to be the former.

   ---

   Since, after my first teaching job, I've yet to run out of hope, I offered to answer questions via email after the fact and a few messages laster, here is what most students seem to have problems with:

   How do you find out whether a language is regular/context-free?

   For both types of language we have something called the "pumping lemma" which is basically that in any infinite language with a finite set of production rules, there exists a list of words that form a repeating pattern that has a relation to a loop within the production rules.

   For regular languages (say \(R\)) it is basically \(L \in R \to (\exists uvw \in L: uv^*w \subseteq L)\) with the condition of \(v\) being not empty. The idea is, that a regular language can be represented as a deterministic finite automata (DFA) that has a finite number of states while the language is infinite so that some state has to be reached more than once in the course of accepting a word. After reading \(u\) you are in some state and then you read \(v\) and are in the same state you were after reading \(u\) and after then reading \(w\) the word is accepted. The word \(v\) can be repeated many times or not at all.

   CC BY-SA 3.0 / Jochen Burghardt

   For context free languages (say \(CF\)) this is nearly the same, only that there is some nonterminal that can produce itself from the production rules. Repeating words appear left and right of the looping nonterminal equally often (\(v\) and \(x\)). The looping nonterminal also produces a word without looping (or every production including that nonterminal wouldn't halt) that we call \(w\). So the formula for the context-free version of the pumping lemma is basically \(L \in CF \to (\exists uvwxy \in L: (\forall n \in N : uv^nwx^ny \in L))\) with the sidecondition of not both \(vw\) and \(wx\) being empty.

   In both formulas have the form \(L \in L' \to PL\) and we get the reversal \(\neg PL \to L \notin L'\) for free. So to show that a language is regular or context free it is not enough to show that the pumping lemma holds because there are languages that are not in that category and still have words that can be pumped.

   So to show that a language is context free/regular one has to construct a context free grammar/(non)deterministic finite automata and if you can't find any way to pump words then the language is not in that category.

   The direction of the implication-arrow (or that it isn't an equivalence) seems to have my students stumped.

   ---

   And here you go with two languages that fulfill the pumping lemma for a language category and are not a language of that type:

   • \(a^n | n \text{ is not prime}\) with \((u,v,w) = (aa,aa,\varepsilon)\)
   • \(a^nb^n | n \text{ not a power of two}\) with \((u,v,w,x,y) = (\varepsilon,aaa,aabb,bbb,\varepsilon)\)

   ---

7. Solving Tatham's Puzzles - Pattern

   I've started writing solvers for games of Simon Tatham's Portable Puzzle Collection. Those Problems can usually be reduced to some NP-complete problem. This is quite a fun exercise.

   We will be starting with the puzzle "Pattern", also known as Nonograms that we reduce to SAT.

   

   Unsolved Nonogram

   First to explain the puzzle: The cells of the puzzle can be filled with black or white squares. The numbers on the sides of the rows and colums denote the number of consecutive black squares. Every run of black squares has to be seperated from another run by white squares.

   First we want to define a type for our problem.

   type PSize = (Int, Int)
   type Run = [[Int]]
   type Runs = (Run, Run)
   data Problem = Problem PSize Runs deriving Show
   

   The puzzle on the side is defined in the Tatham format by the string 10x10:2/3.2/1.1.3/2.5/2.2.4/1.1.4/1.3/1.1.2/4/4.1/5.2/2.3.3/1.2/6/3/1/4/6/7/4.1. It has a size information and then the list of runs. Another format we want to support is the Haskell Runs format which would be ([[2],[3,2],[1,1,3],[2,5],[2,2,4],[1,1,4],[1,3],[1,1,2],[4],[4,1]],[[5,2],[2,3,3],[1,2],[6],[3],[1],[4],[6],[7],[4,1]]). This format seperates the runs for rows and columns and ommits the size information.

   For the second format we can use Haskell's own read function. For Tatham's format we have to define a parser. I've added type information for most functions which is often needed for code involving read.

   import Text.ParserCombinators.ReadP
   number' = many1 (choice (map char ['0'..'9']))
   
   r_size :: ReadP PSize
   r_size = do l <- number'
               char 'x'
               r <- number'
               return (read l, read r)
   
   r_run :: ReadP [Int]
   r_run = do { li <- sepBy number' (char '.'); return $ map read li }
   
   r_runs :: ReadP [[Int]]
   r_runs = sepBy r_run (char '/')
   
   r_problem :: ReadP Problem
   r_problem = do size <- r_size; char ':'
                  runs <- r_runs
                  skipSpaces; eof
                  return $ Problem size (take (fst size) runs, drop (fst size) runs)
   

   What do we now do with such a problem? First we want to check it for consistency. If we got size information it should fit the runs and the numbers in the runs (and the spaces between them) shouldn't add up to more than the size.

   import qualified Prelude as P (all, (&&), not)
   consistent :: Problem -> Bool
   consistent (Problem size (xin, yin)) = consistent' size xin P.&& consistent' (swap size) yin
   consistent' (w, h) xs = (w == length xs) P.&& P.all (\x -> (sum x) + (length x - 1) <= h) xs
   

   

   Calling our solver

   But now on to solving the problem. We will reduce this problem to SAT using the Ersatz library. The encoding of a problem, I guess, is obvious. We say that every cell within the Nonogram is a Variable Bit and a bit being True has the semantics of that field being colored black while False would mean white.

   We want to build constraints of single rows or columns and then solve the conjunction of all those row/column-constraints for satisfiability. Therefore we define a function of the type [Int] -> [Bit] -> Bit that takes a list of Integers (the numbers of one column or row) and the list of remaining Bits that do not yet are constrained.

   First we begin with the end of the recursion. If no number is left or the remaining number is zero (for empty columns or rows), we want all remaining variables to be False. (we take for to be defined as flip map)

   build_runs :: [Int] -> [Bit] -> Bit
   build_runs nums vars = case nums of
     [] -> all not vars
     [0] -> all not vars
     x:xs -> let max_d = length vars - (length xs + sum xs) - x
                 run   = [not] ++ replicate x id ++ [not]
                 v     = [false] ++ vars ++ [false]
             in any id $ for [0..max_d] $ \ d ->
                (all not $ take d vars)
                && (all id $ zipWith id run $ take (x + 2) $ drop d v)
                && (build_runs xs $ drop (x + d + 1) vars)
   

   

   Solved Nonogram

   The recursion is something to think about a bit. We're given a number of consecutive black squares x and all the variables in the column/row vars. The x Trues can be put anywhere from 0 to max_d where max_d is all the rest of the variables take the minimum necessary space of the remaining number of numbers xs, while all variables before that number of black squares and one after need to be white. For every possible position the rest of the variables need to fulfill the same condition with the rest of the numbers.

   Now we have to combine all the constraints from a given problem.

   nono :: (MonadState s m, HasSAT s) => Problem -> m (Map (Int,Int) Bit)
   nono (Problem (sizex, sizey) (xin, yin)) = do
     let indices = [(x, y) | x <- [1..sizex], y <- [1..sizey] ]
     vars' <- replicateM (length indices) exists
     vars <- return $ Map.fromList $ zip indices vars'
     let getx x = for [1..sizey] $ \y -> (vars ! (x,y))
         gety y = for [1..sizex] $ \x -> (vars ! (x,y))
         xs = zipWith build_runs xin (map getx [1..])
         ys = zipWith build_runs yin (map gety [1..])
     assert (all id xs && all id ys)
     return vars
   

   Internally we let Ersatz identify variables by their position in the grid Map (Int,Int) Bit. Now we can solve our problem easily using minisat with Ersatz's native minisat binding. Given a solution, we just format it correctly and give it to the user.

   main = do
     input <- getContents
     let parsed = parse_tat input
         problem = case parsed of
           Just p -> p
           Nothing -> let (xin, yin) = read input :: ([[Int]],[[Int]])
                      in Problem (length xin, length yin) (xin, yin)
   
     putStrLn $ "Size: " ++ (show $ problem_size problem)
     unless (consistent problem) $ do {putStrLn "Problem inconsitent"; exitFailure}
   
     (Satisfied, Just solution) <- solveWith minisat (nono problem)
     let sizey = snd $ problem_size problem
         lines = for [1..sizey] $ \i -> filter (\ ((x, y), b) -> y == i) $ toList solution
         conv  = map $ \((x,y), b)-> if b then 'X' else ' '
         join = foldr (:) ""
     forM_ (map (join . conv) lines) print
   

   And we're done.

   ---

8. Gnome Foundation membership renewed

   My membership in the Gnome Foundation has been renewed. I've been co-maintaining several of the included games for the last two-and-a-half years. My membership has now been renewed until early 2018. I hope I can find a little more time to spend on our favorite desktop environment in the near future.

   ---

« Page 6 / 8 »