MCP-Solver: Integrating Language Models with Constraint Programming Systems
This work addresses a key deficiency in LLMs for AI system integration, though it appears incremental as it builds on existing protocols and solvers.
The paper tackles the problem of integrating Large Language Models (LLMs) with symbolic solvers to address their reasoning deficiencies, resulting in the MCP-Solver system that provides interfaces for constraint programming, propositional satisfiability, and SAT modulo Theories.
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.