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 · Institute for Symbolic Artificial Intelligence, JKU Linz, Austria · Institute for Machine Learning, LIT AI Lab, Department of Virtual Morphology, Clinical Research Institute Medical AI, JKU Linz, Austria
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
{[c,a:e]}
a not at entity e
⋃e^∈E{[c,a:e^]}\{[cα,a:e]}
a at same entity as a^
⋃e^∈E{[c,a:e^,a^:e^]}
a is Π entities from a^
⋃i=1N−Π{[c,a:ei,a^:ei+Π],[c,a:ei+Π,a^:ei]}
a directly left/right of a^
⋃i=1N−1{[c,a:ei,a^:ei+1]}
a left/right of a^
⋃i=1N−1⋃j=iN{[c,a:ei,a^:ej]}
Appendix
Table 3: Exact cover encodings of all different clue types as sets of options. Here, c∈C denotes a clue, a∈Ap,a^∈Ap^ any attribute of a property p,p^∈P , and e,e^∈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 a^ .
clue_property_right_of
Attribute a is somewhere to the right of attribute a^ .
clue_property_at_house
Attribute a is fixed at entity e .
clue_property_at_property
Attributes a and 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 [%] ↑
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 ↻
0
0
0
0
0
0
0.6B
NEC (ours) ↻
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 .
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.
Hyunseok Oh, Sam Stern, Youngki Lee +1
Seoul National University · U. Mass. Amherst · Microsoft
Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on https://github.com/sunjia72/SAT-RL.
Chain-of-thought (CoT) prompting can fail severely on constraint-dense logical reasoning tasks, where unverified errors accumulate silently across steps. We introduce SymStep: an LLM makes one atomic claim at a time (DEDUCE: Alice, pet, Cat), then a lightweight constraint propagator checks the claim for consistency with prior accepted deductions, rejects contradictions, and cascades implied facts automatically. SymStep+G additionally provides MRV guidance after each accepted step, directing the LLM toward the most constrained unresolved variable. On a 35-puzzle retained subset of ZebraLogicBench, a benchmark of 1,000 Einstein-style logic puzzles, Direct and CoT both achieve 0%, while SymStep+G reaches 97%. On AR-LSAT analytical reasoning problems, SymStep achieves 100% vs. CoT's 87%. On LGP-14, SymStep+G achieves 100% vs. 0% for CoT and Logic-LM, the strongest prior symbolic+LLM baseline we compare against. Ablation studies reveal that MRV guidance is a key mechanism for reducing directionless cycling, while consistency checking provides a safety net against explicit contradictions. Across six benchmarks spanning five task domains, SymStep variants match or exceed every baseline on constraint-dense and arithmetic tasks. Experiments on AQUA-RAT algebra confirm the advantage is constraint-density-specific.
Aida Usmanova, Rui Gao, Dilshod Azizov +2
Leuphana University of Lüneburg · Mohamed bin Zayed University of Artificial Intelligence