Solving a puzzlehunt with Satisfiability Modulo Theories

Z3 is a Satisfiability Modulo Theories (SMT) solver. One can think of it as a tool that can take systems of human-understandable equations and find solutions for them by reducing them to SAT instances, then efficiently solving the SAT instances. In practice, Z3 allows you to easily solve complex optimization problems without needing to deeply understand the problem and develop your own heuristics or solution. This makes it a valuable tool in your arsenal for exploring new problem spaces, and I'm going to walk through an example where I've used it (via Python bindings) recently.

Note that although I've solved various problems with Z3, I'm definitely not an expert at it and am likely doing things inefficiently. If you're interested in trying it yourself, I'd recommend starting at with official references, rather than my words.

Solving a puzzlehunt problem

In late 2020, I played in Teammate Hunt with some friends, and one of the questions that stuck out was Icebreaker. In this question, the five partygoers are playing an icebreaker where they say two truths and a lie, and we apparently need to derive the correct set of facts about each of the participants. While it would be possible to do this by hand, it would be rather tedious. What if we could quickly write a program to decipher this system for us? Enter Z3...

First, we need to determine what information we're looking for. We note there are five partygoers, each of which is associated with a unique city, pet, and house on their block (apparently they're all neighbors). Additionally, we can look at each one of these categories on its own.

We know each entry in a category appears exactly once, and we know each person can only have one entry in each category, so we can start encoding the structure of this problem into Z3. In Z3, BoolVectors represent a set of boolean variables that we'd like to find valid values for. 

names = ["Sandra", "Walter", "Turner", "Ramsey", "Martin"]
cities = ["London", "Taipei", "Kansas", "Mumbai", "France"]
pets = ["Robins", "Whales", "Ferret", "Poodle", "Tigers"]
houses = ["1", "2", "3", "4", "5"]

# Vector of constraints indexed by name
city_vars = [BoolVector("city_{}".format(c), len(names)) for c in cities]
pet_vars = [BoolVector("pet_{}".format(p), len(names)) for p in pets]
house_vars = [BoolVector("house_{}".format(h), len(names)) for h in houses]

Our goal is to find a valid assignment of these variables that meets the constraints given in the problem. We can start with some general uniqueness constraints. Note that If(expr, t, f) in Z3 is a ternary expression (expr ? t : f in most languages). 

solver = Solver()

# Each person must have exactly one city membership
for city_var in city_vars:
  solver.add(Sum([If(x, 1, 0) for x in city_var]) == 1)
# Across all of the partygoers, each city must have exactly one member
for i, name in enumerate(names):
  solver.add(Sum([If(x[i], 1, 0) for x in city_vars]) == 1)

# ... Repeats for the other categories ...

Now, we've encoded what we want the structure of this problem to look like — each category should have its entries assigned to unique partygoers. However, we still need to encode the remainder of the information we've been given, such as the two truths and a lie each partygoer has provided. To encode this, we'll want one key function. 

# Given three statements, this is satisfiable if any two of them are satisfiable.
def two_of_three(a,b,c):
  return Or([
    And(a, b),
    And(a, c),
    And(b, c)
  ])

To understand what two_of_three will do, it's easiest to think of Z3 as trying various assignments of variables to see what works. We provide the constraints for how they're assigned, and Z3 either says that the constraints can't be met, spins forever trying to solve the NP-complete SAT problem (rarer than you might expect!), or manages to find a solution for us. With two_of_three, we're encoding that the problem is satisfiable if any two of the three inputs were true under Z3's current variable assignment.

Finally, to simplify our implementation before we start encoding truths and lies using all of this, we'd like a couple helpers. 

# Map each category name to the set of Z3 boolean vectors representing it
types = {
  "city": (cities, city_vars),
  "pet": (pets, pet_vars),
  "house": (houses, house_vars)
}

# Given a category, an item, and a name, return the corresponding Z3 boolean.
def into(typ, item, name):
  (key, varlist) = types[typ]
  return varlist[key.index(item)][names.index(name)]

Putting it all together

Now, we're ready to encode our truths and lies! For each of the partygoers, we'll add a separate Z3 constraint for their statements using two_of_three. For ease of reading, I've put the statement we're encoding above each section of corresponding code. 

# Martin's two truths and a lie
solver.add(two_of_three(
  # STATEMENT: The five of us are, in no particular order, the person who lives
  # in the first house, RAMSEY, the person who has a pet FERRET, the person who
  # has a pet POODLE, and the person from KANSAS.
  And([
    # We know Ramsey doesn't have any of the other traits mentioned
    into("house", "1", "Ramsey") == False,
    into("pet", "Ferret", "Ramsey") == False,
    into("pet", "Poodle", "Ramsey") == False,
    into("city", "Kansas", "Ramsey") == False,
  ] + [
    # We know anyone who has one of these traits must not have the others.
    Implies(
      Or(into("pet", "Ferret", person), into("pet", "Poodle", person)),
      And(
        into("city", "Kansas", person) == False,
        into("house", "1", person) == False
      )
    )
    for person in names
  ]),

  # STATEMENT: TURNER and the person who owns WHALES live on opposite
  # ends of the street.
  And(
    # Turner doesn't own whales, and either lives in the first or last
    # house on the block.
    And(
      into("pet", "Whales", "Turner") == False,
      Or(
        into("house", "1", "Turner"),
        into("house", "5", "Turner")
      )
    ),
    And([
      # Whoever owns whales also lives in the first or last house on the block.
      Implies(into("pet", "Whales", person),
        Or(
          into("house", "1", person),
          into("house", "5", person)
        )
      ) for person in names
    ])
  ),

  # STATEMENT: WALTER is from FRANCE, but doesn't own a FERRET.
  And(
    into("city", "France", "Walter"),
    into("pet", "Ferret", "Walter") == False
  )
))

# ... Repeats with the information for each partygoer ...

In the above code, we added a constraint that at least two of the statements given must be true, then encoded each statement into operations on the boolean variables we defined earlier. The logic ends up surprisingly understandable, since Z3 in Python reads fairly closely to propositional logic.

With our constraints from the problem encoded, all that remains is to compute a solution! 

assert str(solver.check()) == "sat"
solutions = solver.model()

With some fancy printing, we now know the truth about each of the devious partygoers: 

             Sandra    Walter    Turner    Ramsey    Martin
-----------  --------  --------  --------  --------  --------
city_France                                          X
city_Kansas                      X
city_London  X
city_Mumbai                                X
city_Taipei            X
house_1                X
house_2                                    X
house_3                                              X
house_4      X
house_5                          X
pet_Ferret                                           X
pet_Poodle   X
pet_Robins                                 X
pet_Tigers                       X
pet_Whales             X

Try it yourself!

Though this was only a fun example, Z3 has various practical uses. It's similarly great at classes of CTF problems, can be used for one-off optimization attempts, and has been used in major projects like compilers. Next time you'd like a solution for a nontrivial system of equations, consider trying Z3!

Other articles