本文へスキップ
ReviewRamble

週刊ブリーフ

AIのレビューを、あなたの受信箱に。

  • ツール、モデル、MCPサーバー、リポジトリの新しいレビュー(結論を最初に)
  • 変更があったときに再確認した価格と評価
  • 公開された新しい分析記事

モデル、エージェント、MCPサーバー、そして本当に時間をかける価値のあるツール。

週に1通です。配信停止は各メールのリンクからできます。 メールアドレスの利用について

MCP Solver

SAT、MaxSAT、SMT、制約、ASPソルバー用の本物のプログラムをエージェントに書かせ、実行し、検証させる研究水準のサーバー。

レビュー: Sheela · 更新

導入ガイド オープンソース

当サイトの評価

3.9/5

モデルが頭の中で解くべきではないスケジューリングやパズルの問題に対する正しい発想ですが、今のところはリポジトリからしか入れられないことと、モデルが書いたコードを何でも実行するカーネルが足かせです。

MCP Solverとは?

Stefan SzeiderによるMCP Solverは、Claude DesktopやClaude CodeなどのMCPホストをソルバーのプログラマーに変えます。ホストはバックエンドを選び、モデリングの指示と、ソルバーライブラリを読み込んだ永続的なIPythonカーネルを受け取り、プログラムを書いて本物のソルバーで実行し、答えを検証してから最終プログラムを提出します。手元には解と、それを生んだコードの両方が残ります。

バージョン4はPySAT、MaxSAT、Z3、CPMpy、Clingo、DIDPの6つのバックエンドに対応します。MITライセンスでPythonで書かれ、GitHubのスターは約187、最後のコミットは2026年10月13日です。以前のv3の設計はSAT 2025の論文に記述され、専用のブランチに残されています。

MCP Solverのインストール方法

git clone https://github.com/szeider/mcp-solver.git && cd mcp-solver && uv venv && uv pip install -e ".[agent]"

MCP Solverは使う価値があるか?

MCP Solverは、言語モデルが組合せ問題でよく犯す失敗、つまり制約に反する答えを当て推量で出すことを正します。ここではモデルは直接答えません。PySAT、MaxSAT、Z3、CPMpy、Clingo、そして経路やスケジューリング向けのDIDPという6つのバックエンドのいずれかに向けたソルバープログラムを書き、実行し、結果を検証してから初めてsubmit_codeを呼びます。出てくるのは再実行も監査もできるプログラムで、勤務表や構成の妥当性を説明しなければならない人にとっては答えそのものより価値があります。

裏付けはほとんどのMCPサーバーより充実しています。Claude Opusをホストにした場合、READMEはCP-Bench(101)とASP-Bench(128)で厳格な検証のもと229件中229件を正しく解いたと報告し、同梱の30個のテスト問題はすべてCLI経由のGPT-5.6 Terraで解けています。ただし著者自身が作ったベンチマークでの著者自身の実行結果なので、独立した結果ではなく強い兆候として読むべきです。バージョン4は書き直しでもあり、細かなモデル編集ツールとMiniZincを備えたv3のサーバーはなくなり、カーネルと6つのツールに置き換わりました。

注意点:インストールと安全性の両方に気を配る必要があります。第三者がmcp-solverという名前でv2.0.0の古いコードを保持しているため、v4はPyPIになく、uvx mcp-solverでは別物が入ります。名前の移管申請が決着するまではクローンしてソースからインストールするしかありません。INSTALLガイドによれば、v4はmacOSでしか検証されていません。さらに土台のカーネルは同じ著者のagentic-python-coderのもので、モデルが書いたコードを作業ディレクトリで自動的に実行します。その安全上の注意書きは、信頼できない入力にはVMかコンテナーを使うよう勧めています。

結論:現実のスケジューリング、割り当て、検証の問題を抱える計画担当者、研究者、エンジニアにとって、これはもっともらしい答えとソルバーが証明した答えの差です。クローンとコンテナーの手間をかける価値があります。パッケージングは追いつくでしょうし、手法はすでに確かです。

