The MCP Solver provides a powerful interface for connecting Large Language Models (LLMs) with constraint solving technologies through the Model Context Protocol. It supports multiple constraint solving backends including MiniZinc, PySAT, MaxSAT, and Z3, allowing LLMs to create, edit, and solve complex constraint problems.
MCP Solver requires Python 3.11+, the uv package manager, and solver-specific dependencies. Here's how to get started:
git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv
source .venv/bin/activate
uv pip install -e ".[all]" # Install all solvers
You can also install specific solvers instead of all:
uv pip install -e ".[mzn]"uv pip install -e ".[pysat]"uv pip install -e ".[z3]"MiniZinc provides rich constraint modeling capabilities with:
To run in MiniZinc mode:
mcp-solver-mzn
PySAT allows modeling with propositional logic using:
To run in PySAT mode:
mcp-solver-pysat
MaxSAT specializes in optimization problems with:
To run in MaxSAT mode:
mcp-solver-maxsat
Z3 provides SMT (Satisfiability Modulo Theories) capabilities with:
To run in Z3 mode:
mcp-solver-z3
The included client helps with testing and experimentation:
# Install client dependencies
uv pip install -e ".[client]"
# Verify client installation
uv run test-setup-client
The client requires an API key from an LLM provider. For Anthropic (default), set the ANTHROPIC_API_KEY environment variable.
Run the client with different solver backends:
# MiniZinc mode
uv run run-test mzn --problem <path/to/problem.md>
# PySAT mode
uv run run-test pysat --problem <path/to/problem.md>
# MaxSAT mode
uv run run-test maxsat --problem <path/to/problem.md>
# Z3 mode
uv run run-test z3 --problem <path/to/problem.md>
The MCP Solver provides these tools for interacting with models:
| Tool Name | Description |
|---|---|
clear_model |
Remove all items from the model |
add_item |
Add new item at a specific index |
delete_item |
Delete item at index |
replace_item |
Replace item at index |
get_model |
Get current model content with numbered items |
solve_model |
Solve the model (with timeout parameter) |
This example solves a theatrical casting problem with constraints:
var bool: alvarez;
var bool: cohen;
var bool: branislavsky;
var bool: davenport;
constraint alvarez \/ cohen; % Must cast either Alvarez or Cohen
constraint not (alvarez /\ cohen); % Alvarez won't work with Cohen
constraint alvarez -> davenport; % If Alvarez is cast, Davenport must be cast
constraint branislavsky; % Branislavsky must be cast
constraint not (branislavsky /\ alvarez); % Branislavsky won't work with Alvarez
constraint not (branislavsky /\ davenport); % Branislavsky won't work with Davenport
solve satisfy;
Solution: Cast Cohen and Branislavsky, but not Alvarez or Davenport.
This example places n queens on an n×n chessboard:
int: n = 10;
array[1..n] of var 1..n: queens;
constraint alldifferent(queens);
constraint alldifferent([queens[i] + i | i in 1..n]);
constraint alldifferent([queens[i] - i | i in 1..n]);
solve satisfy;
Solutions exist for all tested board sizes (n=10, 20, 30, 40) with increasing but manageable solving times.
This example finds the shortest route through Austrian province capitals:
include "globals.mzn";
int: n = 9;
array[1..n,1..n] of int: dist = [|0,65,60,184,195,319,299,478,631|65,0,125,119,130,254,234,413,566|60,125,0,184,157,281,261,440,593|184,119,184,0,208,252,136,315,468|195,130,157,208,0,136,280,459,629|319,254,281,252,136,0,217,391,566|299,234,261,136,280,217,0,188,343|478,413,440,315,459,391,188,0,157|631,566,593,468,629,566,343,157,0|];
array[1..n] of var 1..n: succ;
var int: total_dist = sum(i in 1..n)(dist[i,succ[i]]);
constraint circuit(succ);
solve minimize total_dist;
The optimal route has a total distance of 1,564 km.
To add this MCP server to Claude Code, run this command in your terminal:
claude mcp add-json "mcp-solver-mzn" '{"command":"mcp-solver-mzn","args":[]}'See the official Claude Code MCP documentation for more details.
There are two ways to add an MCP server to Cursor. The most common way is to add the server globally in the ~/.cursor/mcp.json file so that it is available in all of your projects.
If you only need the server in a single project, you can add it to the project instead by creating or adding it to the .cursor/mcp.json file.
To add a global MCP server go to Cursor Settings > Tools & Integrations and click "New MCP Server".
When you click that button the ~/.cursor/mcp.json file will be opened and you can add your server like this:
{
"mcpServers": {
"mcp-solver-mzn": {
"command": "mcp-solver-mzn",
"args": []
},
"mcp-solver-pysat": {
"command": "mcp-solver-pysat",
"args": []
},
"mcp-solver-maxsat": {
"command": "mcp-solver-maxsat",
"args": []
},
"mcp-solver-z3": {
"command": "mcp-solver-z3",
"args": []
}
}
}To add an MCP server to a project you can create a new .cursor/mcp.json file or add it to the existing one. This will look exactly the same as the global MCP server example above.
Once the server is installed, you might need to head back to Settings > MCP and click the refresh button.
The Cursor agent will then be able to see the available tools the added MCP server has available and will call them when it needs to.
You can also explicitly ask the agent to use the tool by mentioning the tool name and describing what the function does.
To add this MCP server to Claude Desktop:
1. Find your configuration file:
~/Library/Application Support/Claude/claude_desktop_config.json%APPDATA%\Claude\claude_desktop_config.json~/.config/Claude/claude_desktop_config.json2. Add this to your configuration file:
{
"mcpServers": {
"mcp-solver-mzn": {
"command": "mcp-solver-mzn",
"args": []
},
"mcp-solver-pysat": {
"command": "mcp-solver-pysat",
"args": []
},
"mcp-solver-maxsat": {
"command": "mcp-solver-maxsat",
"args": []
},
"mcp-solver-z3": {
"command": "mcp-solver-z3",
"args": []
}
}
}3. Restart Claude Desktop for the changes to take effect