MCP Solver

@szeider

代码仓库

基本信息

分类

其他

许可证

MIT

传输方式

stdio

作者

szeider

关于 MCP Solver

Model Context Protocol (MCP) server for constraint optimization and solving"

MCP Solver 配置

使用下面的配置,将此服务器添加到你的 MCP 客户端。

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uv",
      "args": [
        "venv"
      ]
    }
  }
}

MCP Solver 工具

Remove all items from the model

Add new item at a specific index

Delete item at index

Replace item at index

Get current model content with numbered items

Solve the model (with timeout parameter)

概览

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

常见问题

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.

其他分类下的更多 MCP 服务器

YOUB

Connect your AI assistant to your own YOUB endurance training account. Read recorded activities with full analysis, planned sessions, race goals, wellness (HRV, sleep, resting HR) and your athletic profile. Create or mov

Glasswarp

See and control a real Windows PC you own — from any MCP client, locally or remotely. Observe (UIA + screenshots), click/type/drag/scroll, launch apps, owner Live View. BYOH: your machine, your key.

Reactive Resume

amruthpillai

A one-of-a-kind resume builder that keeps your privacy in mind. Completely secure, customizable, portable, open-source and free forever. Try it out today!

39.5K

Maestro

mobile-dev-inc

Painless E2E Automation for Mobile and Web

14.8K

Senso MCP for Joomla

sensomedia

Senso MCP turns a Joomla 5 or 6 site into a remote MCP server. It runs inside Joomla itself (no extra server, no Node.js bridge) and is secured with OAuth 2.1 and Joomla's own ACL. The free pack lets an AI assistant crea