💬 NLP

Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems

This paper introduces ZPS, a constraint-guided multi-agent system that combines Large Language Models with an off-the-shelf theorem prover to generate and refine SMT code for solving complex Zebra puzzles, demonstrating significant accuracy improvements over standalone LLMs.

Original authors: Shmuel Berman, Kathleen McKeown, Baishakhi Ray

Published 2026-06-04

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Shmuel Berman, Kathleen McKeown, Baishakhi Ray

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a very tricky logic puzzle, like the famous "Zebra Puzzle" where you have to figure out who lives in which house, what color it is, what pet they have, and what sport they play, based only on a few confusing sentences.

This paper is about teaching a computer (specifically, a Large Language Model or LLM) how to solve these puzzles much better than it could on its own. Here is how they did it, explained simply:

The Problem: The Computer Gets Confused

Think of an LLM like a very smart, well-read student who is great at writing essays but sometimes struggles with strict math rules. When you ask it to solve a logic puzzle, it tries to guess the answer based on patterns.

The Issue: Logic puzzles require perfect precision. If the student misinterprets one tiny clue (like "The person with the fish lives to the left of the cat"), the whole answer falls apart.
The Result: On its own, the computer student gets the answer right only about 24% of the time. It's like a student who knows the vocabulary but keeps making calculation errors.

The Solution: A Team of Specialists

The authors built a system called ZPS (Zebra Puzzle Solver). Instead of asking one computer to do everything, they created a team of three agents (specialized AI workers) that work together like a construction crew:

The Architect (Decomposition Agent):
- Role: This agent reads the messy, confusing puzzle clues and breaks them down into small, manageable blueprints. It organizes the chaos into a clear list of rules.
- Analogy: Imagine a foreman who takes a messy pile of instructions and sorts them into neat, labeled boxes so the workers know exactly what to do.
The Translator (Solver Agent):
- Role: This agent takes the organized rules and translates them into a strict, computer-readable language called SMT-LIB. This is a language that logic machines understand perfectly, with no room for ambiguity.
- Analogy: This is like a translator who converts a vague story into a precise mathematical equation.
The Judge (Theorem Prover):
- Role: This isn't an AI; it's a standard, off-the-shelf logic engine (like a super-fast calculator for logic). It takes the strict equations from the Translator and checks if they actually work.
- Analogy: This is the strict math teacher who checks the homework. If the answer is wrong, the teacher doesn't just say "No"; they point out exactly where the logic failed.

The Secret Sauce: The Feedback Loop

The magic happens because these agents talk to each other in a loop:

The Architect breaks down the puzzle.
The Translator writes the rules in code.
The Judge tries to solve it.
If the Judge finds a mistake (e.g., "This code has a syntax error" or "This solution contradicts Clue #3"), it sends the work back to the Translator.
The Translator fixes the mistake and tries again.
They keep doing this until the Judge says, "This is perfect."

Think of it like a sculptor chipping away at a block of marble. If they hit a crack (an error), they adjust their chisel (the translation) and try again. They don't just guess; they refine their work based on immediate, hard facts.

The Results: A Massive Improvement

The authors tested this team approach on 114 different puzzles using three different AI models (GPT-4, GPT-3.5, and Llama3).

Before the team: GPT-4 solved about 24% of the puzzles correctly on its own.
After the team: With the help of the logic engine and the feedback loop, GPT-4 solved 63% of the puzzles correctly.
The Gain: That is a 166% improvement. It's like a student who used to get a D suddenly getting an A+ because they had a tutor and a strict grader helping them.

How They Checked the Work

To make sure their computer grading system was fair, they hired a group of human students to grade a sample of the puzzles. They compared the human grades to the computer's grades.

The Finding: The computer grader agreed with the humans almost all the time (over 85% of the time). This proved that their automated system was reliable and didn't need humans to check every single answer.

Summary

The paper shows that while AI is great at understanding language, it needs help with strict logic. By combining a "smart" AI (which understands the clues) with a "strict" logic machine (which checks the math) and letting them correct each other, they created a system that solves complex logic puzzles far better than the AI could do alone.

Technical Summary: Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems

Problem Definition

The paper addresses the challenge of solving Zebra puzzles (also known as Einstein or logic grid puzzles), a specific class of unstructured natural language problems. These puzzles require deducing the correct assignment of attributes (e.g., nationality, animal, sport) to a set of entities (e.g., houses) based on a series of ambiguous natural language clues.

The authors identify five primary factors that make these puzzles difficult for both humans and AI systems:

Complex Inferences: Clues provide partial information requiring combination to deduce solutions.
High Interdependency: Errors in interpreting one clue propagate significantly through the solution space.
Natural Language Ambiguity: Translating ambiguous clues into precise logical statements is non-trivial.
Large Solution Space: Solvers must explore numerous combinations.
Consistency Checking: Solutions must be validated against all clues, requiring sophisticated reasoning.

