MCP Solver

What is MCP Solver?

MCP Solver is a Model Context Protocol server that exposes constraint solving, SAT, SMT, and ASP capabilities to Large Language Models. It integrates with MiniZinc, PySAT, Z3 Python, and Clingo, allowing AI models to interactively create, edit, and solve constraint models through the MCP interface.

How to use MCP Solver?

Requires Python 3.11+, uv package manager, and solver-specific dependencies. Clone the repository, create a virtual environment, and install with uv pip install -e ".[all]" for all solvers. Run a mode-specific command (e.g., mcp-solver-mzn for MiniZinc) to start the MCP server. Alternatively, use the included test client with uv run run-test <mode> --problem <path/to/problem.md>.

Key features of MCP Solver

• Provides six MCP tools for model manipulation and solving
• Supports five solving backends: MiniZinc, PySAT, MaxSAT, Z3, and ASP
• Enables creation, editing, deletion, and replacement of model items
• Offers SAT, optimization, SMT, and answer set programming capabilities
• Includes a ReAct-based test client for natural language problem translation
• Supports multiple SAT solvers (Glucose3, Glucose4, Lingeling, etc.)
• Features template library for common modeling patterns (Z3 mode)

Use cases of MCP Solver

• Casting problem: satisfying logical constraints for theatrical cast selection
• N-Queens problem: checking placement feasibility and comparing solve times
• Traveling Salesperson Problem: finding shortest route via optimization
• Solving propositional CNF formulas using PySAT mode
• Solving SMT formulas with rich type system via Z3 mode

FAQ from MCP Solver

What are the system requirements?

Python 3.11+, uv package manager, and solver-specific dependencies (MiniZinc, PySAT, Z3, Clingo). Supports macOS, Windows, and Linux.

Which solver backends are available?

Five modes: MiniZinc (constraint programming), PySAT (SAT), MaxSAT (weighted optimization), Z3 (SMT), and ASP (logic programs with Clingo).

How do I install and run a specific mode?

Clone repo, install with uv, then run the mode-specific command (e.g., mcp-solver-mzn for MiniZinc or mcp-solver-pysat for PySAT).

What tools does the MCP server provide?

Six tools: clear_model, add_item, delete_item, replace_item, get_model, and solve_model (with timeout parameter).

Can I use the server with different LLM providers?

Yes, the test client supports Anthropic, OpenAI, Google (Gemini), OpenRouter, and local models via LM Studio. Set the corresponding API key via environment variable.