Bridging Language Models and Symbolic Solvers via the Model Context Protocol
Open accessAbstract
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.
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
The claims and statistics of this paper haven’t been checked yet.
Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
The closest precedent is the MCP-Solver discussed in [31], which exposes constraint, SAT, SMT and answer sets backends (MiniZinc, PySAT, Z3 and clingo) but not Prolog-style SLDNF resolution with unification and backtracking over a database of clauses.
“The closest precedent is the MCP-Solver discussed in [31], which exposes constraint, SAT, SMT and answer sets backends (MiniZinc, PySAT, Z3 and clingo) but not Prolog-style SLDNF resolution with unification and backtracking over a database of clauses.”
From PrologMCP: A Standardized Prolog Tool Interface for LLM Agents (2026) · cites this paper as [31]
Split into 2 atoms — 0 confirmed, 2 partially supported, 0 disputed, 0 misattributed, 0 unverifiable. Expand the claim to see per-atom verdicts.
Experimental — accuracy not yet measured
Self-check
Percentages, sums and reported differences re-computed from the paper’s own numbers.
The self-check needs the paper’s full text.
Cites
No references could be resolved yet.
Research works printed but not linked: 22
- Aidan Curtis, Nishanth Kumar, Jing Cao, Tomás Lozano-Pérez, and Leslie Pack Kaelbling. Trust the PRoC3S: Solving long-horizon robotics problems with llms and constraint satisfaction. In Pulkit Agrawal, Oliver Kroemer, and Wolfram Burgard, editors, Conference on Robot Learning, 6-9 November 2024, Munich, Germany, volume 270 of Proceedings of Machine Learning Research, pages 1362-1383. PMLR, 2024. URL: https://proceedings.mlr.press/ v270/curtis25a.html.
- Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24. · DOI · Paper page
- Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. PAL: program-aided language models. In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett, editors, International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA, volume 202 of Proceedings of Machine Learning Research, pages 10764-10799.
- PMLR, 2023. URL: https://proceedings.mlr.press/v202/gao23f.html.
- Jiawei Gu, Xuhui Jiang, Zhichao Shi, Hexiang Tan, Xuehao Zhai, Chengjin Xu, Wei Li, Yinghan Shen, Shengjie Ma, Honghao Liu, Yuanzhuo Wang, and Jian Guo. A survey on LLM-as-a-Judge. CoRR, abs/2411.15594, 2024. doi:10.48550/arXiv.2411.15594. · DOI · Paper page
- Alexey Ignatiev, Zi Li Tan, and Christos Karamanos. Towards universally accessible SAT technology. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, pages 16:1-16:11. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.SAT.2024.16. S. Szeider 30:11 · DOI
- Sumit Kumar Jha, Susmit Jha, Patrick Lincoln, Nathaniel D. Bastian, Alvaro Velasquez, Rickard Ewetz, and Sandeep Neema. Counterexample guided inductive synthesis using large language models and satisfiability solving. In IEEE Military Communications Conference, MILCOM 2023, Boston, MA, USA, October 30 -Nov. 3, 2023, pages 944-949. IEEE, 2023. doi:10.1109/MILCOM58377.2023.10356332. · DOI
- Subbarao Kambhampati, Karthik Valmeekam, Lin Guan, Mudit Verma, Kaya Stechly, Siddhant Bhambri, Lucas Saldyt, and Anil Murthy. Position: Llms can't plan, but can help planning in LLM-modulo frameworks. In Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024. OpenReview.net, 2024. URL: https://openreview. net/forum?id=Th8JPEmH4z.
- Bill Yuchen Lin, Ronan Le Bras, Kyle Richardson, Ashish Sabharwal, Radha Poovendran, Peter Clark, and Yejin Choi. Zebralogic: On the scaling limits of llms for logical reasoning. CoRR, abs/2502.01100, 2025. doi:10.48550/arXiv.2502.01100. · DOI · Paper page
- Zhan Ling, Yunhao Fang, Xuanlin Li, Zhiao Huang, Mingu Lee, Roland Memisevic, and Hao Su. Deductive verification of chain-of-thought reasoning. In Alice Oh, Tris- tan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, Decem- ber 10 -16, 2023, 2023. URL: http://papers.nips.cc/paper_files/paper/2023/hash/ 72393bd47a35f5b3bee4c609e7bba733-Abstract-Conference.html.
- Kostis Michailidis, Dimos Tsouros, and Tias Guns. Constraint modelling with llms using in-context learning. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain, volume 307 of LIPIcs, pages 20:1-20:27. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CP.2024.20. · DOI
- Seyed-Iman Mirzadeh, Keivan Alizadeh, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. GSM-Symbolic: understanding the limitations of mathematical reasoning in large language models. CoRR, abs/2410.05229, 2024. doi:10.48550/arXiv.2410.05229. · DOI · Paper page
- Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. Minizinc: Towards a standard CP modelling language. In Christian Bessiere, editor, Principles and Practice of Constraint Programming -CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, volume 4741 of Lecture Notes in Computer Science, pages 529-543. Springer, 2007. doi:10.1007/ 978-3-540-74970-7_38. · DOI
- Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-LM: empow- ering large language models with symbolic solvers for faithful logical reasoning. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023, pages 3806-3824. Association for Computational Linguistics, 2023. doi:10.18653/V1/2023.FINDINGS-EMNLP.248. · DOI · Paper page
- Chengwen Qi, Ren Ma, Bowen Li, He Du, Binyuan Hui, Jinwang Wu, Yuanjun Laili, and Conghui He. Large language models meet symbolic provers for logical reasoning evaluation. CoRR, abs/2502.06563, 2025. doi:10.48550/arXiv.2502.06563. · DOI
- Florian Régin, Elisabetta De Maria, and Alexandre Bonlarron. Combining constraint pro- gramming reasoning with large language model predictions. In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain, volume 307 of LIPIcs, pages 25:1-25:18. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CP.2024.25. S AT 2 0 2 5 30:12 Bridging Language Models and Symbolic Solvers 21 André Schidler and Stefan Szeider. Extracting problem structure with LLMs for optimized SAT local search. In The 18th International Symposium on Combinatorial Search (SoCS 2025), 2025. To Appear. · DOI
- Parshin Shojaee, Iman Mirzadeh, Keivan Alizadeh, Maxwell Horton, Samy Bengio, and Mehrdad Farajtabar. The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity, 2025. arXiv:2506.06941. · arXiv
- Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, and Stefan Szeider. Stream- LLM: Enhancing constraint programming with large language model-generated stream- liners. In 2025 IEEE/ACM 1st International Workshop on Neuro-Symbolic Software Engineering (NSE), pages 17-22, Los Alamitos, CA, USA, 5 2025. IEEE Computer Soc. URL: https://doi.ieeecomputersociety.org/10.1109/NSE66660.2025.00010, doi: 10.1109/NSE66660.2025.00010. · DOI
- Yuxuan Wan, Wenxuan Wang, Yiliu Yang, Youliang Yuan, Jen-tse Huang, Pinjia He, Wenxiang Jiao, and Michael R. Lyu. Logicasker: Evaluating and improving the logical reasoning ability of large language models. In Yaser Al-Onaizan, Mohit Bansal, and Yun-Nung Chen, editors, Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Miami, FL, USA, November 12-16, 2024, pages 2124-2155. Association for Computational Linguistics, 2024. doi:10.18653/V1/2024.EMNLP-MAIN.128. · DOI
- Haoze Wu, Clark W. Barrett, and Nina Narodytska. Lemur: Integrating large language models in automated program verification. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net, 2024. URL: https://openreview.net/forum?id=Q3YaCghZNt.
- Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik R. Narasimhan, and Yuan Cao. ReAct: synergizing reasoning and acting in language models. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. URL: https://openreview.net/forum?id=WE_vluYUL-X.
- Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. Satlm: Satisfiability-aided lan- guage models using declarative prompting. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Informa- tion Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 -16, 2023, 2023. URL: http://papers.nips.cc/paper_files/paper/2023/hash/ 8e9c7d4a48bdac81a58f983a64aaf42b-Abstract-Conference.html.
Cited by
Sorted by citations
PrologMCP: A Standardized Prolog Tool Interface for LLM Agents
Mensfelt, A., Prabhakaran, A., Haret, A., Trencsenyi, V., & Stathis, K. (2026) · arXiv · doi:10.48550/arxiv.2606.14935 · Cited by 1 · see citing works
- Authors
- Szeider, S.
- Affiliations
- TU Wien (AT)
- Corresponding author
- Szeider, Stefan
- ORCID
- Szeider, Stefan
- Venue
- Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- Publisher
- Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- Published
- 2025
- OpenAlex
- W7223737154
- Cited by
- 5
- References
- 0
- Citations by year
- 2026: 5
- FWCI
- 1.76
- Type
- journal article
- Language
- en
- Open access
- green
- drops.dagstuhl.de
- Licence
- Locations
- DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) (submittedVersion, cc-by)
- Leibniz international proceedings in informatics (cc-by)
- Topics
- Physical Sciences › Computer Science › Computer Networks and Communications › Constraint Satisfaction and Optimization
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Physical Sciences › Computer Science › Artificial Intelligence › AI-based Problem Solving and Planning
- Keywords
- Model Context Protocol, large language models, symbolic solvers, neural-symbolic integration, constraint programming, propositional satisfiability, MaxSAT, SAT modulo theories, MiniZinc, Z3, problem encoding, LLM agents
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