Prior research indicates that Large Language Models (LLMs) alone struggle with these tasks, with reported correctness rates as low as 8.33% for Zebra puzzles, often failing to correctly encode implicit constraints or subtextual nuances.

Methodology: The Zebra Puzzle Solver (ZPS)

The authors propose ZPS, a multi-agent system that integrates LLMs with an off-the-shelf Satisfiability Modulo Theories (SMT) theorem prover (specifically Z3). The system operates on a workflow that decomposes the problem, translates it into a formal language, solves it, and iteratively refines the output based on feedback.

Core Workflow

The process is modeled as a recursive feedback loop involving the following agents and steps:

Decomposition Agent: An LLM agent takes the natural language puzzle and decomposes it into smaller, manageable sub-problems, identifying key entities, attributes, and relationships.
Translation Agent (Solver LLM): This agent translates the decomposed components into SMT-LIB (Satisfiability Modulo Theories Library) format. This formal representation allows the system to interface with a theorem prover.
Theorem Prover: The Z3 solver processes the SMT-LIB code to find a satisfying assignment that adheres to all logical constraints.
Evaluation and Feedback Loop:
- The output from the theorem prover (including the solution model or syntactic errors) is fed back to the Solver LLM.
- The LLM evaluates the solution against the puzzle's requirements.
- If the solution is insufficient (due to errors or incorrect attribute assignments), the LLM modifies the SMT-LIB translation to address syntactic or semantic errors.
- This cycle repeats until the solution is deemed correct or a maximum retry limit is reached.

Mathematical Modeling

The feedback loop is formally described by the recursive function:
$S_{k+1} = F(E(T(G(D(P))), S_k)), S_k)$
Where $P$ is the initial puzzle, $D$ is decomposition, $G$ is translation to SMT-LIB, $T$ is theorem solving, $E$ is evaluation, and $F$ is the feedback adjustment function. Convergence is achieved when the evaluation function $E$ confirms the solution meets all requirements without detectable errors.

Automated Grading

To assess performance, the authors developed an autograder LLM-agent. This agent compares the solver's output against ground-truth answers, calculating a partial score based on the number of correct attribute assignments. The reliability of this autograder was validated through a user study involving human graders.

Key Contributions

The paper outlines four primary contributions:

Agent-Based Integration: Demonstrating that combining a formal constraint solver with an LLM interpreter via a multi-agent approach significantly improves Zebra puzzle solving over existing baselines.
Decomposition Strategy: Implementing a plan generation and decomposition strategy that enables step-by-step reasoning, enhancing the handling of complex interdependencies.
Iterative Feedback Mechanism: Introducing a conversation-based feedback loop that allows for the continual refinement of solutions, dynamically adapting to the solving context.
Automated Assessment: Incorporating a validated autograder that correlates well with human grading, ensuring reliability in automated performance assessment.

Experimental Results

The system was evaluated on a dataset of 114 Zebra puzzles using three LLMs: GPT-4, GPT-3.5, and Llama3-8b.

Baseline Performance: Without solver assistance, GPT-4 achieved an average partial score of 52.4% and solved 27/114 puzzles (23.7%) completely correctly.
Impact of Solver Integration:
- Integrating the theorem prover (without decomposition) increased GPT-4's average partial score to 0.687 and the number of fully solved puzzles to 59 (51.8%), representing a 118.5% improvement in the number of fully correct solutions.
- With variable temperature settings and retries, GPT-4 achieved a 166.7% improvement in fully correct solutions (72/114).
Impact of Decomposition: Adding a decomposition agent further improved GPT-4's performance to 63 fully solved puzzles (55.3%) with a partial score of 0.700.
Model Variance: GPT-3.5 showed similar positive trends. Llama3-8b showed more modest gains (50% improvement in correct solutions) and struggled more with generating syntactically correct SMT-LIB code, often resulting in errors.
Grader Validation: The user study showed that the LLM-based autograder achieved an exact match rate with human graders exceeding 78% across various setups, with "Joint Full Credit" (agreement on fully correct solutions) registering above 85%.

Significance and Claims

The paper claims that the primary significance of this work lies in demonstrating that structured planning and agent-feedback loops greatly enhance the capability of LLMs to solve logical problems that require precise interpretation and inference.

The authors argue that while LLMs are powerful, they lack the rigorous consistency checking required for complex logic puzzles. By offloading the constraint satisfaction to a formal theorem prover and using the LLM as an interpreter and feedback mechanism, the system bridges the gap between natural language ambiguity and formal logic. The inter-agent critique mechanism, where agents refine each other's contributions through dialogue, is highlighted as a crucial factor in achieving more accurate and consistent results.

The paper concludes that this approach offers a robust framework for solving unstructured natural language problems, provided that the system can effectively translate natural language into a formal space and utilize feedback to correct semantic and syntactic errors.