Coffee Lecture vom 15.Juli 2026

# Coffee-Lecture - Options for running programs on the bwUniCluster

Coffee-Lecture by Benedikt Otto from July 8th 2026.

# Coffee-Lecture - Introduction to the Z3 Theorem Prover

Coffee-Lecture by Benedikt Otto from July 15th 2026.

```

We give a brief introduction into what the SAT/SMT problem is in theoretical computer science and present the

Z3 Theorem Prover, which is a powerful tool that helps with solving some SMT problems. We will then present

several simple applications of Z3 where we use it to solve several different types of logic puzzles.

```

The examples are written in **Python** using the `z3-solver` package.

 No newline at end of file

# This solves the following logical puzzle:

#     Spend exactly 100 dollars and buy exactly 100 animals. Dogs cost 15 dollars,

#     cats cost 1 dollar and mice cost 25 cents each. You have to buy at least one

#     of each animal. How many of each should you buy?

#

from z3 import *

# Define three integer variables.

dog = Int('dog')

cat = Int('cat')

mouse = Int('mouse')

# Create solver object and add assertions.

s = Solver()

s.add(dog + cat + mouse == 100)

s.add(1500*dog + 100*cat + 25*mouse == 10_000)

s.add(dog >= 1, cat >= 1, mouse >= 1)

# Check for SAT and return model.

if s.check() == sat:

    print(s.model())

# Solution for the second part of the Advent of Code

# puzzle from 2023 day 24 using the z3 solver.

# (Here only with the example input).

#

# https://adventofcode.com/2023/day/24

#

from dataclasses import dataclass

from z3 import *

@dataclass

class Hailstone:

    pos_x: int; pos_y: int; pos_z: int

    vel_x: int; vel_y: int; vel_z: int

# Create list of hailstones.

hailstone_list = [

    #           Position    Velocity

    #          x   y   z  vx  vy  vz

    Hailstone(19, 13, 30, -2,  1, -2),

    Hailstone(18, 19, 22, -1, -1, -2),

    Hailstone(20, 25, 34, -2, -2, -4),

    Hailstone(12, 31, 28, -1, -2, -1),

    Hailstone(20, 19, 15,  1, -5, -3)

]

s = Solver()

# Variables for the rock position.

r_x,   r_y,  r_z = Ints('rock_x rock_y rock_z')

r_vx, r_vy, r_vz = Ints('rock_vx rock_vy rock_vz')

# Add constraints for each hailstone.

for h_num, h in enumerate(hailstone_list):

    # Timestamp where the rock hits this hailstone.

    t_h = Int(f't_{h_num}')

    s.add(t_h >= 0)

    # The xyz coord of the rock and the hailstone

    # must be the same at time t_h.

    s.add(r_x + t_h * r_vx == h.pos_x + t_h * h.vel_x)

    s.add(r_y + t_h * r_vy == h.pos_y + t_h * h.vel_y)

    s.add(r_z + t_h * r_vz == h.pos_z + t_h * h.vel_z)

# Let z3 do its magic.

if s.check() == sat:

    m = s.model()

    print(m)