mcp-solver

The MCP Solver exposes multiple backend solvers (MiniZinc, PySAT, MaxSAT, Z3, and ASP) through the Model Context Protocol, enabling an LLM to compose, modify, and solve constraint problems interactively. It provides a command-driven interface for building models: you can clear the current model, add or remove items, replace items at a given index, inspect the model content with numbered items, and trigger solving with an optional timeout. This setup makes it possible to iteratively refine problem encodings in MiniZinc, SAT (via PySAT), MaxSAT, SMT (via Z3), and ASP (via Clingo), while allowing your agent to switch backends as needed depending on the problem class.

Key tools available to the MCP client include:

• clear_model: remove all items from the current model
• add_item: append a new constraint or variable at a specific position
• delete_item: remove an item by index
• replace_item: replace an existing item at a given index
• get_model: retrieve the current model content with item indices
• solve_model: solve the current model, with optional timeout control

The MCP Test Client is also included to experiment with the server interactions, offering commands tailored to each backend (mzn, pysat, maxsat, z3, asp) via uv run run-test. This client relies on an API key for an LLM provider and supports multiple LLM backends (Anthropic, OpenAI, Gemini, OpenRouter, or local models). Use it to translate natural language problems into formal encodings and then invoke the MCP Solver to obtain solutions.

Prerequisites:

• Python 3.11+ installed on your system
• git installed
• uv (the Python package manager from Astral) installed via instructions in the project
• Internet access to clone the repository and install dependencies

Step-by-step installation (Linux/macOS/Windows):

1. Install uv if you don’t have it yet (example using Python's pip):

pip install uv

2. Clone the MCP Solver repository:

git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver

3. Set up a virtual environment and install all solvers (as recommended by the project):

uv venv
source .venv/bin/activate  # on Unix/macOS
# On Windows use: .venv\Scripts\activate
uv pip install -e ".[all]"

4. Run the MCP Solver server locally in Python mode:

uv run server  # or: python -m mcp_solver  (depending on project entrypoints)

5. For Windows/macOS/Linux, follow the detailed Windows/macOS/Linux installation in INSTALL.md provided in the repository for any platform-specific nuances.

If you prefer a different start method, you can also run the module directly once dependencies are installed:

python -m mcp_solver

Notes and tips:

• The solver backends require additional system dependencies (MiniZinc, Z3, and PySAT components). Install with the per-backend commands documented under Available Modes in the README. For MiniZinc, install the minizinc package; for Z3, install z3-solver; for PySAT, install python-sat.
• The MCP Test Client requires an API key from an LLM provider. Set the ANTHROPIC_API_KEY (or other provider keys) in your environment or in a .env file at the project root.
• Environment variables for solver backends (like path to MiniZinc, CLINGO, or Z3) may be required depending on your platform. Refer to INSTALL.md and the backend-specific sections for details.
• If you encounter issues with environment activation, ensure your shell is correctly sourcing the virtual environment and that the correct Python interpreter is used when launching the server.
• The MCP interface is designed to be used by an LLM-driven client; when integrating with an agent, you can map natural language prompts to the available commands (clear_model, add_item, etc.) and then call solve_model to obtain results.