Using a SMT solver to find optimal GBA palettes

by catboli

I've always wanted to make a GBA game and finally had such an opportunity when I had to brush up my low-level C programming skills and doing such a game looked like the perfect challenge. Luckily, there is a great SDK for writing GBA games in C, no ARM assembly needed (mostly): devKitPro. However, I'll have to leave what I found for a following blog post (and once a finish a decent game!) because, as expected, I ended up getting sidetracked by I problem I found when dealing with palettes on the GBA.

In summary, the GBA has a limited set of colors it can display at a time on the LCD screen, these colors are organized in palettes. I downloaded a bunch of image assets from the web that I wanted to use on my game and obviously they weren't made with the GBA in mind so I had to find a way to map colors in the image to the GBA format, doing so seemed simple and first but it ended up being a (fun) can of worms.

Obviously, someone could manually figure out the colors used in an image and create an appropriate palette. But we're smarted than that, even if writing this Python script takes longer than doing it by hand a x100 times :)

From GBATek we have all the GBA BG Modes, In my game I'll be using BG Mode 0 and we also can choose between 1) A single palette of 256 colors or 2) 16 palettes of 15 colors each (first color is always transparent). I prefer to use (2) because this way tiles consume less memory (just 4 bits per pixel instead of 8).

So in summary:

  • We have N tiles (always 8x8 pixels).
  • Each tile has a 4-bit index into one of the 16 available palettes.
  • Each palette has 15 colors + transparent
  • Each color is 15-bits (5-bits for R, G and B and one wasted bit)

This is a combinatorial problem so I started looking for solvers and found Z3 which is from Microsoft Research that can be used for problems like this and it has a great Python API. I decided for it because I read SAT SMT By Example and this problem seemed a bit similar to Minesweeper and Sudoku, which are problems that were solved using Z3.

We have to map your problem to a boolean system of equations, so here's our first try:

We want to find colors P(i,j,k) where i is the palette index (0-15), j is one the 15 colors (0-14) and k is one of the 15-bit colors (0-32767).

So, for example if P(10,1,0x7fff) = 1 it means that the color 0x7fff (R=31,G=31,B=31) is being used for color 1 on palette 10.

We want a solution such that:

  1. P(i,j,k) is boolean so:
Or(P(i,j,k)=0, P(i,j,k)=1)=1 for all i,j,k
  1. Each P(i,j) has at most one color selected, so:
Sum(P(i,j,k)) <= 1 for all k
  1. Each 8x8 tile should have at least one palette that contains the colors used on it:
For tile T in tiles:
    And(P(i,j,c)=1 for c in colors(T))=1 for some i and j

However, we don't even have to code this up to there's a monstruous amount of variables, it would take forever to run this. The breakthrough is that most images I download from the web have a limited number of colors anyway so we can restrict the problem a lot by considering only colors that are actually used.

First I do a pass over the image and create a sorted list AllColors of all unique 15-bit colors present in the image. We have as output variables P(i,j) booleans where again i is the palette index but j in the index on AllColors (>=0 and < #AllColors). For instance, P(5,10)=1 means that the 10th color on AllColors is used on the 5th palette. So we reduced the number of boolean variables for each color from 32768 to #AllColors! This makes it tractable.

P_ = 16 # maximum number of palettes
C_ = len(all_colors)
Pvars = [[z3.Int('p%d%d' % (p,c)) for c in range(C_)] for p in range(P_)]

Now we have to find P(i,j) such that the following 4 conditions are satisfied:

  1. Pij can only be zero or one
for p in range(P_):
    for c in range(C_):
        solver.add(z3.Or(Pvars[p][c] == 0, Pvars[p][c] == 1) == True)
  1. Each palette has 16 colors at most
for p in range(P_):
    sum_ = 0
    for c in range(C_):
        sum_ += Pvars[p][c]
        solver.add(sum_ <= 16)
  1. Each 8x8 tile should have at least one palette that contains the colors used on it
for g in tile_palletes:
    pallete_is_match = False
    for p in range(P_):
        GxP = True
        for color in g:
            GxP = z3.And(GxP, Pvars[p][all_colors.index(color)] == 1)
        pallete_is_match = z3.Or(pallete_is_match, GxP)
    solver.add(pallete_is_match)
  1. Each palette should include the transparent color.
for p in range(P_):
    solver.add(Pvars[p][transparent_index] == 1)

And solve!

r = solver.check()
if r != z3.sat:
    print("There's no solution")
else:
    m = solver.model()
    for p in range(P_):
        for c in range(C_):
            v = m[Pvars[p][c]].as_long()
            color = all_colors[c]
            if v: print("Pallete %d, color %d, used" % (p,color))

And this works! Now, back to making that game :)