MCP Solver

MCP Solver

制約充足（SAT、MaxSAT、SMT、CP、ASP、DP）用の MCP サーバーです。接続された LLM ホストを、ソルバーのプログラムを作成するエージェントに変えます。ホストには、実際のソルバーライブラリを事前読み込みした Python カーネル、選択したバックエンド向けのモデル化手順、および提出ゲートが提供されます。ホストは問題をエンコードし、実際のソルバーで実行して検証したうえで、最終プログラムを提出します。成果物は、解と、それを生成した検証済みソルバープログラムです。

バージョン 4 はアーキテクチャを全面的に再設計しました。 MCP インターフェースとソルビングエンジンの両方が変更されています。SAT 2025 の論文に基づく設計（v3）は、v3 ブランチにそのまま残っています。 以下の「v3 から v4 へ」をご覧ください。

MCP サーバー

mcp-solver-serve は stdio 経由で実行され、Claude Desktop、Claude Code、Cursor、自作のクライアントなど、あらゆる MCP ホストで動作します。ソルビング自体はホスト側の LLM が行います。サーバーはソルバーツールキットであり、LLM を実行せず、API キーも必要ありません。

• select_backend(solver) は、選択したバックエンドのソルバーライブラリとヘルパー関数を備えた永続的な IPython カーネルをセットアップし、そのバックエンド向けのモデル化手順を返します。再度呼び出すと、次の問題に向けてカーネルを再利用します。
• カーネルツール（python_exec、python_reset、python_status、python_interrupt）を使うと、ホストは実際のソルバープログラムを作成、実行、検証できます。python_exec のみを呼び出した場合は、自動的にソルビングカーネルへルーティングされます。
• submit_code(code) は最終提出のための機能です。自己完結型の最終プログラムを構文チェックし、成功すると保存して、MCP リソース（mcp-solver://submissions/{id}）としてリンクし、判定結果を構造化コンテンツで返します。
• リソース： mcp-solver://guide（バックエンドの選択とワークフロー）および mcp-solver://template/{solver}（選択せずに閲覧できる、モデル化手順の全内容）。
• 統計情報（任意）：サーバーの env に MCP_SOLVER_STATS=/path/to/stats.jsonl を設定すると、ソルビングの各回について、ツール呼び出し数、実行失敗、提出、実時間を JSON 1 行に記録します。設計上、ホストのトークン数はサーバーから確認できません。ツールの使用状況がホスト間で比較できる指標です。（submit_code の結果にも、構造化コンテンツとして簡潔な統計スナップショットが含まれます。CLI 経由では --stats-json によりトークン数と実際の OpenRouter 費用が報告されます。）

チェックアウトから Claude Desktop を設定する方法（現時点で動作するセットアップであり、常に開発用の手順です。インストールを参照してください）：

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uv",
      "args": ["run", "--project", "/path/to/mcp-solver", "--extra", "agent", "mcp-solver-serve"]
    }
  }
}

PyPI のパッケージ名の移管が完了すれば、チェックアウトは不要になります。それまでは、この設定で無関係な古い v2.0.0 のアップロード版が取得されるため、まだ使用しないでください。

{
  "mcpServers": {
    "mcp-solver": {
      "command": "uvx",
      "args": ["--python", "3.14", "--from", "mcp-solver[agent]", "mcp-solver-serve"]
    }
  }
}

サーバーに API キーは必要ありません。ソルビングを行うモデルはホストに属します。以下のコマンドラインでの使用では、独自のエージェントを使用するため、OpenRouter のキーが必要です。

必要条件

• Python 3.13 または 3.14（まだ 3.15 には対応していません。ソルバーカーネルはサーバーの Python バージョンで実行されますが、ortools と python-sat はまだ 3.15 用のホイールを公開していません）
• uv（実行時の必須要件です。ソルバーライブラリはソルビング時に uv run --with 経由で提供されます）
• OpenRouter の API キー（CLI とベンチマークハーネスでのみ必要です。MCP サーバー自体はキーなしで動作します）

インストール

v4 はまだ PyPI からインストールできません。 PyPI のパッケージ名 mcp-solver は、古い v2.0.0 コードをアップロードした第三者によって保持されており、PyPI は紛らわしい類似名をブロックします。PEP 541 に基づく名称移管の申請は保留中です。解決するまでは、チェックアウトからインストールしてください。

git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv                         # Python 3.13 or 3.14, per pyproject.toml
uv pip install -e ".[agent]"

# OpenRouter key — only needed for the CLI path, not the MCP server:
mkdir -p ~/.config/coder
echo 'OPENROUTER_API_KEY="sk-or-v1-..."' > ~/.config/coder/.env

