Can First-Order Logic Catch a Killer? Modeling Murdoku with a Theorem Prover

Enter Murdoku, a brilliant logic puzzle game created by Manuel Garand where Sudoku meets a classic whodunit murder mystery. The game was recommended to me by my friends Ceylin and Arne (huge thanks!). Naturally, instead of merely enjoying the deductive bliss of cross-referencing witness alibis, I did what any reasonable computer scientist would do: I wrote an SMT-based constraint solver in Python using Microsoft's Z3 theorem prover.

Why write about this? Logic puzzles and automated theorem proving are intimately tied to my research in formal verification and program synthesis. However, explaining concepts like SMT solvers, formal verification, and program analysis to a general audience is notoriously difficult. Murdoku is a delightful, intuitive way to introduce constraint satisfaction problems, satisfiability, and theorem proving to a wider audience without drowning in academic jargon.

Act 0: The Crime Scene (When Sudoku Meets Agatha Christie)

Before we summon automated theorem provers, let’s inspect the scene of the crime.

In Murdoku you play a detective investigating a murder laid out on an orthogonal 2D grid. The board is partitioned into distinct rooms (Dining Room, Kitchen, Bedroom, Porch, Front Yard), littered with furniture, carpets, and shrubbery.

Case: 24-Hour Delivery (6×6 Grid) — 5 Rooms, 6 People, 1 Victim, and 6 Clues. Try solving it yourself!

In the first crime scene "24-Hour Delivery", Viraj has been murdered. Your job is to deduce who the murderer is, based on the witness statements and the spatial layout of the crime scene. The game operates under a strict set of spatial rules:

• The Sudoku Rook Rule: No two characters can ever share the same row or column (identical to Rooks on a chessboard or numbers in Sudoku).
• Passable vs. Solid Tiles: Characters can sit on chairs and stand on carpets. But solid obstacles—like dining tables, kitchen counters, bed frames, and thorny bushes—are strictly impassable. Suspects cannot occupy their coordinates.
• The Whodunit Goal: Exactly one character is the Victim. The murderer is the person who was alone in the same room with the victim.

Our crime scene is a 6×6 estate with five distinct rooms: A Dining Room, a Bedroom, a Kitchen, a Porch, and a Front Yard. Each room has its own furniture and obstacles that restrict where suspects can be located.

We have six individuals on the scene: our unfortunate victim Viraj, and five suspects: Alexander, Bella, Carol, Dalia, and Evangeline.

On our detective clipboard, we have collected six witness statements:

Six innocent-sounding clues. Five rooms. One dead body. How hard could this possibly be?

Act I: The Appearance of the Detective (That’s You!)

This is where you step onto the scene. You pull on your detective trench coat, grab a sharp pencil, take a confident sip of coffee, and look over the murder scene. You are a seasoned professional—you've solved hundreds of logic puzzles before, and you're ready to crack this case wide open.

You look at the board and the clues, reasoning through the spatial constraints. Each clue is a direct statement about where a suspect was located, which can be leveraged to eliminate possibilities. Your gut instinct tells you that Alexander did it (you know a guy named Alexander, and he always looks suspicious), but true detective work demands following the clues and the rules of the game to find the real murderer.

You start reading the clues one by one, eliminating squares. And then it hits you!

Clue 1: Alexander was beside the box. The delivery box sits at (5, 1) on the Porch. The only adjacent passable tiles are the porch floor at (5, 0) and the porch carpet at (4, 1). But Clue 3 dictates that Carol was the only person on a carpet! Therefore, Alexander cannot be on the carpet. He must be on the porch floor at (5, 0)!

Step 1: Alexander is placed at (5, 0). By the Rook rule, Row 5 and Column 0 are eliminated for everyone else.

Watch how the deductive dominoes begin to fall. Because of the Sudoku Rook rule, nobody else can ever occupy Row 5 or Column 0.

