# Solving Myst Puzzles with Z3

### How I Got Nerd-Sniped Playing VR Myst over Christmas

Posted on December 29, 2021 by Eric Hayden Campbell, debugging help by Frances Campbell

So my sibling, Frances, has a sweet new VR set, and as a family we spent a bunch of time over Christmas nerding out playing Half Life: Alyx, Beat Saber, and Myst. It was a great time! As we were playing, I got nerd-sniped by implementing one of the puzzles in VR Myst. Here’s the puzzle and my Z3 implementation of the solution.

Warning: Minor Spoilers for Myst

One of the early puzzles in Myst is to rotate a set of 3 vertically-stacked gears to a desired using a pair of levers. Once you find the desired combination from the environment (it’s 2-2-1), the trick is to pull the two levers to move the three gears into that position. The catch is that the left lever moves the top two gears up one and the right lever moves the bottom two gears up one. Holding either lever down causes the middle gear to move after the original simultaneous rotation.

So, being the nerd I am, this seemed like a fun cheesy SMT problem. So, I spent the rest of the evening not paying attenion to the game and hacking together an SMTLIB implementation, much to the chagrin of my family. My Dad (who was in the Index) solved the actual problem in only a few minutes, but I wanted to flex my Z3 muscles.

### The Datatypes

First, I wrote down the Datatypes for the problem. A `Gear` is an enum with values `one`, `two`, or `three` as below:

``````(declare-datatype ((Gear 0))
(( (one) (two) (three) )))``````

Then the user can take one of three `Action`s, pull the right lever (`PullRight`), pull the left lever (`PullLeft`), or `Hold` the previouly pulled lever down. I added a `Noop` action to give the solver a bit more freedom in finding solutions.

``````(declare-datatype ((Action 0))
(( (PullLeft) (PullRight) (Hold) (Noop) )))``````

Finally, I wrote down a triple, `Gears` representing the `top`, `mid`dle and `bot`tom gears.

``````(declare-datatypes ((Gears 0))
(( (gears (top Gear) (mid Gear) (bot Gear)) )))``````

### The Semantic Operations

With the datatypes in hand, I wrote down the functions that perform the specific actions. First I defined a helper function `shift` that shifts the gear using plus-1-mod-3 arithemetic:

``````(declare-fun shift ((g Gear)) Gear
(if (= one g) two
(if (= two g) three one)))``````

Now, it’s easy to use these to implement the behavior of pulling the left and right levers, by shifting the appropriate gears. The `left` and `right` functions are defined below.

``````(define-fun left ((g Gears)) Gears
(gears
(shift (top g))
(shift (mid g))
(bot g)))

(define-fun right ((g Gears)) Gears
(gears
(top g)
(shift (mid g))
(shift (bot g))))
``````

Then the `hold` function, which corresponds to holding down the previously-pulled lever is defined similarly, `shift`ing only the middle one.

``````(define-fun hold ((g Gears)) Gears
(gears
(top g)
(shift (mid g))
(bot g)))``````

### The Transition System

Now, in order to turn this into a synthesis problem, where the solver decides what actions to execute, we need interpret the `Action` datatype. There are a few ways to do this, `define`-ing the function, `declare`-ing it, or `declare`-ing it as a relation and `assert`-ing the funcitonal constraint. My first attempt was to just `define` it, but this triggered a known bug relating to inverted argument order in computing the model.

Instead, I had to declare the interpetation function, called `action`, and specify it. For the cleanliness of specifying the transition system, I wrote it as a relation with a functional assertion.

So we define `action` to be a relation with the following type:

``(declare-fun action (Action Gears Gears) Bool)``

Here, the `Action` argument is the action being interpreted, the first gear `g` is the input, and the second is the output.

