mcpソルバー

MCPソルバー

SAT、SMT、制約解決機能を大規模言語モデルに公開するモデルコンテキストプロトコル (MCP) サーバー。

概要

MCP ソルバーは、モデルコンテキストプロトコルを通じて SAT、SMT、制約解決を LLM と統合し、AI モデルが対話的に作成、編集、解決できるようにします。

MiniZincの制約モデル
PySATのSATモデル
Z3 PythonのSMT式

MCP ソルバーのシステムアーキテクチャと理論的基礎の詳細な説明については、付随する研究論文「Stefan Szeider、「MCP-Solver: Integrating Language Models with Constraint Programming Systems」、arXiv:2501.00539、2024 を参照してください。

利用可能なツール

以下では、 item は(MinZinc/Pysat/Z3) コードの一部を指し、 model はエンコーディングを指します。

ツール名	説明
`clear_model`	モデルからすべてのアイテムを削除します
`add_item`	特定のインデックスに新しいアイテムを追加する
`delete_item`	インデックスのアイテムを削除
`replace_item`	インデックスの項目を置換
`get_model`	番号付きアイテムで現在のモデルコンテンツを取得する
`solve_model`	モデルを解く（タイムアウトパラメータ付き）

システム要件

PythonとプロジェクトマネージャーUV
Python 3.11以上
モード固有の要件: MiniZinc、PySAT、Python Z3 (必要なパッケージは pip 経由でインストールされます)
オペレーティングシステム: macOS、Windows、Linux（適切な適応が必要）

インストール

MCP Solver には、Python 3.11 以上、 uvパッケージマネージャー、およびソルバー固有の依存関係 (MiniZinc、Z3、または PySAT) が必要です。

Windows、macOS、Linux の詳細なインストール手順については、 INSTALL.md を参照してください。

クイックスタート:

git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv
source .venv/bin/activate
uv pip install -e ".[all]"  # Install all solvers

利用可能なモード / バックエンドの解決

MCPソルバーは3つの異なる動作モードを提供し、それぞれ異なる制約解決バックエンドと統合されます。各モードは特定の依存関係を必要とし、異なる種類の問題に対処するための独自の機能を提供します。

MiniZincモード

MiniZinc モードは、次の機能を備えた MiniZinc 制約モデリング言語との統合を提供します。

グローバル制約を備えた豊富な制約式
Chuffed制約ソルバーとの統合
最適化機能
get_solution経由でソリューション値にアクセスする

依存関係: minizincパッケージが必要です ( uv pip install -e ".[mzn]" )

設定: MiniZinc モードで実行するには、次を使用します。

mcp-solver-mzn

PySATモード

PySAT モードでは、次の機能を使用して Python SAT 解決ツールキットと対話できます。

CNF（連言正規形）を使用した命題制約モデリング
さまざまな SAT ソルバー (Glucose3、Glucose4、Lingeling など) へのアクセス
カーディナリティ制約 (at_most_k、at_least_k、exactly_k)
ブール制約解決のサポート

依存関係: python-satパッケージが必要です ( uv pip install -e ".[pysat]" )

設定: PySAT モードで実行するには、次を使用します。

mcp-solver-pysat

Z3モード

Z3 モードでは、次の機能を備えた Z3 SMT (Satisfiability Modulo Theories) 解決機能にアクセスできます。

豊富な型システム: ブール値、整数、実数、ビットベクトル、配列
量指定子による制約解決
最適化機能
一般的なモデリングパターンのテンプレートライブラリ

依存関係: z3-solverパッケージが必要です ( uv pip install -e ".[z3]" )

設定: Z3 モードで実行するには、次を使用します。

mcp-solver-z3

MCP テストクライアント

MCPソルバーには、 ReActエージェントフレームワークをベースにした、開発、実験、診断用のMCPクライアントが含まれています。このクライアントはLLMとMCPサーバー間の仲介役として機能し、自然言語による問題記述を形式制約プログラミングによるソリューションに変換します。

インストール

# Install client dependencies
uv pip install -e ".[client]"

# Verify client installation and configuration
uv run test-setup-client

クライアントはLLMプロバイダからのAPIキーを必要とします。Anthropic（デフォルトのLLMはClaude Sonnet 3.7）の場合は、 ANTHROPIC_API_KEY環境変数を設定してください。この環境変数は、ご自身の環境で設定するか、プロジェクトルートの.envファイルに含めることができます。

使用法

クライアントは、各ソルバーバックエンドに特化したコマンドを提供します。

# MiniZinc mode
uv run run-test mzn --problem <path/to/problem.md>

# PySAT mode
uv run run-test pysat --problem <path/to/problem.md>

