From Natural Language to Exact Cover: A Neuro-Symbolic Approach to Zebra Puzzles

Paulius Skaisgiris; Thomas Pammer; Veronika Semmelrock; Mykyta Ielanskyi; Maximilian Heisinger; Erich Kobler

cs.AINov 2, 2026

From Natural Language to Exact Cover: A Neuro-Symbolic Approach to Zebra Puzzles

Authors: Paulius Skaisgiris, Thomas Pammer, Veronika Semmelrock, Mykyta Ielanskyi, Maximilian Heisinger, Erich Kobler

Organizations: Institute of Logic and Computation, TU Wien, Austria · Institute for Application-Oriented Knowledge Processing, JKU Linz, Austria · Department of Artificial Intelligence and Cybersecurity, University of Klagenfurt, Austria · Institute for Machine Learning, JKU Linz, Austria ·

Abstract

Chain-of-Thought (CoT) generation has substantially improved the performance of Large Language Models (LLMs) on complex reasoning tasks, including code generation, data analysis, and exam-style question answering. Despite these advances, purely neural LLMs continue to struggle with elementary logical reasoning problems and lack the determinism, soundness, and reliability characteristic of symbolic reasoning systems. Conversely, classical symbolic methods such as SAT solving and exact cover guarantee correctness and completeness, but require problems to be expressed in highly specialized formal encodings, limiting their applicability to natural language inputs. In this work, we present a synergistic neuro-symbolic framework that bridges this gap by combining neural semantic parsing with deterministic exact cover reasoning. Given a Zebra-style logic puzzle in natural language, an LLM translates entities and constraints into structured tool calls that construct an exact cover instance. A symbolic solver then computes the solution and provides feedback to iteratively refine invalid, under- or overconstrained encodings, exploiting the uniqueness property of Zebra puzzles. We conduct a comprehensive empirical evaluation across multiple parameter scales, post-training paradigms, and LLM families. The results demonstrate that our hybrid approach consistently outperforms strong plain neural baselines, including CoT prompting, as well as recent neuro-symbolic methods.

Figures & tables

Figure 1: Visualization of NeuralExactCover . A puzzle instance is combined with our prompt template and processed by an LLM that harmonizes attributes, extracts entities and clues, and translates clues into an exact cover encoding. The symbolic MiniExact solver then solves the encoding and provides iterative feedback on failures to refine the generated tool calls. This loop continues until a unique solution is found or the retry limit is reached, after which the solution is converted into plain text.

Size	Metric	Base					Instruct					Thinking
		P	LL	NEC	LP ↻	NEC ↻	P	LL	NEC	LP ↻	NEC ↻	P	LL †	NEC	LP ↻	NEC ↻
4B	All	$52.7$	$25.6$	82.6	$68$	84.9	$66.1$	$43.5$	53.8	$80.2$	65.7	$27.5$	–	3.3	$45.1$	10.3
	S	98.44	$25.94$	95	$82.5$	96.56	$97.81$	$70.31$	71.88	$93.12$	82.19	$79.06$	–	9.38	$55.31$	29.38
	M	$71.07$	$26.43$	93.93	$72.5$	96.79	$85.71$	$50.71$	57.14	$85.36$	73.57	$7.86$	–	1.07	$44.29$	3.21
	L	$6.5$	$24$	82	$65.5$	83	$48$	$27$	39.5	$73.5$	52.5	$0$	–	0	$36$	0
	XL	$0$	$25.5$	47.5	$41$	51.5	$6$	$7$	34.5	59	41.5	$0$	–	0	$39$	0

Table 1: Effect of training mode of Qwen3 LLMs. The best result per model-size group is shown in italics . The best result across all models is shown in bold italics .

Model			ZebraLogic						ZebraExtreme
	Size	Approach	All	S	M	L	XL	Cell	All	XXL	XXXL	Cell
Qwen 3-I	30B	Plain	$70.9$	99.38	$95.71$	$55$	$6.5$	$54.28$	$0.5$	$0.83$	$0$	$14.58$
	30B	Logic-LM	$83$	$95.31$	$87.14$	$74.5$	$66$	$85.67$	$6.75$	$11.5$	$2$	$19.27$
	30B	NEC (ours)	92.7	95.94	95	91.5	85.5	93.77	43.75	48.75	36.25	58.05
	30B	Logic.py ↻	$87.5$	$95.94$	$88.57$	$85$	$75$	$85.44$	$6$	$12$	$0$	$10.58$
	30B	NEC ↻ (ours)	95	98.44	97.5	92.5	88.5	95.54	46.75	52.08	38.75	59.89

Table 2: Performance by model family. The overall best performance per column is marked bold , while the best performance per LLM family is in italics . Model output was capped at 4K tokens for ZebraLogic and 30K for ZebraExtreme.

Figure 2: Runtimes of the LLM (left) and the symbolic solver (right) for gpt-oss-20b.

Appendix figures & tables3 assets

Supplementary material from the paper’s appendix.

Appendix

