mcp-solver

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 はエンコーディングを指します。

システム要件

• 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 を参照してください。

クイックスタート:

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

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

MiniZincモード

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

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

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

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

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 モードで実行するには、次を使用します。

Z3モード

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

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

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

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

MCP テストクライアント

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

インストール

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

使用法

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

例

例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ファイルを参照してください。