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

「その他」の他のコンテンツ