内容
# 求解器-MCP
`solver-mcp` 是一个本地的 MCP 服务器，为 AI 代理提供实时 Timefold 求解器后端，用于解决分配问题。代理编写具有通用实体、值、属性和约束基元的声明式 JSON 规范；服务器验证它，解决它，并返回具有得分明细的分配。LLM 编写声明式规范，而不是代码；Timefold 计算答案；不会出现幻觉。
由 Timefold 求解器社区（Apache 2.0）提供支持的非官方项目。
## 快速入门
前提条件：
- JDK 21
- 可以启动 stdio 服务器的本地 MCP 客户端
构建可运行的 fat jar：
```bash
./gradlew build
```
运行服务器：
```bash
java -jar build/libs/solver-mcp-1.0.0-all.jar
```
对于 MCP 客户端，请使用上面的 jar 命令。不要通过 `./gradlew run` 启动 MCP 服务器；Gradle 将进度输出写入 stdout，而 stdio MCP 需要 stdout 仅包含协议帧。
或者构建和运行 Docker 镜像：
```bash
docker build -t solver-mcp:1.0.0 .
docker run -i --rm solver-mcp:1.0.0
```
Docker MCP 客户端必须使用 `-i` 保持 stdin 打开；服务器通过 stdio 使用 MCP 进行通信。
## Claude 代码
从此存储库：
```bash
claude mcp add solver-mcp -- java -jar /absolute/path/to/solver-mcp/build/libs/solver-mcp-1.0.0-all.jar
```
Docker 替代方案：
```bash
claude mcp add solver-mcp -- docker run -i --rm solver-mcp:1.0.0
```
然后启动 Claude Code 并要求它使用 `solver-mcp` 来验证和解决规范。
## Claude 桌面版
在您的 Claude Desktop MCP 配置中添加一个 stdio 服务器条目：
```json
{
"mcpServers": {
"solver-mcp": {
"type": "stdio",
"command": "java",
"args": [
"-jar",
"/absolute/path/to/solver-mcp/build/libs/solver-mcp-1.0.0-all.jar"
]
}
}
}
```
编辑配置后重启 Claude Desktop。
Docker 替代方案：
```json
{
"mcpServers": {
"solver-mcp": {
"type": "stdio",
"command": "docker",
"args": ["run", "-i", "--rm", "solver-mcp:1.0.0"]
}
}
}
```
## 工具
| 工具 | 用途 |
| --- | --- |
| `modeling_guide` | 返回 DSL 指南、表达式语法、基元示例、完整示例和修复工作流。 |
| `validate_spec` | 检查 JSON 形状、表达式解析、属性引用、基元兼容性和大小警告。 |
| `solve` | 使用有界 Timefold 运行解决 ASSIGNMENT 规范，并返回最佳分配。 |
| `explain_solution` | 重建提供的分配，并返回确定性的每个约束总计和最佳匹配。 |
| `diagnose_infeasible` | 列出损坏的硬约束，并简要地一次放松一个硬约束来重新求解。 |
## 规范
v1.0 架构在 [spec-schema.json](spec-schema.json) 中发布。当前原型是 `ASSIGNMENT`；每个实体从值列表中获得一个值。
```json
{
"name": "考试时间表",
"archetype": "ASSIGNMENT",
"entities": [
{ "id": "examA", "attrs": { "students": 120, "teacher": "kim" } }
],
"values": [
{ "id": "slot1_roomX", "attrs": { "day": 1, "slot": 1, "capacity": 150 } }
],
"constraints": [
{
"id": "capacity",
"type": "require",
"when": "entity.attrs.students <= value.attrs.capacity",
"level": "HARD"
}
]
}
```
约束权重使用规范架构：
```json
{ "level": "HARD" }
```
```json
{ "level": "SOFT", "weight": 3 }
```
## 表达式语言
表达式由小型手动滚动的解析器解析，并针对通用模型求值。它们支持标识符 `entity`、`value`、`a`、`b` 和 `group`；路径如 `entity.attrs.load`、`value.id` 和 `a.value.attrs.day`；数字、字符串、布尔值和空字面量；算术、比较、`&&`、`||`、`!` 和括号。
没有方法调用、循环、反射或任意代码执行。
## 基元参考
| 基元 | 级别 | 必要字段 | 含义 |
| --- | --- | --- | --- |
| `require` | HARD 或 SOFT | `when` | 惩罚每个 `when` 为假的分配。 |
| `forbid` | HARD 或 SOFT | `when` | 惩罚每个 `when` 为真的分配。 |
| `all_different` | HARD 或 SOFT | `expr` | 惩罚具有相同 `expr` 值的实体对。 |
| `pair_rule` | HARD 或 SOFT | `forbid` 或 `penalizeIf` | 对可选 `pairFilter` 选择的实体对进行惩罚，当对条件为真时。 |
| `group_count` | HARD 或 SOFT | `groupBy`、`min` 或 `max` | 限制每个组的已分配实体数量。 |
| `group_sum` | HARD 或 SOFT | `groupBy`、`sumExpr`、`min` 或 `max` | 限制每个组的数字总和。 |
| `cardinality` | HARD 或 SOFT | `min` 或 `max` | 限制每个值分配的实体数量，可选地由 `valueFilter` 限制。 |
| `balance` | SOFT | `groupBy` | 对每个组的 `(组计数)^2` 进行惩罚。 |
| `objective` | SOFT | `expr` | `minimize` 惩罚总和；`maximize` 奖励总和。 |
## 示例
存储库中包含五个完整的规范：
- [N-queens 8](examples/n-queens-8.json)
- [图着色](examples/graph-coloring.json)
- [具有容量的任务到机器](examples/task-machine-capacity.json)
- [具有不兼容对的婚礼座位安排](examples/wedding-seating.json)
- [考试时间表](examples/exam-timetabling.json)
参见 [examples/demo.md](examples/demo.md) 以获取预期代理循环的记录：
```text
validate_spec -> solve -> explain_solution -> 如果硬不可行则修复规范
```
## 架构
`solver-mcp` 故意避免使用诸如员工、班次、房间或工作等领域类。Timefold 模型具有通用 `Element` 事实、通用规划实体和约束规范项存储在规划解决方案中作为问题事实。
`ConstraintProvider` 始终包含用于每个基元和得分级别的流。每个流从 `ConstraintSpecItem` 开始，按基元和级别过滤，连接通用实体或值，并评估缓存的表达式 AST。这使求解器保持数据驱动，无需静态注册或生成的代码。
`solve` 在请求的 timeLimit 内返回最佳解决方案。`explain_solution` 从 `{ spec, assignments }` 重建解决方案，并生成确定性的约束总计和最佳匹配，以便跟踪每个得分贡献。
## 限制
- v1.0 仅支持 ASSIGNMENT。SEQUENCE 计划在未来版本中提供。
- Timefold 在 timeLimit 内返回最佳解决方案，除非另行配置；该项目不证明最优性。
- 表达式语言故意设计得小且有界。
- 通用约束流灵活，但不是大型生产实例的手动调优域求解器的替代品。
- `validate_spec` 在超过 500 个实体或 50,000 个估计对时发出警告。
## 路线图
- SEQUENCE 原型，带有 list-variable shadow 变量：`@IndexShadowVariable`、`@PreviousElementShadowVariable` 和 `@CascadingUpdateShadowVariable`。
- 用于最优性证明的 CP-SAT 后端，其中 DSL 可以精确编译。
- 更多基元约束和更强的静态类型检查。
- 打包的桌面扩展分发。
## 开发
运行完整的套件：
```bash
./gradlew build
```
构建容器：
```bash
docker build -t solver-mcp:1.0.0 .
```
测试涵盖表达式解析和求值、每个分配基元的 Timefold `ConstraintVerifier`、端到端的 N-queens 和图着色、不可行诊断、验证错误、stdout 纪律和所有检查的示例。
## 许可证
Apache License 2.0。参见 [LICENSE](LICENSE)。
