Short tutorial at ESSAI 2026
Stefan Szeider · Algorithms and Complexity Group, TU Wien
Download Slides
This page previews the ideas the tutorial is built on, so you can decide whether to attend. It is about principles you can take home and reuse, not about any one result. No prior background in language models or constraint solving is assumed: we build up SAT, constraint programming, and LLM basics from scratch.
The tension at the heart of the tutorial
Large language models are fluent and flexible, but notoriously unreliable at exact reasoning. Symbolic solvers for SAT, SMT, and constraint programming are precise and trustworthy, but rigid and demanding to use.
In terms, these are two complementary ways of thinking:
-
System 1 — fast, intuitive, associative → language models
-
System 2 — slow, deliberate, exact → solvers
The guiding question of the tutorial: how do we get these two to work together? Neither paradigm alone is enough, but combined, they cover for each other's weaknesses.
Principle 1: From autocomplete to autonomous agents
To see where "neurosymbolic" lives, it helps to climb a short ladder. Each level adds one idea to the one below it.
A plain LLM is just one input, one output. Fixed workflows chain several such calls. The decisive jump is Level 3: the model itself decides when to reach outside itself. That is the moment an LLM becomes an agent, and the moment a symbolic solver can enter the loop.
Principle 2: The agentic loop
Tool calling is the mechanism that makes everything else possible. The model emits a request, an external tool runs, and the result flows back into the model's reasoning, repeated until the task is done (the ReAct loop).
This is the big jump: the model itself decides whether and when to act. It is the difference between code completion (Copilot) and a coding agent that writes, runs, reads the error, and fixes: a write–test–fix loop.
It is also exactly where the neurosymbolic bridge is built: the neural LLM on one side, a precise symbolic tool (a SAT or constraint solver) on the other. The LLM supplies fluency and intuition; the solver supplies correctness you can check.
Principle 3: A shared interface (the Model Context Protocol)
When tool calling first appeared, every agent had to be wired to every tool by hand: N × M integrations. The Model Context Protocol (MCP), introduced in late 2024, standardizes this into N + M: the "USB port for tool calling."
Thousands of MCP servers already exist (GitHub, AWS, Google Workspace, and many more). The lesson is general: a clean, reusable interface is what lets a solver drop into any agent, and any solver into one agent. We will see how a solver exposes itself this way, so that building an encoding becomes a validated, interactive conversation.
The two directions of synergy
With those principles in hand, the tutorial examines the partnership both ways.
Solvers help LLMs: offload what LLMs are bad at.
-
Hand the LLM a tool that does exact reasoning, so it stops guessing.
-
Keep every edit to the model validated, so the encoding is always well-formed.
-
An agentic coder can turn a plain-English problem statement into a checked formal model. This lowers the modeling barrier that keeps solvers out of non-experts' hands.
LLMs help solvers: inject creativity they lack.
-
An LLM proposes streamlining constraints: extra constraints that use domain intuition to prune the search space. The solver then validates each candidate, so bad guesses are simply discarded.
-
The same idea, let the LLM propose, let the solver check, turns a creative-but- unreliable generator into a dependable one.
These principles are not hypothetical: we will look at openly available tools (the MCP Solver and an agentic constraint-programming coder) where they already work end-to-end.
A little background: the silent revolution of SAT
Why is it worth bringing a solver into the loop at all? Because modern SAT solvers are astonishingly good, routinely handling formulas with millions of variables, a capability that quietly reshaped verification, planning, and optimization. A short, accessible overview:
📺 The Silent (R)evolution of SAT (Communications of the ACM)
🔗 Read the article: https://cacm.acm.org/research/the-silent-revolution-of-sat/
We will recap just enough SAT and constraint programming to follow along. No homework required.
Who should attend, and what you'll take home
This tutorial is for you if you want to combine the flexibility of LLMs with the rigor of solvers, whether you come from machine learning, optimization, formal methods, or simply want AI systems you can trust.
You will leave with:
-
a clear mental model of agentic AI: tool calling, the ReAct loop, MCP, sub-agents;
-
the neurosymbolic principle (let the LLM propose, let the solver check) and how it works in both directions;
-
pointers to runnable, open-source tools you can experiment with today.
Prerequisites: none. Format: one 90-minute session.
If "fluent but unreliable" meets "precise but rigid," sounds like a problem worth solving, come along.
References and resources
The tutorial draws mainly on the following work; these are good starting points if you want to dig deeper.
- J. K. Fichte, D. Le Berre, M. Hecher, S. Szeider. The Silent (R)evolution of SAT. Communications of the ACM 66(6):64–72, 2023. ·
- S. Szeider. Bridging Language Models and Symbolic Solvers via the Model Context Protocol. SAT 2025, LIPIcs vol. 341, 30:1–30:12.
- S. Szeider. CP-Agent: Agentic Constraint Programming. arXiv:2508.07468, 2025 (AGENT@ICSE 2026).
- F. Voboril, V. Peruvemba Ramaswamy, S. Szeider. Generating Streamlining Constraints with Large Language Models. Journal of Artificial Intelligence Research 84, 2025.
- F. Voboril, V. Peruvemba Ramaswamy, S. Szeider. Balancing Latin Rectangles with LLM-Generated Streamliners. CP 2025, LIPIcs vol. 340, 36:1–36:17.
- V. Peruvemba Ramaswamy, S. Szeider. Proven Optimally-Balanced Latin Rectangles with SAT (Short Paper). CP 2023, LIPIcs vol. 280, 48:1–48:10.
Software
-
MCP Solver — https://github.com/szeider/mcp-solver
-
Agentic Python coder (CP-Agent) — https://github.com/szeider/agentic-python-coder
