MCP-Solver: Integrating Language Models with Constraint Programming Systems

TL;DR

MCP-Solver integrates large language models with symbolic constraint solvers via an open standard, enhancing AI reasoning capabilities while maintaining model consistency through iterative validation.

Contribution

It introduces the Model Context Protocol (MCP), enabling seamless integration of LLMs with various symbolic solvers and supporting structured refinement.

Findings

Provides interfaces for Minizinc, PySAT, and Z3

Ensures model consistency with iterative validation

Facilitates AI reasoning with formal solvers

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.