# MCP-Solver: Integrating Language Models with Constraint Programming Systems

arXiv: https://arxiv.org/abs/2501.00539 · HTML: https://mlsanity.com/paper/2501.00539/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Placed in Tool learning and function calling, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 28 references that are in the map.
- First posted on arXiv 31 Dec 2024.

## Placed in

- LLM agents and tool use / [Tool learning and function calling](https://mlsanity.com/agents/tool-learning-and-function-calling/)

## Builds on (most cited first, 14 of 14)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [Deductive Verification of Chain-of-Thought Reasoning](https://mlsanity.com/paper/2306.03872/) (2023)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Do Language Models Plagiarize?](https://mlsanity.com/paper/2203.07618/) (2022)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models](https://mlsanity.com/paper/2401.00757/) (2024)
- [Trust the PRoC3S: Solving Long-Horizon Robotics Problems with LLMs and Constraint Satisfaction](https://mlsanity.com/paper/2406.05572/) (2024)
- [Combining Constraint Programming Reasoning with Large Language Model Predictions](https://mlsanity.com/paper/2407.13490/) (2024)
- [Generating Streamlining Constraints with Large Language Models](https://mlsanity.com/paper/2408.10268/) (2024)
- [Calculating Originality of LLM Assisted Source Code](https://mlsanity.com/paper/2307.04492/) (2023)

## Built on by (most cited first, 10 of 10)

- [Optimizing Prompt Sequences using Monte Carlo Tree Search for LLM-Based Optimization](https://mlsanity.com/paper/2508.05995/) (2025)
- [Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry](https://mlsanity.com/paper/2505.14479/) (2025)
- [Distributed Multi-Agent Coordination Using Multi-Modal Foundation Models](https://mlsanity.com/paper/2501.14189/) (2025)
- [LLMs versus the Halting Problem: Characterizing Program Termination Reasoning](https://mlsanity.com/paper/2601.18987/) (2026)
- [CP-Model-Zoo: A Natural Language Query System for Constraint Programming Models](https://mlsanity.com/paper/2509.07867/) (2025)
- [Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability](https://mlsanity.com/paper/2605.29687/) (2026)
- [Large Language Models as Optimizers: A Survey of Direct vs. Tool-Augmented Approaches and Their Performance Frontiers](https://mlsanity.com/paper/2606.15577/) (2026)
- [SPL: Orchestrating Workflows with Declarative Deterministic-Probabilistic Composition](https://mlsanity.com/paper/2607.07727/) (2026)
- [Automating Attack Graph Construction for Agentic Pentesting. Towards Neuro-Symbolic Vulnerability Hunting](https://mlsanity.com/paper/2609.15523/) (2026)
- [SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers](https://mlsanity.com/paper/2610.14402/) (2026)

## Abstract (arXiv)

The MCP Solver bridges Large Language Models (LLMs) with symbolic solvers through the Model Context Protocol (MCP), an open-source standard for AI system integration. Providing LLMs access to formal solving and reasoning capabilities addresses their key deficiency while leveraging their strengths. Our implementation offers interfaces for constraint programming (Minizinc), propositional satisfiability (PySAT), and SAT modulo Theories (Python Z3). The system employs an editing approach with iterated validation to ensure model consistency during modifications and enable structured refinement.