Usolver

🚀 USolver

USolver 是一個模型上下文協議（Model Context Protocol）服務器，它提供瞭解決組合規劃、凸規劃、整數規劃和非線性優化問題的工具。該服務器提供了與以下求解器的接口：

• highs - 線性和混合整數規劃求解器
• ortools - 組合優化求解器
• cvxpy - 凸優化求解器
• z3 - 布爾、整數、實數和字符串上的 SMT 求解器

🚀 快速開始

要安裝 USolver，運行 install.py 腳本。這將為 Claude Desktop 和/或 Cursor 安裝 MPC 服務器。

uv run install.py

然後打開 Claude 或 Cursor，你應該能在工具列表中看到 MCP 工具 usolver。

✨ 主要特性

• 提供多種優化問題的求解工具，涵蓋組合規劃、凸規劃、整數規劃和非線性優化等領域。
• 集成了多個知名求解器，如 highs、ortools、cvxpy 和 z3。
• 包含豐富的使用示例，涉及化學工程、物流、投資組合理論等多個領域。

💻 使用示例

基礎用法

以下是一些不同類型的使用示例：

邏輯謎題

你和一個朋友路過一臺標準的投幣式自動售貨機，你決定買一根糖果棒。價格是 0.95 美元，但你翻遍口袋後發現只有一美元，而機器只接受硬幣。你轉向你的朋友，有了以下對話：

你：嘿，你有一美元的零錢嗎？
朋友：讓我看看。我有 6 枚美國硬幣，雖然它們加起來是 1.15 美元，但我沒法湊出一美元的零錢。
你：哈？那你能湊出半美元的零錢嗎？
朋友：不能。
你：那 25 美分呢？
朋友：不行，在你問之前我就告訴你，我也湊不出 10 美分或 5 美分的零錢。
你：真的嗎？而且這 6 枚硬幣都是美國政府目前正在發行的硬幣？
朋友：是的。
你：那你能把你的硬幣放進自動售貨機給我買根糖果棒，然後我再還給你錢嗎？
朋友：對不起，我很想幫你，但我現有的硬幣做不到。

你的朋友拿著哪些硬幣呢？

可以將這個問題輸入到 usolver 中，它會生成一個約束系統：

設 $C$ 是 6 個未知硬幣值的集合，從 $c_1$ 到 $c_6$，每個 $c_i$ 都必須是表示美分的正整數。 $$ C = {c_1, c_2, c_3, c_4, c_5, c_6}, \quad \text{其中每個 } c_i \in \mathbb{Z}^+ $$ $\mathcal{S}$ 是從 6 枚硬幣中選擇 2 枚或更多硬幣的所有可能組合的集合。 $$ \mathcal{S} = {S \mid S \subseteq C \land |S| \geq 2 } $$ 排除 50 美分硬幣在自動售貨機中的使用。 $$ v(x) = \begin{cases} 0 & \text{如果 } x = 50 \ x & \text{如果 } x \neq 50 \end{cases} $$ 約束 0：6 枚硬幣的總價值為 115 美分。 $$ \sum_{i=1}^{6} c_i = 115 $$ 約束 1：不能湊出一美元的零錢。 $$ \forall S \in \mathcal{S}, \quad \sum_{x \in S} x \neq 100 $$ 約束 2：不能湊出半美元的零錢。 $$ \forall S \in \mathcal{S}, \quad \sum_{x \in S} x \neq 50 $$ 約束 3：不能湊出 25 美分的零錢。 $$ \forall S \in \mathcal{S}, \quad \sum_{x \in S} x \neq 25 $$ 約束 4：不能湊出 10 美分的零錢。 $$ \forall S \in \mathcal{S}, \quad \sum_{x \in S} x \neq 10 $$ 約束 5：不能湊出 5 美分的零錢。 $$ \forall S \in \mathcal{S}, \quad \sum_{x \in S} x \neq 5 $$ 約束 6：如果排除半美元硬幣，不能湊出 95 美分來買糖果棒。 $$ \forall S \in \mathcal{S}, \quad \sum_{x \in S} v(x) \neq 95 $$ 如果將這個問題輸入到求解器中，它會合成上述約束系統，使用 Z3 求解，並返回結果。

你的朋友有：1 枚半美元硬幣、1 枚 25 美分硬幣和 4 枚 10 美分硬幣
總價值為 50 美分 + 25 美分 + 40 美分 = 115 美分 = 1.15 美元 ✓
硬幣總數正好是 6 枚 ✓

現代投資組合理論

一個金融領域的示例：

目標：最大化投資組合的預期回報
約束條件：

債券投資比例不能超過 40%
股票投資比例不能超過 60%
房地產投資比例不能超過 30%
大宗商品投資比例不能超過 20%
所有投資比例必須為非負
總投資比例必須恰好等於 100%
投資組合的總加權風險不能超過 10%

給定數據：

預期回報率：債券 8%、股票 12%、房地產 10%、大宗商品 15%
風險係數：債券 2%、股票 15%、房地產 8%、大宗商品 20%

