Bridging Language Models and Constraint Solvers via the Model Context Protocol
A protocol-based architecture that lets large language models invoke symbolic solvers as tools through the Model Context Protocol, giving them reliable formal reasoning they otherwise lack. A single server exposes constraint-programming (MiniZinc), propositional-SAT (PySAT), and SMT (Z3) backends behind a uniform item-based model-editing interface, with incremental validation after each edit ensuring the encoding stays consistent and the model receives immediate, structured feedback for iterative refinement.
2501.00539
The MCP Solver is an open-source server implementing the Model Context Protocol so that large language models can invoke symbolic solvers as tools, compensating for LLMs' weakness in formal logical r…