Clue 2: Bella was sitting in a chair. Looking at the chairs on the board, the ones along Column 0 are already blocked by Alexander. That leaves only one valid, open chair: the dining chair at (0, 1). Bella takes her seat, knocking out Row 0 and Column 1 for everyone else.

Step 2: Bella is placed at (0, 1) in the Dining Room. Row 0 and Column 1 are eliminated.

Now the cascade gains momentum:

Clue 4: Dalia was in the Bedroom. The Bedroom spans Rows 0–1 and Columns 3–5. Row 0 is completely blocked by Bella. In Row 1, tile (1, 4) contains an impassable potted plant, and (1, 5) is a carpet (which Clue 3 reserves exclusively for Carol). The only possible square left for Dalia is (1, 3)!

Step 3: Dalia is placed at (1, 3) in the Bedroom. Row 1 and Column 3 are now blocked.

Clue 3: Carol was the only person on a carpet. We scan the board for surviving carpets. The Bedroom carpet at (1, 5) was ruled out when Dalia took Row 1. The Porch carpet at (4, 1) was blocked by Bella's column. That leaves only one solitary carpet tile in the entire mansion: (2, 4) in the Kitchen. Carol is placed!

Step 4: Carol is placed at (2, 4) on the Kitchen carpet. Row 2 and Column 4 are eliminated.

Clue 5: Evangeline was either beside a shrub or a plant. Looking at open positions in Row 4, tile (4, 3) is already blocked by Dalia's column. That leaves (4, 2) in the Front Yard, directly adjacent to the garden shrub. Evangeline is positioned!

Step 5: Evangeline is placed at (4, 2) in the Front Yard, right beside the shrub.

With five suspects positioned, exactly one unassigned square remains on the entire board: (3, 5) in the Kitchen. That is where our victim, Viraj, was found!

Step 6: Viraj is placed at (3, 5) in the Kitchen. All six characters are now placed on the board.

Now, the final clue: Viraj was alone with the murderer.

Viraj was in the Kitchen at (3, 5). Looking across the Kitchen, there is only one other soul present: Carol, standing at (2, 4).

You gather everyone into the drawing room (except Viraj, of course, as he is dead), dramatically point your finger, and announce: Carol is the murderer! Case closed in under 3 minutes.

Case Solved! Carol was alone in the Kitchen with Viraj. She is the killer!

That felt delightfully clean, didn't it? Every clue triggered a direct, linear deduction. No guessing. No backtracking. Just pure, orderly logic.

But leaning back in your chair, you notice something. You are getting tired. All this deducing—and dealing with a fresh murder every single day—is exhausting work. These cases take a toll on you. You would love to hang up your trench coat and retire, but who else is going to catch these killers?

Especially when the cases get harder. On larger 9×9 boards with multi-way disjunctions and sightlines, human working memory quickly hits its limit—cognitive psychology shows we can only comfortably juggle 4 to 7 items at once. Two nested layers of hypothetical branching, smudged pencil notes, and frantic backtracking cause human brains to overheat and give up.

You take a sip of your lukewarm coffee, open the morning newspaper, and a bold headline catches your eye: "S(herloc)MT: The Newest Detective in Town".

You read on. This new sleuth isn't human at all—it's an automated theorem prover. It never forgets a constraint, never gets tired, doesn't need erasers, and can evaluate 10 million hypothetical branches before your coffee even gets cold. You are intrigued, but deeply skeptical. Can a computer program really catch a killer? How does this machine even think?

It's time to do some detective work of your own and investigate this new colleague. You open your laptop and start reading...

Act II: The Mandatory Flashback (aka The Background Story)

To understand how our new digital detective works, we need to peek under his fedora.

At his core, S(herloc)MT relies on a Satisfiability Modulo Theories (SMT) solver. An SMT solver is essentially a specialized reasoning engine built on top of a classic Boolean Satisfiability (SAT) solver.

