Solving Myst Puzzles with Z3

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 Actions, 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, middle and bottom 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, shifting 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_ion 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 Actions 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 Actions.

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 Actions 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;).