# Z3 mode
uv run run-test z3 --problem <path/to/problem.md>

例

例1：鋳造問題（MiniZinc）

これは、George Johnson (NYT、1999 年 7 月 13 日) の例に基づいています。

ユーザー

ある演出家が、純真な女優アルバレスか、甥の俳優コーエンのどちらかを作品に出演させる義務があるとします。しかし、アルバレスさんはコーエン氏（彼女の元恋人）との共演を断り、新たな恋人である俳優ダベンポートをキャストに加えるよう要求します。プロデューサーは、自身の好意に応えたい一心で、俳優ブラニスラフスキーに出演を強く求めます。しかし、ブラニスラフスキー氏はアルバレスさんやダベンポート氏との共演は断ります。演出家は、この劇に出演させることができるでしょうか？

システム: clear_model

Model cleared

システム: add_item (複数)

var bool: alvarez; var bool: cohen; var bool: branislavsky; var bool: davenport; constraint alvarez \/ cohen; % Must cast either Alvarez or Cohen constraint not (alvarez /\ cohen); % Alvarez won't work with Cohen constraint alvarez -> davenport; % If Alvarez is cast, Davenport must be cast constraint branislavsky; % Branislavsky must be cast constraint not (branislavsky /\ alvarez); % Branislavsky won't work with Alvarez constraint not (branislavsky /\ davenport); % Branislavsky won't work with Davenport solve satisfy;

システム: solve_model

{'status': 'SAT', 'solution': Solution(alvarez=False, cohen=True, branislavsky=True, davenport=False, _checker=''), 'solve_time': 0.0}

解決策 (コーエンとブラニスラフスキーをキャストし、アルバレスやダベンポートはキャストしない) はすべての制約を満たします。

例2: Nクイーン問題 (MiniZinc)

ユーザー

n×nのチェス盤にn個のクイーンを置けるかどうか試してみましょう。n=10、20、30、40で試し、解く時間を比較してみましょう。

システム: clear_model

Model cleared

システム: add_item (複数)

int: n = 10; array[1..n] of var 1..n: queens; constraint alldifferent(queens); constraint alldifferent([queens[i] + i | i in 1..n]); constraint alldifferent([queens[i] - i | i in 1..n]); solve satisfy;

システム: solve_model (nの値を変更してn=10、20、30、40で実行)

解決時間の比較: n=10: 0.001sn=20: 0.005sn=30: 0.040sn=40: 0.043s

テストされたすべてのボードサイズに対してソリューションが存在します。時間計算量は非線形に増加しますが、n=40までは管理可能な範囲に留まります。

例3: 巡回セールスマン問題 (MiniZinc)

ユーザー

ウィーンに拠点を置く営業担当者が、オーストリア全土を巡るツアーを計画し、各州都を一度ずつ訪問したいと考えています。最短ルートを見つけるお手伝いをお願いします。距離（km）：1=ウィーン、2=ザンクト・ペルテン、3=アイゼンシュタット、4=リンツ、5=グラーツ、6=クラーゲンフルト、7=ザルツブルク、8=インスブルック、9=ブレゲンツ
[ユーザーメッセージに距離マトリックス表が提供されています]

システム: add_item (複数)

include "globals.mzn"; int: n = 9; array[1..n,1..n] of int: dist = [|0,65,60,184,195,319,299,478,631|65,0,125,119,130,254,234,413,566|60,125,0,184,157,281,261,440,593|184,119,184,0,208,252,136,315,468|195,130,157,208,0,136,280,459,629|319,254,281,252,136,0,217,391,566|299,234,261,136,280,217,0,188,343|478,413,440,315,459,391,188,0,157|631,566,593,468,629,566,343,157,0|]; array[1..n] of var 1..n: succ; var int: total_dist = sum(i in 1..n)(dist[i,succ[i]]); constraint circuit(succ); solve minimize total_dist;

システム: solve_model

{'status': 'SAT', 'solution': Solution(objective=1564, succ=[2, 4, 1, 7, 3, 5, 9, 6, 8], _checker=''), 'solve_time': 0.002}

最適ルート: ウィーン→ザンクト・ペルテン→リンツ→ザルツブルク→ブレゲンツ→インスブルック→クラーゲンフルト→グラーツ→アイゼンシュタット→ウィーン、総距離は1,564km。

フィードバック

このフォームから著者にフィードバックを送信できます。

免責事項

このMCPソルバーはプロトタイプ段階であり、慎重に使用する必要があります。ユーザーは実験することをお勧めしますが、クリティカルな環境での使用は自己責任となります。

ライセンス

このプロジェクトは MIT ライセンスに基づいてライセンスされています - 詳細についてはLICENSEファイルを参照してください。

mcp-solver