真価を発揮する場面

  • 定員40床の介護施設の運営責任者

    シフト規則、休息時間、希望を満たす勤務表を作る

    Claudeに規則を説明すると、CPMpyかMaxSATを選び、必須規則と重み付きの希望をコード化し、ソルバーを実行してプログラムを提出します。翌月はプロンプトし直す代わりに、保存したプログラムを新しい勤務可能日で再実行します。

  • ファームウェアエンジニア

    ビット操作ルーチンがすべての入力で仕様どおりに動くことを証明する

    エージェントが両方の版をZ3でコード化し、反例を探します。unsatなら証明で、モデルが見つかればそれが失敗する入力です。カーネルが生成コードを実行するので、コンテナー内で動かします。

  • 大学の教務担当者

    30科目を重複なく教室に割り当てる

    ClingoかCPMpyのバックエンドで教室、定員、教員の衝突をコード化すると、提出されたプログラムがそのまま次の学期の時間割生成器になります。ホストのモデルのトークン代以外は無料です。

導入前に確認すること

導入
リポジトリをクローンし、uv venv、uv pip install -e ".[agent]"を実行してから、クライアントをuv run --project <パス> --extra agent mcp-solver-serveに向けます。PyPIの名前移管が終わるまでuvxの設定は使わないでください。Python 3.13か3.14とuvが必要です。
連携
バックエンドはpython-sat、RC2 MaxSAT、z3-solver、cpmpy(ortools付き)、clingo、didppy。ツールはselect_backend、python_exec、python_reset、python_status、python_interrupt、submit_codeで、ガイドとテンプレートのリソースもあります。CLIとベンチマーク用ハーネスはOpenRouter経由で動きます。
データとプライバシー
stdioでローカルに動作します。問題の記述と生成コードはホストのモデル提供元に送られます。ソルバープログラムは作業ディレクトリのローカルIPythonカーネルでサンドボックスなしに実行され、任意の統計は指定したJSONLファイルに書き込まれます。
大規模利用時のコスト
MITで無料です。費用はホストのモデルのトークン代で、CLIの実行ではOpenRouterの利用料が自分のキーに請求されます。
制限
CLIの各実行は既定でエージェントの30ステップで止まります。ortoolsとpython-satが対応パッケージを出していないため、Python 3.15にはまだ対応しません。暴走した求解はpython_interruptで止められます。

良い点

  • SATから動的計画法まで6つのソルバーバックエンド
  • 検証済みで再実行できるソルバープログラムが残る
  • 著者の実行でベンチマーク229件中229件を解決
  • APIキー不要で、ホストのモデルが解く

気になる点

  • PyPIから入れられず、その名前には古いv2.0.0のコード
  • v4は今のところmacOSでのみ検証
  • カーネルはモデルが書いたコードをサンドボックスなしで実行
  • Python 3.13か3.14とuvが必要

おすすめの人

スケジューリング、割り当て、構成、検証の問題を本物のソルバーでエージェントに解かせ、プログラムも手元に残したいオペレーションズリサーチの専門家、エンジニア、アナリスト。

MCP Solverの代替

MCP Solver:よくある質問

MCP Solverは使う価値があるか?
モデルが頭の中で解くべきではないスケジューリングやパズルの問題に対する正しい発想ですが、今のところはリポジトリからしか入れられないことと、モデルが書いたコードを何でも実行するカーネルが足かせです。 評価は5点満点中3.9点です。
MCP Solverの料金は?
無料のオープンソース(MIT)。サーバーにAPIキーは不要で、任意のCLIは自分のOpenRouterキーを使います。
MCP Solverの欠点は?
PyPIから入れられず、その名前には古いv2.0.0のコード; v4は今のところmacOSでのみ検証; カーネルはモデルが書いたコードをサンドボックスなしで実行; Python 3.13か3.14とuvが必要.
MCP Solverは誰に向いているか?
スケジューリング、割り当て、構成、検証の問題を本物のソルバーでエージェントに解かせ、プログラムも手元に残したいオペレーションズリサーチの専門家、エンジニア、アナリスト。
チームや本番環境でMCP Solverを使うと費用はいくらか?
MITで無料です。費用はホストのモデルのトークン代で、CLIの実行ではOpenRouterの利用料が自分のキーに請求されます。
MCP Solverは企業データを扱っても安全か?
stdioでローカルに動作します。問題の記述と生成コードはホストのモデル提供元に送られます。ソルバープログラムは作業ディレクトリのローカルIPythonカーネルでサンドボックスなしに実行され、任意の統計は指定したJSONLファイルに書き込まれます。
MCP Solverの代わりになるものは?
当サイトでレビューした中で最も近い代替はLean LSP MCP 、 Sequential Thinking (reference server)です。

回答確認日:2026年11月7日