Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

MCP-Solver: Integrating Language Models with Constraint Programming Systems

Stefan Szeider

TL;DR

The paper introduces the MCP Solver, a protocol-based system that integrates Large Language Models with symbolic solvers through the open-source Model Context Protocol (MCP). It provides three backends—MiniZinc for constraint programming, PySAT for propositional satisfiability, and Z3 for SMT—within an item-based incremental editing framework that validates changes iteratively to maintain consistency. A robust execution and solution-processing pipeline ensures isolated, timeout-bounded solver runs and outputs standardized results, enabling reliable interaction in AI chat interfaces and autonomous multi-agent setups. The work demonstrates the system via show-case problems, discusses legacy and lightweight client variants, and outlines future enhancements to broaden solver backends and enable asynchronous solving and orchestration across multiple agents, highlighting practical impact for reliable LLM-assisted formal reasoning. Overall, the MCP Solver advances the integration of natural language interfaces with formal solvers, facilitating dynamic problem refinement, educational explanations, and scalable multi-agent problem solving in real-world applications.

Abstract

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.

MCP-Solver: Integrating Language Models with Constraint Programming Systems

TL;DR

The paper introduces the MCP Solver, a protocol-based system that integrates Large Language Models with symbolic solvers through the open-source Model Context Protocol (MCP). It provides three backends—MiniZinc for constraint programming, PySAT for propositional satisfiability, and Z3 for SMT—within an item-based incremental editing framework that validates changes iteratively to maintain consistency. A robust execution and solution-processing pipeline ensures isolated, timeout-bounded solver runs and outputs standardized results, enabling reliable interaction in AI chat interfaces and autonomous multi-agent setups. The work demonstrates the system via show-case problems, discusses legacy and lightweight client variants, and outlines future enhancements to broaden solver backends and enable asynchronous solving and orchestration across multiple agents, highlighting practical impact for reliable LLM-assisted formal reasoning. Overall, the MCP Solver advances the integration of natural language interfaces with formal solvers, facilitating dynamic problem refinement, educational explanations, and scalable multi-agent problem solving in real-world applications.

Abstract

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.
Paper Structure (13 sections, 3 figures)

This paper contains 13 sections, 3 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. System Architecture
  4. Incremental Validation
  5. Execution and Solution Processing
  6. Legacy Version
  7. Lightweight MCP Client
  8. Showcase Problems
  9. Conclusion
  10. Appendix: Case Studies
  11. MiniZinc Mode: Traveling Salesperson
  12. PySAT Mode: 6 Queens and 5 Knights
  13. Z3 Mode: Processor Parity Verification

Figures (3)

  • Figure 1: Sequence diagram of MCP Solver's interaction within an AI chat application.
  • Figure 2: Example for MCP Solver's item-based model editing with validation. Each modification is validated before being applied, maintaining model consistency. Numbers indicate item indices.
  • Figure 3: Sequence diagram of MCP Solver's interaction with our test client.