A traditional SAT solver is a master of pure binary deduction. It evaluates whether a formula in propositional logic—constructed purely from boolean variables and connectives, such as $(A \lor B) \land (\neg A \lor \neg B)$—can be satisfied by any assignment of TRUE and FALSE.

While remarkably fast, pure boolean logic is clumsy when dealing with crime scenes. A detective does not want to manually encode "Suspect Alexander is at column 4" into dozens of mutually exclusive boolean flags ($A_{c0}, A_{c1}, A_{c2}, \dots$) and write hundreds of extra constraints just to say "a person can only be in one column at a time."

This is where SMT enters the precinct. An SMT solver equips the SAT engine with domain-specific background theories—most importantly for us, the theory of Linear Integer Arithmetic (LIA). Instead of seeing only abstract truth values, S(herloc)MT can reason directly about integer coordinates, grid bounds ($0 \le r \lt 6$), and spatial inequalities ($c_{\text{Alexander}} > c_{\text{Carol}}$) with mathematical certainty.

Defining The Problem & Goal

Before writing formulas, let's clearly state what the problem is from a computational standpoint. What do we have, and what do we want to find?

In any Murdoku puzzle, we are given:

1. A finite set of suspects: $S = \{ \text{Alexander}, \text{Bella}, \text{Carol}, \dots \}$
2. A physical space: An orthogonal grid partitioned into rooms, with passable floors and impassable obstacles.
3. A set of rules and witness clues: Such as rook uniqueness, adjacency, and room assignments.

Our goal is to find an assignment of coordinates—a model—that satisfies all conditions simultaneously:

• Variables: For each suspect $s \in S$, we declare two integer variables:
  • $r_s \in \mathbb{Z}$ (their row coordinate)
  • $c_s \in \mathbb{Z}$ (their column coordinate)

• The Master Formula ($\Phi_{\text{case}}$): We translate every game rule, room boundary, and witness statement into a formal logical constraint. The entire case is represented as one master conjunction:
  $$\Phi_{\text{case}} \equiv \Phi_{\text{grid}} \land \Phi_{\text{rook}} \land \Phi_{\text{obstacles}} \land \Phi_{\text{clues}}$$
• Satisfiability: We ask the solver: Does there exist an assignment of integers to all $(r_s, c_s)$ that makes $\Phi_{\text{case}}$ true?
• The Model ($\mathcal{M}$): If the answer is SAT, the solver produces a valuation $\mathcal{M}$ (a concrete coordinate for every person):
  $$\mathcal{M} \models \Phi_{\text{case}}$$
  (Read: "The model $\mathcal{M}$ satisfies the formula $\Phi_{\text{case}}$")
• The Whodunit: A valid logic puzzle has exactly one unique model $\mathcal{M}$. Once all coordinates are pinned down, we simply check who shares a room with the victim to catch the killer!

A Detective's Guide to Formal Notation

Formal logic can look intimidating at first glance, but it is really just an unambiguous shorthand for common English statements. Here is the decoder ring:

A Micro-Case: The $2 \times 2$ Porch

To see how this works in practice without drowning in a full 6×6 board, let's isolate the Porch into a minimal $2 \times 2$ micro-case with two suspects: Arne and Ceylin.

Given the physical layout and two clues, we want to find a model that satisfies all spatial constraints and game rules:

The $2 \times 2$ Porch: Two carpets in Row 0, bare floor at (1, 0), and delivery box at (1, 1).

The Facts & Clues

• The Layout: The delivery box sits at $(1, 1)$ and is an impassable solid obstacle. The porch has two carpet tiles at $(0, 0)$ and $(0, 1)$ (Row 0), and a bare floor tile at $(1, 0)$.
• The Rook Rule: Just like in Sudoku, Arne and Ceylin cannot share the same row or the same column.
• Clue 1: Arne was beside the box. (Orthogonally adjacent: North, South, East, or West).
• Clue 2: Ceylin was the only person on a carpet. (Ceylin must be on a carpet tile, and Arne cannot be on any carpet tile).

