Solving Zelda Puzzles Satisfactorily

By: on June 1, 2018

In the game Breath of the Wild, there’s a puzzle which in­volves a set of fans and tur­bines in a 4×5 grid, and you must po­s­i­tion the fans in order en­sure all of the tur­bines are spin­ning. Un­for­tu­nately, I’ve never really had much pa­tience for solving this kind of logic puzzle the old fash­ioned way, so given that com­puters are good at this sort of thing, I thought I’d try that.

Now, we can ex­press this problem as a boolean al­gebra prob­lem. Given that we have some set of vari­ables and some con­straints (ie: the fan po­s­i­tions and dir­ec­tions), how do we en­sure all of these vari­ables are set to true?

Hap­pily, this kind of problem can be given to a Sat­is­fiab­ility solver to solve. The only re­maining ques­tion is … how do we teach it to solve the prob­lem?

So, we know that in our prob­lem, each fan can only ever be fa­cing in one dir­ec­tion at once.

So that leaves us with two prob­lems: En­suring that each fan only blows in a single dir­ec­tion, and en­suring that all tur­bines are pro­pelled by some fan.

We know that all of the tur­bines on the line from the fan in the dir­ec­tion of air flow will be spin­ning. So, if we have a trivial 1×2 grid, with a Fan in (0, 0) and a tur­bine at (1, 0); we can in­tuit that the tur­bine will only be spin­ning if the fan is fa­cing east, ie: the wind flows with a dir­ec­tion of (1, 0).

So, given that we know the grid size and fan loc­a­tions ahead of time, we can notate this prob­lem:

as fol­lows:
Fan(0, 0, E) => Tur­bine(1, 0)

ie: A fan at 0, 0 will propel the tur­bine at 1, 0. Now, in a setup with two fans, say an­other one at (3, 0):

Can be ex­pressed as:

Fan(0, 0, E) => Tur­bine(1, 0) & Tur­bine(3, 0)
Fan(2, 0, E) => Tur­bine(3, 0)
Fan(2, 0, W) => Tur­bine(1, 0)

(the or­dering of the tur­bines here doesn’t par­tic­u­larly mat­ter; it’s mostly in­cluded for con­veni­ence).

Now, this is fine, but there’s one small hitch; our solver will only ac­cept input in Con­jun­ective Normal Form (CNF for short). so, we can say that “(A ∨ ¬B) ∧ (A ∨ B)”, for ex­ample. However, be­cause we know that all of the tur­bines have to be spin­ning, we don’t need to ex­pli­citly de­note them in the de­scrip­tion we pass to the solver (ie: we don’t need to create vari­ables for them), we can simply as­sert the con­di­tions that make them up. In this case, this would be a union of the fans that blowing over that given po­s­i­tion.

# Tur­bine(1, 0)
Fan(0, 0, E) ∨ Fan(2, 0, W)
# Tur­bine(3, 0)
Fan(0, 0, E) ∨ Fan(2, 0, E)
...

And so on. as you can tell, this can get quite te­dious to do by hand. Hap­pily, we can make the com­puter do the boring bits for us. I’ve used the lib­rary pycryptosat to do this. I’m not going to in­clude snip­pets here, since the code

I wrote is hardly ex­em­plary, but can be found in a gist.

The other part of the problem is making sure that each fan only points in a single dir­ec­tion. We can say that a solu­tion is in­valid iff a fan is point­ing, say, North and East at once. The py­thon that does this is as fol­lows:

class Fan(ob­ject):
    def __in­it__(self, name, solv­er):
        self.name = name
        fvar = nex­t_­free_var(­solver)
	# North, East, South and West are just off­sets into our list of vari­ables.
        self.nesw = range(fvar, fvar+4)
        
	# For each pair of dir­ec­tions, as­sert that they can't both be set.
	# We as­sert that ¬(d0 ∧ d1); which via De-­Mor­gan's laws, can be written as:
  # (¬d0 ∨ ¬d1).
  # This com­mutes, so (¬d0 ∨ ¬d1) is the same as (¬d1 ∨ ¬d0), and we can avoid
  # adding it in twice.
        clauses = [[-d0, -d1] for d0 in self.nesw for d1 in self.nesw  if d0 > d1]
        #print clauses
        solv­er­.ad­d_clauses(clauses)

    def show(self, solu­tion):
        re­turn "{}:{}".format(
            self.name, ",".join(d for v, d in zip(self.nesw, "NESW") if solu­tion[v]))

    def __re­pr__(self):
        re­turn "<­Fan: {};{}>".format(self.name, self.nesw)

So when we ini­tialize a Fan ob­ject, we pass it some­thing to identify it (a tuple of co­ordin­ates, in this case), create some fresh vari­ables in the solver for each dir­ec­tion, and then as­sert to the solver that the fan will only ever spin in one dir­ec­tion.

We then ask the solver for a set of solu­tions. Ef­fect­ively, the solver will only re­turn one solu­tion at a time, but we then add a clause that will mean that the pre­vious solu­tion isn’t valid any more. And thus when the solu­tions are ex­hausted, the solver will say that the ori­ginal problem ex­cluding the pre­vi­ously given an­swers is un­sat­is­fiable.

The solver in use will output an as­sign­ment of all vari­ables to either true or false. The Fan#show method above can then lookup how each vari­able for each dir­ec­tion has been as­signed, and dis­play the dir­ec­tions that are set to true. The reason output all of the dir­ec­tions that match is as an in­ternal conm­s­ist­ency check. In this case, it’s easy enough to see when a fan is either not blowing in any dir­ec­tion, or mul­tiple dir­ec­tions (both quite im­possible).

So, we can build an IPy­thon Note­book to glue everything to­gether, and we find it will output a single solu­tion. Checking this by hand, we find that all of the tur­bines are covered by wind from a fan, thus solving the shrine puzzle, and granting ac­cess to the Monk and their spirit Orb.

Share

Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>

*