z3

z3 is a constraints solver - it’s got a fancy title “Satisfiability Modulo Theories”, but basically allows you to express problems in certain logical ways, and quickly and efficiently solve them.

There are online playgrounds and support for various languages. I’m using Python’s z3 … I see z3-solver shows up more easily in searches. Oh, they are the same, it’s just the import is simpler.

I ran into it last year during Advent of Code - the second part of that day had a tree searching problem which was vast. I’d written code to solve the first part, I could see it wouldn’t work for the second, so I went hunting for alternative approaches.

I’ve been wanting to take a proper look at it again - I don’t have a need for it at work, sadly, but I have a long-standing project to explore in the back of my head : my dad was a headmaster, and used to set timetables every summer. I wonder if we can use z3 to solve it.

Let’s build up some knowledge from scratch.

examples

trivial

    x = Int('x')
    solve(x + 2 == 4)

You can test if there was a solution (it’s 2, by the way) by expanding it a bit more:

    x = Int('x')
    s = Solver()
    s.add(x + 2 == 4)

    if s.check() == sat:
        m = s.model()
        return  m[x].as_long()
    else:
        return None

trivial only less so

x > 2, y < 10, x + 2*y == 7

making change - dumb

First the dumb version - can we simply make change for a given amount from certain coins ? In my example, I don’t have pennies - so only numbers divisible by 5 work. But the solutions are dumb - making 50c with 5x10c counts, rather than two quarters. (Don’t know why not 10x5c ?)

def solve(amount):

    # available coins
    coins = [5, 10, 25]

    coin_vars = [Int(f"coin_{i}") for i in range(len(coins))]

    s = Solver()
    s.add(Sum([coin_vars[i] * coins[i] for i in range(len(coins))]) == amount)

    for var in coin_vars:
        s.add(var >= 0)

    if s.check() == sat:
        model = s.model()
        total_coins = sum(model[var].as_long() for var in coin_vars)
        print("Number of coins used:", total_coins)
        map = {}
        for i, var in enumerate(coin_vars):
            print(f"Number of {coins[i]}-cent coins:", model[var].as_long())
            map[coins[i]] = model[var].as_long()
        return total_coins, map
    else:
        print("No solution found.")
        return None, None

making change - optimisation

Now we add some optimisation in : the minimal number of coins, now including pennies.

def solve(amount, use_all):

    # available coins
    coins = [1, 5, 10, 25]

    coin_vars = [Int(f"coin_{i}") for i in range(len(coins))]

    o = Optimize()

    o.add(Sum([coin_vars[i] * coins[i] for i in range(len(coins))]) == amount)

    for var in coin_vars:
        o.add(var >= (1 if use_all else 0))

    # Minimize the total number of coins used
    o.minimize(Sum(coin_vars))

    if o.check() == sat:
        model = o.model()
        total_coins = sum(model[var].as_long() for var in coin_vars)
        print("Minimum number of coins needed:", total_coins)
        map = {}
        for i, var in enumerate(coin_vars):
            print(f"Number of {coins[i]}-cent coins:", model[var].as_long())
            map[coins[i]] = model[var].as_long()
        return total_coins, map
    else:
        print("No solution found.")
        return None, None

advent of code

