Logic Based Rummikub Solver

Rummikub is a wonderful boardgame, that is fun for everyone. ... except for me, because I always lose at it. To help me win games, I decided to cheat and build a rummikub solver. While there already exist a few solvers for the game [1,2,3,4], no logical implementation has been published yet. Let's change that!

This post delves a bit deeper into the logical implementation of Rummikub. Using this implementation, a Rummikub Solver was built with a browser-based interface and a Python server. The source code for the entire project is available here. A (slower) online version of the tool is also available.

Rummikub

Rummikub is a fairly simple game to start playing. Everyone starts with 14 tiles on their board, with each tile consisting of a number between 1-13 and one of four colors (blue, red, black, yellow). The goal is to be the first player with an empty board, by placing all your tiles in sets on the table. There are two types of sets:

• Runs: three or more tiles of the same color with consecutive numbers (e.g. red1 - red2 - red3)
• Groups: three or more tiles of the same number, with a different color (e.g. red1 - black1 - blue1)

It's also allowed to manipulate the tiles on the table, as long as the remaining sets remain valid. For instance, if there is a set of four tiles, you can take one of them to form a new set.

Logical Implementation

For the logical implementation, we will rely on a logical solver called the IDP system. It uses an extended version of first order logic as its input language, allowing us to create complex statements without too much of a hassle.

The advantage of using a logical implementation is that instead of creating a procedure to solve a problem, we simply define what a good solution looks like. This is done in a descriptive manner. For instance, let's start by defining that a group has tiles of the same numbers but with different colors.

∀g[Group] t1[Tile] t2[Tile]: t1 ≠ t2 
    ∧ in_group(g, t1) ∧ in_group(g, t2) 
    ⇒ number_of(t1) = number_of(t2) 
       ∧ color_of(t1) ~= color_of(t2).

In words, the above line reads: for every group g, tile t1, tile t2, IF t1 does not equal t2 AND t1 is in group g AND t2 is in group g, THEN the number of t1 equals the number of t2 AND the color of t1 is not the color of t2.

For the runs, we do something similar, except that we first define that their colors should be the same, and then define that their numbers should be consecutive.

∀r[Run] t1[Tile] t2[Tile]: t1 ≠ t2 ∧ in_run(r, t1) ∧ in_run(r, t2)
    ⇒ color_of(t1) = color_of(t2).

∀r[Run] t1[Tile]: in_run(r, t1) ∧ highest_in_run(r) ≠ t1 ⇒
   (∃t2[Tile]: in_run(r, t2) ∧ number_of(t2) = number_of(t1) + 1).

The first rule states that "For every run r, tile t1, tile t2, IF t1 does not equal t2 and they are in the same run, THEN their color should be the same." The second rule states "For every run r, tile t1, IF t1 is in run t2 AND it is not the highest number, THEN there should be a tile t2 with the consecutive number."

Next, we define that every set is either empty or has at least three tiles. Et voila! We have created the rules defining what correct sets should look like. (Note that we haven't defined nb_in_group, nb_in_run or highest_in_run, but I will leave those out for simplicity.)

    ∀g[Group]: nb_in_group(g) = 0 ∨ nb_in_group(g) ≥ 3.
    ∀r[Run]: nb_in_run(r) = 0 ∨ nb_in_run(r) ≥ 3.

All that remains now is defining what tiles a player starts with, and then using IDP's minimization inference task in order to always find the solution in which most of the tiles have been placed on the board. If you are interested in the full implementation, feel free to check it out on GitLab.

[1] Rummikubsolver, by gregorias

[2] Rustikub, by wemyss

[3] RummikubSolver, by Ollie-Hooper

[4] RummySolver, by nachogoro