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.

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

Hindsight

vectorize-io

Hindsight: Agent Memory That Learns

50.4K

Maestro

mobile-dev-inc

Painless E2E Automation for Mobile and Web

14.8K

Klarix Intelligence Engine

Klarix

B2B competitive intelligence, live sales battlecards, 5-axis ICP prospect fit scoring, and tech stack teardowns over MCP and REST with cited public-web evidence.

Codelf

unbug

A search tool helps dev to solve the naming things problem.

14.2K

Volley.sh

Volley

A good sequence diagram can solve almost any communication problem in engineering. Volley lets your agent write them as plain text, with the real request and response payloads on every arrow. It checks its own syntax wi