Solving Knight-Knave-Spy Puzzles with Z3
Three people (X,Y,Z) are in a room with you. One is a knight (knights always tell the truth), one is a knave (knaves always lie), and the other is a spy (spies may either lie or tell the truth). X says, “Z is a knave.” Y says, “X is a knight.” Z says, “I am the spy.”
What role is each person (Knight, Knave, Spy)?
These Knight-Knave-Spy problems are fairly simple logic puzzles. To solve the one given above, first notice that both Y and Z claim to not be the knight, thus X must be the knight. Then, because the knight tells truth, Z must be the knave and Y must be the spy. So the only valid solution is that (X,Y,Z) are (Knight, Spy, Knave).
Problems like this are simple enough as mental exercises, yet have enough depth to motivate solving with a computer. To solve this problem, we will use Python and Z3, which is a SAT solver, or boolean satisfiability solver. SAT solvers take a list of constraints and find the conditions (if any) in which they all are valid. For example, a constraint in any knight-knave-spy problem is: “if X is a Knight, then X must tell the truth.”
We start by declaring a bunch of Z3’s boolean variables. Each person (X,Y,Z) has variables tracking whether they are the knight, knave, spy, and whether they are truthful. At this point there are no constraints, so a person X can simultaneously be the knight, be the knave, and be telling the truth; we’ll fix this later.
from z3 import Bool, And, Solver, Not, Or, Implies, sat
def main():
s = Solver()
x_is_k = Bool("x_is_k")
x_is_n = Bool("x_is_n")
x_is_s = Bool("x_is_s")
y_is_k = Bool("y_is_k")
y_is_n = Bool("y_is_n")
y_is_s = Bool("y_is_s")
z_is_k = Bool("z_is_k")
z_is_n = Bool("z_is_n")
z_is_s = Bool("z_is_s")
x_t = Bool("x_truth")
y_t = Bool("y_truth")
z_t = Bool("z_truth")
...
We add constraints to the solver (s) by using s.add(...).
The simplest constraint is simply a boolean variable.
If we know that X is telling the truth, then we could add s.add(x_t).
We can similarly create a constraint saying “X is Knight, then X is truthful” with the Implies function.
The Implies constraint means: if the left side is true, the right side must also be true.
More familiar boolean operations Not, Or, And are also available.
...
# knaves cannot tell the truth
s.add(Implies(x_is_n, Not(x_t)))
s.add(Implies(y_is_n, Not(y_t)))
s.add(Implies(z_is_n, Not(z_t)))
# knights tell the truth
s.add(Implies(x_is_k, x_t))
s.add(Implies(y_is_k, y_t))
s.add(Implies(z_is_k, z_t))
...
At this point knights won’t lie, and knaves won’t tell the truth, we it’s still valid for multiple people to simultaneously be the knight; and it’s still valid for a single person to be a knight and a spy.
To solve this, we must add constraints that only one of the people can be any specific role, and that any person can only be one role.
We do this with a custom one_of_each function to simplify the logic:
def one_of_each(a, b, c):
# exactly one of the three must be true
return Or(And(a, Not(b), Not(c)),
And(Not(a), b, Not(c)),
And(Not(a), Not(b), c))
Then, we add the one of each constraints:
...
# Each role (knight, knave, spy) is only taken by one person (X, Y, Z)
s.add(one_of_each(x_is_k, y_is_k, z_is_k))
s.add(one_of_each(x_is_n, y_is_n, z_is_n))
s.add(one_of_each(x_is_s, y_is_s, z_is_s))
# Each person can only take one role
s.add(one_of_each(x_is_k, x_is_n, x_is_s))
s.add(one_of_each(y_is_k, y_is_n, y_is_s))
s.add(one_of_each(z_is_k, z_is_n, z_is_s))
...
And the problem-specific constraints:
...
# Problem constraints
# X says, "Z is a knave."
s.add(x_t == z_is_n)
# Y says, "X is a knight."
s.add(y_t == x_is_k)
# Z says, "I am the spy."
s.add(z_t == z_is_s)
...
Finally, some boilerplate code to find whether the system of constraints has any valid solutions, and then list them if they exist:
...
while s.check() == sat:
model = s.model()
pretty_print(model)
if not model:
break
# Find solutions which are different than the current solution
s.add(Not(And([v() == model[v] for v in model])))
def pretty_print(model):
model_values = {}
for constraint in model:
model_values[constraint.name()] = bool(model[constraint])
for c in ["x", "y", "z"]:
for r in ["k", "n", "s"]:
if model_values[f"{c}_is_{r}"]:
print(f"{c.upper()} is {r}, ", end="")
print()
main()
This prints “X is k, Y is s, Z is n,” as expected.
More problems
The neat thing about this (and a justification for all this work) is that we can easily modify the solver constraints to solve any knight-knave-spy problem. Here’s another:
… X says something, but you could not hear it. Then Y says, “X said that he is the knave.” and Z says, “I am the knave.”
What role is each person (Knight, Knave, Spy)?
...
# Problem constraints
# Y says, "X said he is the knave."
s.add(y_t == Or(And(x_t, x_is_n), And(Not(x_t), Not(x_is_n))))
# Z says, "I am the knave."
s.add(z_t == z_is_n)
Which results in “X is k, Y is n, Z is s.” Another problem:
… X says, “I am not a spy.” Then Y says, “I am a spy.” And finally Z says, “Y is lying.”
What role is each person (Knight, Knave, Spy)?
# Problem constraints
# X says, "I am not a spy."
s.add(x_t == Not(x_is_s))
# Y says, "I am a spy"
s.add(y_t == y_is_s)
# Z says, "Y is lying"
s.add(z_t == Not(y_t))
Which has three solutions: (knight,knave,spy), (spy, knave, knight), (knight, spy, knave). Another problem:
… X says, “I am 50 years old.” Then Y says, “X is either 50 years old or a knight.” And finally Z says, “X is either 50 years old or a knave.”
What role is each person (Knight, Knave, Spy)?
This problem is ambiguous: Inclusive Or or Exclusive Or? Trying Xor:
# Problem constraints
x_50_years_old = Bool("x_50_old")
# X says, "I am 50 years old."
s.add(x_t == x_50_years_old)
# Y says, "X is either 50 years old or a night."
s.add(y_t == Xor(x_50_years_old, x_is_k))
# Z says, "X is either 50 years old or a knave"
s.add(z_t == Xor(x_50_years_old, x_is_n))
We see that there exist two solutions: (knight, knave, spy) and (knave, spy, knight). However, with inclusive or:
# Problem constraints
x_50_years_old = Bool("x_50_old")
# X says, "I am 50 years old."
s.add(x_t == x_50_years_old)
# Y says, "X is either 50 years old or a night."
s.add(y_t == Or(x_50_years_old, x_is_k))
# Z says, "X is either 50 years old or a knave"
s.add(z_t == Or(x_50_years_old, x_is_n))
There’s only one solution: (knave, spy, knight).