Building the Formal Model

We represent both suspects $S = \{\text{Arne, Ceylin}\}$ with integer coordinates: $(r_A, c_A)$ for Arne, and $(r_C, c_C)$ for Ceylin. $r_s$ and $c_s$ are integers representing the row and column of suspect $s \in S$, respectively. The grid is bounded by $0 \le r, c \le 1$.

The complete specification for this micro-case, $\Phi_{\text{porch}}$, is the conjunction of five clear constraints:

Let's break down each component:

1. Grid Domain ($\Phi_{\text{domain}}$): Both suspects must stay within the physical $2 \times 2$ boundaries:
   $$\Phi_{\text{domain}} \equiv (0 \le r_A \le 1 \land 0 \le c_A \le 1) \land (0 \le r_C \le 1 \land 0 \le c_C \le 1)$$
2. The Sudoku Rook Rule ($\Phi_{\text{rook}}$): Arne and Ceylin cannot share a row or column:
   $$\Phi_{\text{rook}} \equiv (r_A \ne r_C) \land (c_A \ne c_C)$$
3. Impassable Obstacle ($\Phi_{\text{obstacle}}$): The box at $(1, 1)$ is solid furniture; neither suspect can occupy it:
   $$\Phi_{\text{obstacle}} \equiv \neg (r_A = 1 \land c_A = 1) \land \neg (r_C = 1 \land c_C = 1)$$
4. Beside the Box ($\Phi_{\text{beside}}$): Clue 1 states Arne is orthogonally adjacent to the box at $(1, 1)$. Within grid boundaries, the only neighboring squares are West at $(1, 0)$ or North at $(0, 1)$:
   $$\Phi_{\text{beside}} \equiv (r_A = 1 \land c_A = 0) \lor (r_A = 0 \land c_A = 1)$$
5. Carpet Constraint ($\Phi_{\text{carpet}}$): Clue 3 states Ceylin was the only person on a carpet. Since the carpet occupies the entire Row 0 ($\{ (0, 0), (0, 1) \}$), Ceylin must be on Row 0, and Arne cannot be on Row 0:
   $$\Phi_{\text{carpet}} \equiv (r_C = 0) \land (r_A \ne 0)$$

Evaluating the Formula Step-by-Step

Notice how the dominoes fall when all five constraints are combined:

1. From $\Phi_{\text{carpet}}$, Arne cannot be in Row 0 ($r_A \ne 0$), meaning he must be in Row 1 ($r_A = 1$).
2. From $\Phi_{\text{obstacle}}$, tile $(1, 1)$ is impassable. Thus, Arne's only valid square is $(1, 0)$.
3. Now the Rook rule ($\Phi_{\text{rook}}$) triggers: because Arne is at $(1, 0)$, Ceylin cannot share Row 1 ($r_C \ne 1$) or Column 0 ($c_C \ne 0$).
4. For Ceylin, Column 0 is blocked, ruling out $(0, 0)$. She must be on a carpet ($r_C = 0$), leaving exactly one square: $(0, 1)$.

Only one candidate assignment satisfies the entire conjunction:

Giving the unique model:

The Solved Porch: Arne placed at (1, 0) and Ceylin at (0, 1).

Both suspects are uniquely deduced with mathematical certainty!

You take a sip from your coffee while reading this micro-case and you are struck by the elegance of the solution. The constraints are simple, yet they lead to a single, unambiguous answer. This is the power of formal logic and SMT solving in action.

But you have seen enough theory and young detectives need to see the practical side of things. You decide to implement this micro-case in Python using the Z3 SMT solver. The code will declare the variables, add the constraints, and let Z3 find the unique solution for you.

From Theory to Code: Implementing the Micro-Case in Z3

Translating this complete two-suspect model into Microsoft Z3 in Python is simple and clean. We start by declaring the integer variables for both suspects, Arne and Ceylin:

from z3 import *

