Record link: 
http://hdl.handle.net/20.500.12708/225646
-
Title: 
Bridging Language Models and Symbolic Solvers via the Model Context Protocol
en
Citation: 
Szeider, S. (2025). Bridging Language Models and Symbolic Solvers via the Model Context Protocol. In J. Berg & J. Nordström (Eds.), 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.SAT.2025.30
-
Publisher DOI: 
10.4230/LIPIcs.SAT.2025.30
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Szeider, Stefan 
-
Organisational Unit: 
E192-01 - Forschungsbereich Algorithms and Complexity 
E056-13 - Fachbereich LogiCS 
E056-23 - Fachbereich Innovative Combinations and Applications of AI and ML (iCAIML) 
-
Published in: 
28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) 
-
ISBN: 
978-3-95977-381-2
-
Volume: 
341
-
Date (published): 
7-Aug-2025
-
Event name: 
28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) 
en
Event date: 
12-Aug-2025 - 15-Aug-2025
-
Event place: 
Glasgow, United Kingdom of Great Britain and Northern Ireland (the)
-
Number of Pages: 
12
-
Publisher: 
Schloss Dagstuhl
-
Peer reviewed: 
Yes
-
Keywords: 
Agents; Constraint Programming; Large Language Models; Maximum Satisfiability; Model Context Protocol; SAT Modulo Theories; Satisfiability Solvers
en
Abstract: 
This paper presents the MCP Solver, a system that bridges large language models with symbolic solvers through the Model Context Protocol (MCP). The system includes a server and a client component. The server provides an interface to constraint programming (via MiniZinc Python), propositional satisfiability and maximum satisfiability (both via PySAT), and SAT modulo Theories (via Python Z3). The client contains an agent that connects to the server via MCP and uses a language model to autonomously translate problem statements (given in English) into encodings through an incremental editing process and runs the solver. Our experiments demonstrate that this neurosymbolic integration effectively combines the natural language understanding of language models with robust solving capabilities across multiple solving paradigms.
en
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

14
checked on Jan 27, 2026

Google ScholarTM

Check