I enforced the requisite functional constraint in the standard way. It says that for any action `a` and gear-triple `gin`, if `(action a gin gout1)` and `(action a gin gout2)` hold for gear triples `gout1` and `gout2` the it must be that `gout1` and `gout2` are equivalent.`

``````(assert (forall ((a Action) (gin Gears)
(gout1 Gears) (gout2 Gears))
(=> (action a gin gout1)
(action a gin gout2)
(= gout1 gout2))))``````

Now, we can write the specification. of `action`, which is just that if the action is `PullLeft` (`PullRight`), then the output gear is the result of calling `left` (`right`) on the input gear. Similarly, if the action is `Hold` then the output gear is the result of calling `hold` on the input gear. Finally, if the action is `Noop` then the input and output gear are the same:

``````(assert (forall ((a Action) (g Gears))
(and (=> (= PullLeft a) (= (takeAction a g) (left g)))
(=> (= PullRight a) (= (takeAction a g) (right g)))
(=> (= Hold a) (= (takeAction a g) (hold g)))
(=> (= Noop a) (= (takeAction a g) g)))))``````

### Solving Myst’s Gear Puzzle

To use this machinery to solve Myst’s gear puzzle, I decided to use an approach related to bounded model checking. That is, first I try to solve the problem using 1 action, then two then three, until Z3 gives me a solution.

First, we need to declare the actions, and the intermediate gear states. It will turn out that we’ll only need six, so we’ll only declare that many

``````(declare-const act1 Action)
(declare-const act2 Action)
(declare-const act3 Action)
(declare-const act4 Action)
(declare-const act5 Action)
(declare-const act6 Action)

(declare-const g0 Gears)
(declare-const g1 Gears)
(declare-const g2 Gears)
(declare-const g3 Gears)
(declare-const g4 Gears)
(declare-const g5 Gears)
(declare-const g6 Gears)``````

Now we can write down the transitions that make `g_i` the result of executing `act_i`on gear `g_i-1`:

``````(assert (action act1 g0 g1))
(assert (action act2 g1 g2))
(assert (action act3 g2 g3))
(assert (action act4 g3 g4))
(assert (action act5 g4 g5))
(assert (action act6 g5 g6))``````

Also, to obey the semantics of the game, we need the `Hold` action to only occur after another action has occured (If no lever has been pulled, we can’t hold it down). My initial thought was to enforce this using a big disjuntion on the six actions, but Frances pointed out that it suffices to just ensure that the first action isn’t `Hold`. Its a little tricky to justify in the presence of `Noop`, because a `Hold` following a `Noop` is hard to realize. However, remembering that `Noop` is really the absence of an operation, rather than an operation that does nothing, i.e. that `PullLeft Noop Hold` is equivalent to `PullLeft Hold`.

All this is to say that we add the following assertion to prevent bogus action sequences:

``(assert (not (= act1 Hold))``

So now we can compute the problem instance by just setting the start state to 3-3-3, which was the start state in the game, and the final state to the solution, 2-2-1. Now you can see why its important to have a `Noop` operation. It might be the case that there is a solution that takes only 3 operations! If we care about the minimal solution, then we need that facility.

``````(assert (= g0 (gears three three three)))
(assert (= g6 (gears two two one)))``````

Then we can compute the solution!

``````(check-sat)
(get-value (act1 act2 act3 act4 act5 act6))``````

which is

``````((act1 PullRight)
(act2 Noop)
(act3 PullLeft)
(act4 Hold)
(act5 PullLeft)
(act6 Hold))``````

Notice that the last action here is `Noop`! This means that we can actually get a solution in 5 actions. We can try this using the following commands

``````(check-sat)
(assert (= g0 (gears three three three)))
(assert (= g5 (gears two two one)))
(get-value (act1 act2 act3  act4 act5))
``````

Which gives the solution:

``````sat
((act1 PullLeft)
(act2 PullRight)
(act3 Hold)
(act4 PullLeft)
(act5 Hold))``````

Which gives us a solution in 5 moves!

This model-checking behavior made me wonder about generalizing this problem. How many moves do you need to get from any starting state to any ending state?

### Generalizing

Formally, I want to know what the smallest number `N` is such that, for any starting gear state `start` and ending gear state `end`, we can always find a action sequence of length `N`.

We’ll do this by slowly increasing the number `N` until we find a value that works. We formalize the problem by dualizing it for a given `N`. That is, we will attempt to find a pair of gear states, `start` and `end` such that there is no sequence of `N` `Action`s that transforms `start` into `end`. If this query is `sat`, it gives us a pair of start and end states that require more than `N` moves to solve. Whereas if it returns `unsat` it says that no more than `N` `Action`s.

From the concrete Myst problem instance, we know that we need at least 5 actions, otherwise the pair (`start=3-3-3`, `end=2-2-1`) is an unsolvable problem. Let’s start with the hypothesis that 5 actions are sufficient.

In this version of the problem, we use a functional declaration rather than a relational one to reduce the number of quantified variables we need. (If we used the above relational approach we would need a new variable for every intermediate state). We call this `takeAction` instead of `action`.

``````(declare-fun takeAction (Action Gears) Gears)
(assert (forall ((a Action) (g Gears))
(and (=> (= PullLeft a) (= (takeAction a g) (left g)))
(=> (= PullRight a) (= (takeAction a g) (right g)))
(=> (= Hold a) (= (takeAction a g) (hold g)))
(=> (= Noop a) (= (takeAction a g) g)))))``````

Now we can test whether 5 `Action`s are sufficient by checking the following query:

``````(declare-const start Gears)
(declare-const end Gears)
(assert (forall ((a1 Action)
(a2 Action)
(a3 Action)
(a4 Action)
(a5 Action))
(not (= end
(takeAction a5
(takeAction a4
(takeAction a3
(takeAction a2
(takeAction a1 start)))))))))
(check-sat)
(get-value (start end))``````

But this is insufficient! Giving us the output

``````sat
((start (gears one one one))
(end (gears three one three)))``````

I haven’t tried to come up with a solution to check that it actually is impossible in 5 operations, but (for better or for worse) I believe Z3.

So it seems that we need at least 6. Let’s check:

``````(assert (forall ((a1 Action)
(a2 Action)
(a3 Action)
(a4 Action)
(a5 Action)
(a6 Action))
(not (= end
(takeAction a6
(takeAction a5
(takeAction a4
(takeAction a3
(takeAction a2
(takeAction a1 start))))))))))
(check-sat)``````

Z3 outputs

``unsat``

Which lets us conclude that 6 operations are sufficient, which seems sensible, since the search space is small. I could think about this carefully and prove something about this, but I’ll leave that as an exercise for the reader;).