MCP.so
登录

MCP Solver

@szeider

代码仓库

关于 MCP Solver

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

配置

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

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

工具

6

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

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.

常见问题

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.

评论

基本信息

分类

其他

许可证

MIT

传输方式

stdio

作者

szeider

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

IDA Pro MCP

mrexodia

AI-powered reverse engineering assistant that bridges IDA Pro with language models through MCP.

9.9K

Inbox Zero AI MCP

elie222

The world's best AI personal assistant for email. Open source app to help you reach inbox zero fast.

11.6K

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

Mobile Mcp

mobile-next

Model Context Protocol Server for Mobile Automation and Scraping (iOS, Android, Emulators, Simulators and Real Devices)

5.4K

Website

FunnyWolf

Adversary simulation and Red teaming platform with AI

5.1K