mcp-solver
The MCP Solver is a server aimed at integrating SAT, SMT, and constraint solving with large language models using the Model Context Protocol. It offers interactive capabilities for creating, editing, and solving models with three different operational modes. This includes extensive support for various problem-solving backends and a test client for experiments.
Overview
The MCP Solver connects SAT, SMT, and Constraint Solving with LLMs via the Model Context Protocol. It allows AI models to interactively create, edit, and solve constraint models using MiniZinc, SAT models with PySAT, and SMT formulas via Z3 Python. Key tool functionalities include clearing models, adding, deleting, replacing items, and solving models. Three distinct modes are available: MiniZinc, PySAT, and Z3, each with its dependencies and features. A test client based on the ReAct agent framework is included for development and experimentation, facilitating the translation of natural language problems to formal solutions.
Available Tools
- clear_model: Remove all items from the model.
- add_item: Add a new item at a specific index.
- delete_item: Delete an item at a specific index.
- replace_item: Replace an item at a specific index.
- get_model: Retrieve current model content with numbered items.
- solve_model: Solve the model with a timeout option.
Available Modes / Solving Backends
MiniZinc Mode
- Integrates with MiniZinc modeling language.
- Global constraints, optimization capabilities.
PySAT Mode
- Uses the Python SAT solving toolkit.
- Supports CNF modeling and various SAT solvers.
Z3 Mode
- Access to Z3 SMT solver.
- Rich type system and optimization capabilities.
License
The project is licensed under the MIT License.