詳細とトラブルシューティングについては、INSTALL.mdをご覧ください。

コマンドラインでの使用

mcp-solver CLI は MCP ホストなしで同じソルビングパイプラインを実行するため、スクリプトやベンチマークに便利です。

mcp-solver pysat "Place 8 non-attacking queens on an 8x8 board and give one solution."
mcp-solver pysat --problem tests/problems/pysat/n_queens.md

解の JSON は標準出力に出力されます。提出されたソルバープログラム（例：n_queens_code.py）と完全な実行ログ（run_*.json）は作業ディレクトリに保存されます。

オプション	説明
--problem FILE	テキストの代わりに Markdown ファイルからタスクを読み込みます
--model NAME	エージェントのモデル：gpt56terra などのエイリアス、または OpenRouter の完全な ID（デフォルト：gpt56terra）
--workdir DIR	実行用の作業ディレクトリ（デフォルト：現在のディレクトリ）
--step-limit N	停止するまでのエージェントの最大ステップ数（デフォルト：30）
-q, --quiet	各ステップの進捗出力を抑制します
--dev [PATH]	開発モード：ローカルチェックアウトからヘルパーとテンプレートを使用します（--dev のみの場合は自動検出。チェックアウト内では自動的に有効。MCP_SOLVER_DEV も使用）
--no-dev	開発モードを無効にし、公開済みの（PyPI で固定された）ヘルパーを使用します
--stats-json FILE	実行統計を JSON 形式で FILE に書き込みます

編集可能なクローンから実行すると、CLI は開発モードで動作します。ヘルパーとテンプレートはソースチェックアウトから取得され（自動検出）、出所を示す行が stderr に出力されます。

mcp-minion

CLI は内部で mcp-minion を実行します。これは、このリポジトリでワークスペースパッケージ minion/ として開発された、MCP 上で動作する最小限の ReAct エージェントです。Claude Desktop などの完全な MCP ホストに代わる軽量なバッチ実行可能ツールです。スタンドアロン CLI の接続先に mcp-solver-serve（または任意の MCP サーバー）を指定すると、チャットホストで対話的に行う処理をスクリプト化できます（minion/README.md を参照）。デフォルトのエージェントモデルは gpt56terra で、OpenRouter の openai/gpt-5.6-terra に対応する同梱エイリアスです。

バックエンド

各バックエンドは、CLI の最初の引数（または select_backend ツール）で選択します。適切なソルバーライブラリが、ソルビング時のカーネルに自動的に組み込まれます。

バックエンド	対象領域	ソルバーライブラリ
pysat	ブール充足可能性（SAT）	python-sat
maxsat	重み付き最適化	python-sat (RC2)
z3	SMT ソルビング／検証	z3-solver
cpmpy	制約プログラミング（CP）	cpmpy
clingo	解集合プログラミング（ASP）	clingo
didp	動的計画法（DIDP）	didppy

v3 での MiniZinc モードは廃止されました。制約プログラミングは現在、CPMpy が担います。didp バックエンドは、ドメイン独立型動的計画法（Kuroiwa & Beck）に基づいており、didppy の任意停止可能なビームサーチで問題を解きます。問題は状態遷移系としてモデル化され、経路探索、順序付け、スケジューリング、パッキングに自然に適合します。

動作の仕組み

基本のmcp-solverパッケージは、依存関係を持たないソルバーヘルパーライブラリです （mcp_solver.helpers.{pysat,maxsat,z3}。CPMpy、Clingo、DIDPのバックエンドにはヘルパーモジュールは不要です）。環境にpipインストールされることはありません。代わりに、バックエンドのソルバーライブラリとともに、uv run --with mcp-solver==<version>を介して、各ソルバー実行時のカーネルに注入されます。これにより、ホスト環境をクリーンに保ち、各ソルバー実行の再現性を確保します。

各バックエンドにはプロジェクトテンプレートが付属しています。これは、エンコーディング規約、出力形式、そのソルバー用のヘルパーAPIを記載したMarkdownプロンプト（パッケージデータ）です。テンプレートは問題を解く側に渡されます。MCPホストはselect_backendからテンプレートを受け取り、CLIはmcp-minionエージェントにシステムプロンプトとして渡します。どちらの場合も、問題を解くLLMが、agentic-python-coderのipython_mcpサーバーを使った永続的なIPythonカーネル内で、記述→実行→検証のループを進めます。そして、自己完結型の最終プログラムをsubmit_codeで送信して、ソルバー実行を終了する必要があります（サーバー側で構文チェックされ、カーネルによってディスクに書き込まれることはありません）。MCP経由では、受理された送信内容がリソースとしてホストに紐付けられます。CLI経由では、クライアントが最後に成功した送信内容を抽出し、<basename>_code.pyに書き込んでから、新しいuvカーネルで再実行し、答えを生成します。

