Of Dungeons, Dragons and SAT-Solvers
Tags: computerscience, typescript, tutorial, gamedev
Published: 2020-04-01 13:13:11

I love to work on my [roguelike game](https://github.com/dvallin/tlb-js) 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](http://minisat.se/).

# 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).

```typescript
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](https://en.wikipedia.org/wiki/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](https://www.meteor.com/) even packaged the famous [MiniSat](http://minisat.se/) solver using [Emscripten](https://emscripten.org/) on [npm](https://www.npmjs.com/package/logic-solver) 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.

```typescript
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

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

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)](https://en.wikipedia.org/wiki/Conjunctive_normal_form) first. Now with [material implication](https://en.wikipedia.org/wiki/Material_implication_(rule_of_inference))
{% katex %}
  \lnot C_{vw} \lor \[ \bigwedge\limits_{i \neq v}^{v \in H} \lnot C_{iw} \]
{% endkatex %}
and with the law of distributivity
{% katex %}
  \bigwedge\limits_{i \neq v}^{v \in H} \( \lnot C_{iw} \lor \lnot C_{vw} \)
{% endkatex %}
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
{% katex %}
  \bigwedge\limits^{v \in H} \[ 
  \bigvee^{w \in G} C_{vw} \]
{% endkatex %}
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 :nerd_face:.

```typescript
  // 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!

```typescript
  // 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_.

```typescript
  // 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](https://en.wikipedia.org/wiki/Constraint_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](https://www.itemis.com/en/). That's the place where I work and drink._