Of Dungeons, Dragons and SAT-Solvers

I love to work on my roguelike game in my spare time. Of course there is no end in sight and it will probably not be playable for months or years to come. But on the way, I always encounter some interesting problems. Most of them can be easily solved with some monkey work, but a few call for logic programming and the sledgehammer that is MiniSat.

A graph embedding problem appears

Imagine you have procedurally generated a dungeon. So you basically generated a list of structures representing rooms of the dungeon and their connections (aka doors).

export type RoomId = number
export interface Room {
  id: RoomId
  connections: RoomId[]
}

Now you know that on the current level there should be some rooms filled with enemies and loot. There should also be a shop near the entrance. Next to the shop, a random encounter that gives a side quest. And a dragon that guards the treasure room.

You start building descriptions for each of these structures. And try to fit them randomly into your dungeon. At first it is easy. Just decide for each room, what kind of filling it needs. A room near the entrance: Shop! A room somewhere inside the dungeon: Throw a d20, add some enemies, et voilà full dungeon. But then you try to fit the dragon in your dungeon. Now you have to look out, that there is a treasure room next to the dragon. And the treasure room should have only one entrance. Oh, and there should be only one shop. And not more than eight rooms filled with enemies...
Your code is starting to become more and more tangled and complex.

Let us step back for a moment and think about the problem in more abstract terms. The dungeon represents a graph G. The nodes are rooms and the edges are the doors. The descriptions of room fillings are also a graph H. The nodes are individual room fillings (e.g. a dragon, a treasure room, some enemies) and the edges bind them together. An edge between a dragon node and a treasure room node represents the restriction that they are directly connected.

Now to fill the empty dungeon with interesting content you only have to find an embedding of H in G!

You shall not SAT

You might say that restating the problem with a graph does not solve anything. But it helps in viewing the problem as a mathematical one. At its core it is just the embedding problem and every additional rule adds restrictions on how this embedding should be done. So each rule reduces the pairs of nodes in H and G that are allowed in a correct embedding.

A possible way to solve this problem is to represent it as a boolean satisfiability problem. Yes this problem is NP-hard but there exist a lot of SAT-Solvers that can handle problems far larger than our little dungeon. The devs at meteor even packaged the famous MiniSat solver using Emscripten on npm so you can solve SAT-Problems inside your browser!

Now let us represent the problem in SAT using Typescript!

First we introduce variables. We need a variable for each possible pair of nodes and write a little function that gives each v in G and w in H a unique name.

function createLabel(v: number, w: number): string {
  return `${v}_${w}`
}

Now for the actual rules of the embedding. The first rule is that each node in H can only be mapped to one node in G. That means if we have one dragon in H there shall only be one dragon in G. And if we need ten random ruffian-filled rooms, we need to put ten nodes in H that represent that. As a logical expression this may look like this

$C_{vw} \Rightarrow \bigwedge\limits_{i \neq v}^{v \in H} \lnot C_{iw}$

Written out this means: "If v is mapped to w then for all nodes i (that are not v) there is no mapping from i to w". For a SAT Solver to understand this rule, we need to transform it into conjunctive normal form (CNF) first. Now with material implication

$\lnot C_{vw} \lor [ \bigwedge\limits_{i \neq v}^{v \in H} \lnot C_{iw} ]$

and with the law of distributivity

$\bigwedge\limits_{i \neq v}^{v \in H} ( \lnot C_{iw} \lor \lnot C_{vw} )$

we can reach CNF. If you look closely at the above formulas you might notice that there is a trivial solution that satisfies them. When all variables are false! The formula expresses at least once and we additionally assert

$\bigwedge\limits^{v \in H} [ \bigvee^{w \in G} C_{vw} ]$

that for each node in H there must be a mapping to a node in G to make it exactly one.

Luckily, the logic-solver package has already a bunch of helper functions to create common logical expressions and this one is exactlyOne(). That means there is no need to put any more math formulas in this post 🤓.

  // each w in H on exactly one v in G
  H.V.forEach(w => {
    const Cvw = G.V.map(v => createLabel(v, w))
    solver.require(exactlyOne(...Cvw))
  })

This looks simple enough and solving this problem by running solver.solve() will even yield a solution! After mapping the variable assignments back to the graph embedding you realize that each node in H is mapped to the exact same node in G. Which means that all enemies, shops and dragons are being put into the same room. That would mean no backtracking and yack shaving, and that is the whole point of dungeon crawling. So let us write an additional rule to achieve that!

  // each v in G can map to at most one w in W
  G.V.forEach(v => {
    const Cvw = H.V.map(w => createLabel(v, w))
    solver.require(atMostOne(...Cvw))
  })

This looks very similar to the rule we created above, except that we are now coming from nodes in G to nodes in H and use the atMostOne() helper (we already derived the formula above). Each room of our dungeon now has at most one room mapped to it from H. The solver will fill our dungeon and keep dragons separated from shopkeepers.

Still the dragon is not sitting next to the treasure room, because we have yet to use the edges of H! Let us try to put into code that the neighbourhoods in H are also mapped to G.

  // all neighbours in H are mapped to neighbours in G
  H.V.forEach(w => {
    G.V.forEach(v => {
      const Cvw = createLabel(v, w)
      H.E.forEach(e => {
        const j = traverseEdge(e, w)
        if (j !== undefined) {
          const Cij: string[] = []
          G.E.forEach(f => {
            const i = traverseEdge(f, v)
            if (i !== undefined) {
              Cij.push(createLabel(i, j))
            }
          })
          solver.require(or(not(Cvw), ...Cij))
        }
      })
    })
  })

There is a lot going on here. The first two forEach statements are just to select each possible mapping of node pairs v and w. We use a simple function traverseEdge to find neighbours of nodes. Then for each neighbour j of w in H we create a new restriction. Now we look at each neighbour i in G of v. And we can finally state that if there is a mapping from v to w there must be a mapping from i to j.

Oh, you can imagine the fun that went into testing that code!

Conclusion

I presented only the bare essentials of my room embedder and a lot is still missing. There is for example no concept of an entrance to the dungeon and how deep a room is inside of it. Also rooms might be too small for a dragon or not close enough to the shop. But we can always create new restrictions and modify existing ones to meet our changing needs.

We can refine the solution on multiple levels. The first way is just to add more rules to the problem and to modify the graphs accordingly. But we can also extend the graph nodes with labels, remove nodes from G or modify H. It may also be a good idea to randomize the order of the rooms in G. And a crucial one is to run multiple embedding phases. The first phase to add the must-haves of the level. Dragons, shops, treasures. With the second run you add additional content like side quests. And during the last passes you can add monsters and decorations that can fill the gaps between the more engaging and complex content.

I guess, you can take it from here. Or get inspired to consider some logic programming for your own problems.

I hope you had as much fun learning about SAT solvers as me writing down those formulas in latex. This post was sponsored by itemis AG. That's the place where I work and drink.

Comments

[adelinb]

Hello, great article, im really interested in the use of SAT solver in browsers
But It seems that dev.to does not preview math expression in a pretty way, you might want to fix this