ベンチマークハーネス

mcp-solver-benchは、同梱のテスト問題をtests/problems/<solver>/からエンドツーエンドで実行し、問題ごとの*_ground_truth.pyバリデーターを使って各結果を検証します（バリデーターは標準入力から解のJSONを読み込み、{"valid": ..., "message": ...}を返します）。

# Benchmark every backend
mcp-solver-bench

# Specific backends, several runs each, in parallel
mcp-solver-bench pysat z3 --runs 3 --jobs 4

各実行には--step-limit（デフォルト：エージェントのステップ数30）による上限があり、結果は出力ディレクトリのresults.jsonlに追記されます。

同じ問題はpytestのエンドツーエンドテストとしても実行できます（uv run pytest minion/e2e_tests -k didp）。また、mcp-solver-runfolder <solver> <problem> <dir>を使うと、これらの問題用のスタンドアロンなmcp-minion実行フォルダーを作成できます。

現状：gpt-5.6-terraを使った実行では、同梱のテスト問題30件すべてが正しく解けます。4件のdidp問題（TSPTW、ナップサック、重み付き納期遅延、タレントスケジューリング）も含まれ、いずれもすべての実行で最適性が証明された解に到達しています。MCPサーバー経由の動作は、ホストとしてClaude Opusを使って検証済みです。CP-Bench（101件）とASP-Bench（128件）にわたる229件すべてのインスタンスが、厳密な意味検証のもとで正しく解けています。同梱のSAT、MaxSAT、SMTの問題も同様です。

v3 から v4 へ：新しいアーキテクチャ

SAT 2025 の論文「Bridging Language Models and Symbolic Solvers via the Model Context Protocol」では、 v3 について説明しています。これは、モデル編集ツール（add_item、 replace_item、solve_model など）を公開する MCP サーバーで、チャット LLM が 項目を一つずつ追加してソルバーモデルを構築し、サーバー内で求解を行います。

v4 は、CP-Agent（LLM4Code 2026）および ASP-Bench（NSE '26）の論文で示された IPython カーネル方式を採用しています。ホスト LLM がプロトコルツールを使って モデルを編集する代わりに、専用のコーディングエージェントが永続的な IPython カーネル内で作業します。実際の Python ソルバープログラムを反復的に記述し、 実際のソルバーで実行して結果を独立に検証した後、そのプログラムを解答として 提出します。

	v3（SAT 2025 の論文）	v4（CP-Agent／ASP-Bench 方式）
作業の担当者	MCP 編集ツールを使うホストのチャット LLM	ソルバープログラマーとして働くホスト LLM（またはバッチ実行用の mcp-minion）
作業単位	モデル項目（add_item、solve_model など）	実行可能な完全な Python ソルバープログラム
実行	MCP サーバー内	永続的な IPython カーネル（ipython_mcp）内
検証	ホスト LLM による手動検証	ループに組み込み：実行 → チェック → submit_code
成果物	一時的なモデル状態	検証済みで再実行可能な、保持できるプログラム
ホストインターフェース	多数の細かなモデル編集ツール	求解カーネル：select_backend、python_exec、submit_code
バックエンド	MiniZinc、PySAT、MaxSAT、Z3、ASP	PySAT、MaxSAT、Z3、CPMpy、Clingo、DIDP

引用文献

• Stefan Szeider, "Bridging Language Models and Symbolic Solvers via the Model Context Protocol", SAT 2025. v3 のアーキテクチャについて説明しています（v3 ブランチ）。 DOI 10.4230/LIPIcs.SAT.2025.30
• Stefan Szeider, "CP-Agent: Agentic Constraint Programming", in Proceedings of the 3rd International Workshop on Large Language Models For Code (LLM4Code 2026), pages 6–13, ACM, 2026. v4 の基盤となる IPython カーネル 方式です。 DOI 10.1145/3786181.3788711
• Stefan Szeider, "ASP-Bench: From Natural Language to Logic Programs", in Proceedings of the 2026 IEEE/ACM 2nd International Workshop on Neuro-Symbolic Software Engineering (NSE '26), pages 1–8, ACM, 2026. v4 のテスト問題で使用されている、検証を条件とするベンチマーク手法です。 DOI 10.1145/3786168.3788402

ライセンス

MIT。詳しくは LICENSE を参照してください。