MCP Solver: A Summary

The MCP Solver is a Model Context Protocol (MCP) server that integrates SAT, SMT, and constraint solving capabilities with Large Language Models (LLMs). It enables AI models to interactively create, edit, and solve constraint models in MiniZinc, SAT models in PySAT, and SMT formulas in Z3 Python.

The tool suite includes functionalities like clear_model, add_item, delete_item, replace_item, get_model, and solve_model. It supports Python 3.11+ and requires specific dependencies for each mode (MiniZinc, PySAT, Z3). Installation instructions are detailed in INSTALL.md, with a quick start guide provided.

The solver offers MiniZinc, PySAT, and Z3 modes, each with unique features and dependencies. An MCP test client, based on the ReAct agent framework, is included for development and experimentation, requiring an LLM API key. Examples demonstrate the solver's capabilities in solving problems like the N-Queens and Traveling Salesperson problems. The project is licensed under the MIT License.