# 1. Declare coordinate variables for both suspects
r_A, c_A = Int("r_A"), Int("c_A")
r_C, c_C = Int("r_C"), Int("c_C")

Next, we create a solver instance and add the constraints step by step, following the formal model we derived earlier. We start with the grid domain: both suspects must stay within the $2 \times 2$ boundaries of the porch.

solver = Solver()

# 2. Grid domain: 2x2 porch (rows and cols in [0, 1])
for r, c in [(r_A, c_A), (r_C, c_C)]:
    solver.add(r >= 0, r <= 1)
    solver.add(c >= 0, c <= 1)

Next, we enforce the Sudoku Rook Rule: Arne and Ceylin cannot share the same row or column. Similarly, we add the impassable obstacle constraint for the box at $(1, 1)$. Both suspects cannot occupy that tile:

# 3. Sudoku Rook Rule: Distinct rows and columns
solver.add(r_A != r_C)
solver.add(c_A != c_C)

# 4. Impassable obstacle: box at (1, 1)
solver.add(Not(And(r_A == 1, c_A == 1)))
solver.add(Not(And(r_C == 1, c_C == 1)))

Finally, we add the two clues: Arne must be orthogonally adjacent to the box, and Ceylin must be on a carpet while Arne cannot be on a carpet:

# 5. Clue 1: Arne beside the box (orthogonally adjacent to (1, 1))
solver.add(Or(
    And(r_A == 1, c_A == 0),  # West
    And(r_A == 0, c_A == 1)   # North
))

# 6. Clue 2: Ceylin is the only person on a carpet (carpet is Row 0)
solver.add(r_C == 0)   # Ceylin is on a carpet
solver.add(r_A != 0)   # Arne is NOT on a carpet

We are now ready to let Z3 do its magic and find the unique solution that satisfies all constraints. If a solution exists, we print the coordinates of both suspects. If not, we report that the clues are contradictory:

# 7. Solve!
if solver.check() == sat:
    m = solver.model()
    print(f"Arne placed at:   ({m[r_A]}, {m[c_A]})")
    print(f"Ceylin placed at: ({m[r_C]}, {m[c_C]})")
else:
    print("Unsatisfiable: Contradiction in clues!")

The output of this code will be:

Z3 evaluates the formula in under 1 millisecond. It doesn't loop through candidates or try brute force: it treats the constraints as a system of mathematical equations, simplifies them, and directly derives the unique solution.

You are impressed by how quickly and elegantly the SMT solver handles the problem. This micro-case demonstrates the power of formal logic and SMT solving in a clear and practical way.

You think to yourself, "If this is how it works for two suspects on a tiny porch, imagine what it can do for a full 6×6 Murdoku board with dozens of suspects and complex clues!" You reach for your phone and call the number in the newspaper ad—you want to see how S(herloc)MT can help you solve the full-scale Murdoku puzzle.

Act III: Solving the First Case

To be continued...

The Future: What’s Next for Murdoku?

Murdoku turns out to be an exceptionally fun and intuitive way to demystify SMT (Satisfiability Modulo Theories) solvers. Turning witness statements, furniture layouts, and murder room rules into formal first-order logic brings theoretical computer science to life in a way anyone can visualize.

The solver itself is already fully functional and happily cracking cases in milliseconds! You don't have to wait for the next blog update to explore it—the entire Python codebase, board layout models, and case solutions are open-source and available on GitHub:

This blog post is part of an ongoing series and will be extended with:

• Act III: Solving the First Case with Python & Z3 — Translating the full 6×6 "24-Hour Delivery" case line-by-line into Z3 integer variables, distinct constraints, room topologies, and witness implication rules.
• The Cutting Edge — Extending the solver to handle tricky daily mechanics like line-of-sight/shadow occlusion, Chebyshev distance constraints, and automated natural language clue parsing.

Stay tuned as the next acts unfold! In the meantime, feel free to star the repo on GitHub, and try putting your own detective skills to the test over at murdoku.com/play.