mcp-solver

MCP-решатель

Сервер протокола контекста модели (MCP), который предоставляет возможности SAT, SMT и решения ограничений для больших языковых моделей.

Обзор

MCP Solver объединяет SAT, SMT и решение задач с ограничениями с LLM через протокол контекста модели, позволяя моделям ИИ интерактивно создавать, редактировать и решать:

• Модели ограничений в MiniZinc
• Модели SAT в PySAT
• Формулы SMT в Z3 Python

Подробное описание архитектуры системы MCP Solver и теоретических основ см. в сопутствующей исследовательской статье: Стефан Сейдер, «MCP-Solver: Интеграция языковых моделей с системами программирования в ограничениях» , arXiv:2501.00539, 2024.

Доступные инструменты

Далее item относится к некоторой части кода (MinZinc/Pysat/Z3), а model — к кодировке.

Системные требования

• Python и менеджер проектов uv
• Питон 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 Solver предоставляет три различных режима работы, каждый из которых интегрируется с различным бэкэндом решения ограничений. Каждый режим требует определенных зависимостей и предлагает уникальные возможности для решения различных классов проблем.

Режим 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, exact_k)
• Поддержка решения булевых ограничений

Зависимости : Требуется пакет python-sat ( uv pip install -e ".[pysat]" )

Конфигурация : для запуска в режиме PySAT используйте:

Режим Z3

Режим Z3 обеспечивает доступ к возможностям решения Z3 SMT (теории выполнимости по модулю) со следующими функциями:

• Богатая система типов: логические значения, целые числа, действительные числа, битовые векторы, массивы
• Решение ограничений с помощью квантификаторов
• Возможности оптимизации
• Библиотека шаблонов для общих шаблонов моделирования

Зависимости : Требуется пакет z3-solver ( uv pip install -e ".[z3]" )

Конфигурация : Для работы в режиме Z3 используйте:

Тестовый клиент MCP

MCP Solver включает в себя клиент MCP для целей разработки, экспериментирования и диагностики, основанный на фреймворке агента ReAct . Этот клиент служит посредником между LLM и сервером MCP, облегчая перевод формулировок задач на естественном языке в формальные решения программирования ограничений.

Установка

Клиенту требуется ключ API от поставщика LLM. Для Anthropic (LLM по умолчанию — Claude Sonnet 3.7) установите переменную среды ANTHROPIC_API_KEY . Ее можно установить в вашей среде или включить в файл .env в корне проекта.

Клиент также поддерживает других поставщиков LLM, включая OpenAI, Google (Gemini), OpenRouter и даже локальные модели через LM Studio. Вы можете указать, какую модель использовать, с помощью флага командной строки --mc . Подробности о форматах кода модели см. в INSTALL.md.

Использование

Клиент предоставляет специализированные команды для каждого решателя:

Примеры

Пример 1: Проблема литья (MiniZinc)

Это основано на примере Джорджа Джонсона (NYT, 13 июля 1999 г.).

Пользователь

Предположим, что театральный режиссер чувствует себя обязанным взять на роль либо свою инженю, актрису Альварес, либо своего племянника, актера Коэна, в постановке. Но мисс Альварес не будет играть в пьесе с мистером Коэном (ее бывшим любовником), и она требует, чтобы в актерский состав вошла ее новая страсть, актер Дэвенпорт. Продюсер, которому нужно отплатить за свои услуги, настаивает, чтобы актер Браниславский сыграл роль. Но мистер Браниславский не будет играть ни в одной пьесе с мисс Альварес или мистером Дэвенпортом. Может ли режиссер взять на роль актера?

Система: 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 ферзей на шахматной доске nxn. Попробуйте 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=10, 20, 30 и 40 путем изменения значения n)

Сравнение времени решения: n=10: 0,001sn=20: 0,005sn=30: 0,040sn=40: 0,043с

Решения существуют для всех протестированных размеров плат. Временная сложность увеличивается нелинейно, но остается управляемой до n=40.

Пример 3: Задача коммивояжера (MiniZinc)

Пользователь

Продавщица из Вены должна спланировать предстоящий тур по Австрии, посетив каждую столицу провинции по одному разу. Помогите найти кратчайший маршрут. Расстояния в км: 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}

Оптимальный маршрут: Вена → Санкт-Пёльтен → Линц → Зальцбург → Брегенц → Инсбрук → Клагенфурт → Грац → Айзенштадт → Вена общим расстоянием 1564 км.

Обратная связь

Вы можете оставить отзыв автору через эту форму .

Отказ от ответственности

Этот MCP Solver находится на стадии прототипа и должен использоваться с осторожностью. Пользователям рекомендуется экспериментировать, но любое использование в критических средах осуществляется на их страх и риск.

Лицензия

Данный проект лицензирован по лицензии MIT — подробности см. в файле LICENSE .