Clue Type	Exact Cover Encoding
$a$ at entity $e$	$\bigl\{[c,\,a:e]\bigr\}$
$a$ not at entity $e$	$\bigcup_{\hat{e}\in\mathcal{E}}\bigl\{[c,\,a:\hat{e}]\bigr\}\big\backslash\bigl\{[c_{\alpha},\,a:e]\bigr\}$
$a$ at same entity as $\hat{a}$	$\bigcup_{\hat{e}\in\mathcal{E}}\bigl\{[c,\,a:\hat{e},\;\hat{a}:\hat{e}]\bigr\}$
$a$ is $\Pi$ entities from $\hat{a}$	$\bigcup_{i=1}^{N-\Pi}\bigl\{[c,\,a:e_{i},\;\hat{a}:e_{i+\Pi}],[c,\,a:e_{i+\Pi},\;\hat{a}:e_{i}]\bigr\}$
$a$ directly left/right of $\hat{a}$	$\bigcup_{i=1}^{N-1}\bigl\{[c,\,a:e_{i},\;\hat{a}:e_{i+1}]\bigr\}$
$a$ left/right of $\hat{a}$	$\bigcup_{i=1}^{N-1}\bigcup_{j=i}^{N}\bigl\{[c,\,a:e_{i},\;\hat{a}:e_{j}]\bigr\}$

Appendix

Table 3: Exact cover encodings of all different clue types as sets of options. Here,

c\in\mathcal{C}

denotes a clue,

a\in\mathcal{A}_{p},\hat{a}\in\mathcal{A}_{\hat{p}}

any attribute of a property

p,\hat{p}\in\mathcal{P}

, and

e,\hat{e}\in\mathcal{E}

any entity. Note that we only list the exact cover encoding for the left of clues in the last lines; the right of pendants have similar structure but shifted indices.

Encoding Function	Description
init_zebra	Initializes the puzzle with $N$ entities $M$ property groups, and $K$ clues.
clue_property_left_of	Attribute $a$ is somewhere to the left of attribute $\hat{a}$ .
clue_property_right_of	Attribute $a$ is somewhere to the right of attribute $\hat{a}$ .
clue_property_at_house	Attribute $a$ is fixed at entity $e$ .
clue_property_at_property	Attributes $a$ and $\hat{a}$ occur at the same house.
clue_not_property_at_house	Attribute $a$ is not located at entity $e$ .

Appendix

Table 4: Python API for exact cover encoding.

Model		Accuracies [%] $\uparrow$
Size	Approach	All	S	M	L	XL	Cell
0.6B	Plain	24.1	61.25	15	1.5	0	18.31
0.6B	Logic-LM	$0$	$0$	$0$	$0$	0	$0.04$
0.6B	NEC (ours)	$2.7$	$8.44$	$0$	$0$	0	$1.86$
0.6B	Logic.py $\circlearrowright$	$0$	$0$	$0$	$0$	0	$0$
0.6B	NEC (ours) $\circlearrowright$	$2.2$	$6.88$	$0$	$0$	0	$1.23$

Appendix

Table 5: Performance across Qwen3-base model sizes. The overall best performance per column is marked bold , while the best performance per size is written in italics .

Neuro-Symbolic Reasoning

Neuro-symbolic reasoning combines learned neural models with explicit logic, rules, knowledge structures, or executable tools to solve structured tasks.

See all 281 papers

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory
Feb 20, 2026Hyunseok Oh, Sam Stern, Youngki Lee +1Constraint-Guided Reasoning in Language Models Neuro-Symbolic Reasoning
Seoul National University · U. Mass. Amherst · Microsoft
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
Oct 9, 2026Jialiang Sun, Kuldeep MeelRL for Language Model Reasoning Symbolic Reasoning
University of Toronto
SymStep: Symbolic Step Verification for Logical Reasoning
Jul 25, 2026Aida Usmanova, Rui Gao, Dilshod Azizov +2Constraint Propagation Symbolic Reasoning
Leuphana University of Lüneburg · Mohamed bin Zayed University of Artificial Intelligence

Feb 20, 2026J/K move · Enter open · S save

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

Hyunseok Oh, Sam Stern, Youngki Lee, Matthai Philipose

Seoul National University · U. Mass. Amherst · Microsoft

Constraint-Guided Reasoning in Language Models Neuro-Symbolic Reasoning Symbolic Reasoning in Language Models Satisfiability Modulo Theories

Open paper AskPDF arXiv

Natural language understanding requires interleaving textual and logical reasoning, yet large language models often fail to perform such reasoning reliably. Existing neurosymbolic systems combine LLMs with solvers but remain limited to fully formalizable tasks such as math or program synthesis, leaving natural documents with only partial logical structure unaddressed. We introduce Logitext, a neurosymbolic language that represents documents as natural language text constraints (NLTCs), making partial logical structure explicit. We develop an algorithm that integrates LLM-based constraint evaluation with satisfiability modulo theory (SMT) solving, enabling joint textual-logical reasoning. Experiments on a new content moderation benchmark, together with LegalBench and Super-Natural Instructions, show that Logitext improves both accuracy and coverage. This work is the first that treats LLM-based reasoning as an SMT theory, extending neurosymbolic methods beyond fully formalizable domains.

Abstract

Neuro-Symbolic Reasoning

Explore similar work

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers

SymStep: Symbolic Step Verification for Logical Reasoning