這個問題會被語言模型編譯成一個可以用 cvxopt 求解的凸優化問題。 $$ \begin{align} \text{最大化} \quad & 0.08x_1 + 0.12x_2 + 0.10x_3 + 0.15x_4 \ \text{約束條件} \quad & x_1 + x_2 + x_3 + x_4 = 1 \ & x_1 \leq 0.4 \ & x_2 \leq 0.6 \ & x_3 \leq 0.3 \ & x_4 \leq 0.2 \ & 0.02x_1 + 0.15x_2 + 0.08x_3 + 0.20x_4 \leq 0.10 \ & x_1, x_2, x_3, x_4 \geq 0 \end{align} $$ 其中：

• $x_1$ = 債券投資比例
• $x_2$ = 股票投資比例
• $x_3$ = 房地產投資比例
• $x_4$ = 大宗商品投資比例

答案是：

債券：30.0%
股票：20.0%
房地產：30.0%（達到最大允許比例）
大宗商品：20.0%（達到最大允許比例）
最大預期回報率：每年 10.8%

Z3 - 化學工程示例

使用 `usolver` 設計一個滿足以下要求的輸水管道：

* 體積流量：0.05 m³/s
* 管道長度：100 m
* 水的密度：1000 kg/m³
* 最大允許壓力降：50 kPa
* 流量連續性：Q = π(D/2)² × v
* 壓力降：ΔP = f(L/D)(ρv²/2)，其中對於湍流 f ≈ 0.02
* 實際限制：0.05 ≤ D ≤ 0.5 m，0.5 ≤ v ≤ 8 m/s
* 壓力約束：ΔP ≤ 50,000 Pa
* 求解：最優管道直徑和流速

線性規劃 - 多線性優化示例

使用 `usolver` 求解以下線性規劃問題：

最小化：12x + 20y
約束條件：6x + 8y ≥ 100
           7x + 12y ≥ 120
           x ≥ 0
           y ∈ [0, 3]

這個問題會被語言模型編譯成一個可以用 Z3 求解的約束滿足問題。 $$ \begin{aligned} \text{最小化} \quad & 12x + 20y \ \text{約束條件} \quad & 6x + 8y \geq 100 \ & 7x + 12y \geq 120 \ & x \geq 0 \ & y \in [0, 3] \end{aligned} $$ 其中：

• $x$ = 第一個決策變量（連續、非負）
• $y$ = 第二個決策變量（連續、有界）

最優解是：

x = 15.0
y = 1.25
目標值 = 205.0

CVXPY - 簡單凸優化問題

使用 `usolver` 求解以下凸優化問題：

最小化：||Ax - b||₂²
約束條件：0 ≤ x ≤ 1
其中 
  A = [1.0, -0.5; 0.5, 2.0; 0.0, 1.0] 
  b = [2.0, 1.0, -1.0]

OR-Tools - 經典員工排班問題

使用 `usolver` 解決以下護士排班問題：

* 在週一、週二、週三這三天內，為 4 名護士（Alice、Bob、Charlie、Diana）安排 3 個班次
* 班次：早班（7 點 - 15 點）、晚班（15 點 - 23 點）、夜班（23 點 - 7 點）
* 每天每個班次必須恰好安排一名護士
* 每名護士每天最多工作一個班次
* 平均分配班次（每名護士在這期間工作 2 - 3 個班次）
* Charlie 不能在週二工作。

鏈式示例

一個鏈式示例，使用 OR-Tools 優化餐廳的餐桌布局，使用 CVXPY 優化員工排班。

使用 `usolver` 分兩部分優化餐廳的佈局和員工排班。使用組合優化優化餐桌布局，使用凸優化優化員工排班。

* 第一部分：優化餐桌布局
  - 混合使用 2 人桌、4 人桌和 6 人桌
  - 最大可用面積：150 m²
  - 空間需求：2 人桌 4 m²、4 人桌 6 m²、6 人桌 9 m²
  - 最多 20 張桌子
  - 最少組合：2 張 2 人桌、3 張 4 人桌、1 張 6 人桌
  - 目標：最大化總座位數

* 第二部分：使用第一部分的座位數優化員工排班
  - 營業時間為 12 小時
  - 每名員工可以服務 20 個座位
  - 每小時至少需要 2 名員工
  - 每小時員工更換人數最多為 2 人
  - 可變需求：為座位數的 40% - 100%
  - 目標：最小化人工成本（每名員工每小時 25 美元）

📦 安裝指南

要安裝 USolver，運行 install.py 腳本。

uv run install.py

🐳 Docker 使用方法

也可以直接從 GitHub Container Registry 運行 MCP 服務器。

docker run -p 8081:8081 ghcr.io/sdiehl/usolver:latest

然後在客戶端添加以下內容：

{
  "mcpServers": {
    "sympy-mcp": {
      "command": "docker",
      "args": [
        "run",
        "-i",
        "-p",
        "8081:8081",
        "--rm",
        "ghcr.io/sdiehl/usolver:latest"
      ]
    }
  }
}

📄 許可證

本項目基於 Apache License 2.0 許可協議發佈。詳細信息請參閱 LICENSE 文件。