happy hacks

Solving a "Layton Puzzle" with z3

See [original post] where the author posts a problem from a video game and solves in prolog

Summary for the text-only readers: We have a test with 10 true/false questions (denoted a/b) and four student attempts. Given the scores of the first three students, we have to figure out the fourth student's score.

bbababbabb = 7 baaababaaa = 5 baaabbbaba = 3 bbaaabbaaa = ???

We can model this in z3 and try to solve for Colin’s score

Since we don’t know the answers to all the questions we can define them as variables

answers = [Bool(f"q{i}") for i in range(10)]

The answers to the quiz are z3.Bool because there’s only 2 options - a or b

Next we define scores and answers of Mary, Dan and Lisa

_students = [
    "bbababbabb",
    "baaababaaa",
    "baaabbbaba",
    "bbaaabbaaa",
]

students = [[BoolVal(True) if c == "a" else BoolVal(False) for c in s] for s in _students]

scores = [7, 5, 3]

z3.BoolVal would store concrete values and are not variable, we create an array for all - including Colin

Next is we define how an instructor would mark the answers to get the scores

s = Solver()

for student, score in zip(students[:3], scores):
    s.add(
        Sum([If(ans == stu, 1, 0) for ans, stu in zip(answers, student)])
        == score
    )

We define z3.Solver - an API that provides setting up conditions than needs to be figured out. In this case we don’t know the answers - so we do a symbolic comparison with individual student answers - but since we know the final score we set a constraint on it. A correct answer adds a score of 1.

Now we can define a variable for colin’s score -

score4 = Sum([If(ans == stu, 1, 0) for ans, stu in zip(answers, students[3])])

It is marked the same way - but we don’t know a concrete value so its symbolic Now we can instruct z3 to find solutions and see if all the constraints are satisfied for any set of values in answers

if s.check() == sat:
    m = s.model()
    print("Fourth student's score:", m.eval(score4))
else:
    print("No solution found.")

Instantly it prints

Fourth student's score: 6

Now we can also know that there’s not one but many correct answers - but all yield Colin's score to 6

We can limit z3 to not match a particular answer like this

def deny(solution):
    s.add(Or([BoolVal(solution[i]) != answers[i] for i in range(len(answers))]))

This makes sure that at least one of the values from given solution does not match the reference answer

deny([True, False, True, False, True, True, False, True, True, False])
deny([False, False, True, False, True, True, False, False, True, False])
deny([False, False, True, False, True, True, True, True, True, False])
deny([False, False, False, False, True, True, False, True, True, False])

We repeatedly add new solution as we find them to the deny-list and after these 4 values - z3 would not be able to find the solution.

Final Script

from z3 import *

answers = [Bool(f"q{i}") for i in range(10)]

_students = [
    "bbababbabb",
    "baaababaaa",
    "baaabbbaba",
    "bbaaabbaaa",
]

students = [[BoolVal(True) if c == "a" else BoolVal(False) for c in s] for s in _students]

scores = [7, 5, 3]

s = Solver()

for student, score in zip(students[:3], scores):
    s.add(
        Sum([If(ans == stu, 1, 0) for ans, stu in zip(answers, student)])
        == score
    )

score4 = Sum([If(ans == stu, 1, 0) for ans, stu in zip(answers, students[3])])

def deny(solution):
    s.add(Or([BoolVal(solution[i]) != answers[i] for i in range(len(answers))]))

deny([True, False, True, False, True, True, False, True, True, False])
deny([False, False, True, False, True, True, False, False, True, False])
deny([False, False, True, False, True, True, True, True, True, False])
deny([False, False, False, False, True, True, False, True, True, False])

if s.check() == sat:
    m = s.model()
    print("Fourth student's score:", m.eval(score4))
else:
    print("No solution found.")

#z3