The puzzle on day 10 of 2025 (https://adventofcode.com/2025/day/10) caused a fuss. You can solve part 2 in various ways, but doing it with Z3 was trivial - should it be allowed.

Basically you have a bunch of buttons to press, each of which changes the voltage in certain ways - what’s the minimum number of presses needed to do a certain thing ? Technically possible from first principles, but vast search space : I had code to do it, but I could see it wasn’t go to finish in my lifetime.

But I liked it, because I got to learn how to use z3.

Here’s the code : https://github.com/simongarton/AdventOfCode/blob/main/src/python/2025-10.1-optimise.py

course planner

Now I’m working up to the actual example I want to solve. Here’s a halfway step.

I’m a student at a university. I want to first list all combinations of courses offered that I could take - they happen on certain days and times, and I need to avoid clashes - and then second optimise it, so I’m spending the most possible time in class (doh !)

The course data looks like this:

{
        "id": 100,
        "name": "Course 100",
        "schedule": [
            "Monday 3:00-4:00",
            "Tuesday 2:00-3:00",
            "Wednesday 2:00-3:00",
            "Thursday 2:00-3:00"
        ]
    }

Now Claude enters the chat. I handwrote the course data generator and then got Claude to write the other two scripts, possibles and best.

For the combinations, it did something clever - it generated a list of conflicts - double nested loop though courses, and note which pairs share a time slot. This can be used as a constraints to limit which combinations are allowed.

And this is where the current Ai models are so worth it … because I can then ask Claude to explain, slowly and patiently, what it’s doing. Which is basically solving the problem, getting the first solution, then adding a new constraint saying “don’t give me this one again …”

Clever.

The second part basically optimises for the highest time in class, and then iterates through to find all combinations that match it. And with the small data set, there was one option.

┌─────────────┬──────────┬───────────┬───────────┬──────────┬──────────┐
│    Time     │  Monday  │  Tuesday  │ Wednesday │ Thursday │  Friday  │
├─────────────┼──────────┼───────────┼───────────┼──────────┼──────────┤
│ 9:00-10:00  │          │ Course 10 │           │ Course 5 │          │
├─────────────┼──────────┼───────────┼───────────┼──────────┼──────────┤
│ 10:00-11:00 │ Course 7 │           │ Course 7  │          │ Course 7 │
├─────────────┼──────────┼───────────┼───────────┼──────────┼──────────┤
│ 11:00-12:00 │ Course 8 │           │           │          │ Course 8 │
├─────────────┼──────────┼───────────┼───────────┼──────────┼──────────┤
│ 1:00-2:00   │          │ Course 7  │           │ Course 3 │          │
├─────────────┼──────────┼───────────┼───────────┼──────────┼──────────┤
│ 2:00-3:00   │ Course 9 │ Course 5  │ Course 3  │ Course 8 │ Course 5 │
├─────────────┼──────────┼───────────┼───────────┼──────────┼──────────┤
│ 3:00-4:00   │ Course 3 │ Course 3  │ Course 10 │ Course 7 │          │
└─────────────┴──────────┴───────────┴───────────┴──────────┴──────────┘

Nice.

finally, the timetable

My dad was a headmaster and every summer he would have to disappear into his office and set the timetable. Our schools would have a fixed number of classrooms; a fixed number of teachers with certain skills (mostly one subject, sometimes two); a fixed number of classes, which had certain students in them. Including me. And each class needs to be taught certain subjects.

Now: we can - at this point - ignore the students in each class. And there will be more classrooms than classes. I might add a constraint later that certain subjects can only happen in certain rooms. And in reality, certain teachers could only teach certain classes - a primary school teacher couldn’t teach seniors.

But I will add the obvious constraint that each class needs to have a lesson in every period : 8 periods in a day.

I’ve got 10 classes - so I need at last 10 teachers. Let’s give me 15 teachers and 15 rooms - ah, the good old days, when education was important. And funded.

I asked Claude to create some teachers - and it’s being sneaky, it can see where I’m going.

Created timetable/generate_teachers.py and ran it to produce timetable/teachers.json.

- It reads classes.json and collects all 12 distinct subjects taught anywhere (English, Maths, Science, Geography, History, Art, Biology, Chemistry, Physics, Geology, Economics, Business Studies).
- Generates 15 teachers named "Professor <Color>" (unique colors, no repeats), each assigned 1–3 subjects at random.
- Guarantees every subject has at least one qualified teacher (adjusting a random teacher's list if a subject was missed by chance) — otherwise a timetable solver could hit an unsatisfiable subject later.

Result: 15 teachers generated, all 12 subjects covered, saved to timetable/teachers.json.

Took 1m 13s to write the first script, to return “a” timetable.

I came up with a good way to optimise it, and Claude added the appropriate flexible code for soft optimisations. Here I ran into my first real problem - hi Dad ! - the solution space is vast. So Claude suggested a time constraint and to track “the best so far” …

Not sure this is going to work. If not, I will drop the teachers and rooms : I only have 10 classes.

Ah, Claude suggests an improvement.

Found the real problem: a timed-out Optimize model isn't safe to use — variables Z3 never got around to pinning get filled in independently by "model completion," which can silently violate joint constraints like Distinct (I confirmed this: the "optimized" timetable had 10 classes sharing one teacher per slot, breaking the no-double-booking rule). I need a sounder approach: only ever trust models from a sat result, never unknown.

I'll switch to iterative "solve, then strictly beat this score, repeat" using a plain Solver under a time budget — every accepted answer is a genuine sat result, so it's always valid; we just stop improving once we run out of time or provably hit the optimum.

Now we’re getting solutions in 30 seconds. I’ve tried a 5 minute run, and it hasn’t improved further.

It generates lots of output: both markdown … here’s Professor Black.

… wow, he has a lot of free time …

Discussing further with Claude, it suggests optimizing each day individually - fair enough, give it a whirl.

And now it will return a provably optimum solution (for those constraints) … only it didn’t, and Claude is very apologetic.

Let’s add a constraint : only certain rooms support Science, and the three sciences. And another room is needed for Art.

Ok, that improved it signficantly - faster, and better score.

But then - foolish, in hindsight - we tried to make it better. I noted that most teachers had 38 lessons, but Professor Black had just 7. Yes, he is a Chemistry teacher, but even so, could we make this fairer ?

Claude picked the wrong way to do it, I think - implementing a max load, which in turn meant there turned out to be no valid solutions. (I note that it’s trying to get any solution first, before then trying to get a good one - which is a good approach.) From reading it’s thinking, it’s not sure why this is failing - it should be working. It added a cap of 38 - which is a full week - and it still timed out indicating the constraints are broken / interfering with each other.

But it came up with a new approach, instead of a max load, go for a min load - and got a quick solution. That then meant we could then try and improve it further - and we did. That’s doubled his load.

Later on I asked Claude how to fix this - and basically it’s time for Professor Black to go and do some training ;-)

Fix: searched all 28 candidate single-teacher/single-subject additions and found the best one — giving Professor Black a Science qualification raises the achievable ceiling from 173 to 223 (out of a theoretical max of 236), and as a side effect frees up Navy/Maroon/Pink's bandwidth too, lifting S3 from 15/38 to 32/38 even though S3 doesn't even take Science.

cp-sat and Google

Around this time, Claude started telling me about Google’s CP-SAT solver as being better for this specific task - z3 is good for a range of constraint modelling, cp-sat is specific on scheduling.

So I got Claude to implement the same problem with this new library - a big download.

It worked really well - first finding the root problem with optimising the timetable, and then generating better solutions in seconds. I eventually saw from my diagrams that it was “cheating” and putting blocks of lessons together, so a class would do the same subject all day with the same teacher in the same room. That would be very boring - so I added a constraint that each class has to have each subject each day, and that was better.

conclusions

A good use of an evening, learned heaps. Lots more to do, will see if I can revisit this again.