mcp-solver

Solucionador MCP

Un servidor de Protocolo de Contexto de Modelo (MCP) que expone capacidades de resolución de restricciones, SAT y SMT a modelos de lenguaje grandes.

Descripción general

El solucionador MCP integra SAT, SMT y resolución de restricciones con LLM a través del protocolo de contexto de modelo, lo que permite que los modelos de IA creen, editen y resuelvan de forma interactiva:

• Modelos de restricciones en MiniZinc
• Modelos SAT en PySAT
• Fórmulas SMT en Python Z3

Para obtener una descripción detallada de la arquitectura del sistema y los fundamentos teóricos del solucionador MCP , consulte el artículo de investigación adjunto: Stefan Szeider, "MCP-Solver: Integrating Language Models with Constraint Programming Systems" , arXiv:2501.00539, 2024.

Herramientas disponibles

A continuación, el elemento se refiere a alguna parte del código (MinZinc/Pysat/Z3) y el modelo a la codificación.

Requisitos del sistema

• Python y gestor de proyectos uv
• Python 3.11+
• Requisitos específicos del modo: MiniZinc, PySAT, Python Z3 (los paquetes necesarios se instalan mediante pip)
• Sistemas operativos: macOS, Windows, Linux (con adaptaciones adecuadas)

Instalación

MCP Solver requiere Python 3.11+, el administrador de paquetes uv y dependencias específicas del solucionador (MiniZinc, Z3 o PySAT).

Para obtener instrucciones de instalación detalladas para Windows, macOS y Linux, consulte INSTALL.md .

Inicio rápido:

Modos disponibles / Solución de backends

El solucionador MCP ofrece tres modos operativos distintos, cada uno de los cuales se integra con un backend de resolución de restricciones distinto. Cada modo requiere dependencias específicas y ofrece capacidades únicas para abordar diferentes tipos de problemas.

Modo MiniZinc

El modo MiniZinc proporciona integración con el lenguaje de modelado de restricciones MiniZinc con las siguientes características:

• Expresión de restricción enriquecida con restricciones globales
• Integración con el solucionador de restricciones Chuffed
• Capacidades de optimización
• Acceso a los valores de la solución mediante get_solution

Dependencias : Requiere el paquete minizinc ( uv pip install -e ".[mzn]" )

Configuración : Para ejecutar en modo MiniZinc, utilice:

Modo PySAT

El modo PySAT permite la interacción con el kit de herramientas de resolución de problemas SAT de Python con las siguientes características:

• Modelado de restricciones proposicionales mediante CNF (Forma Normal Conjuntiva)
• Acceso a varios solucionadores SAT (Glucose3, Glucose4, Lingeling, etc.)
• Restricciones de cardinalidad (como máximo k, al menos k, exactamente k)
• Soporte para la resolución de restricciones booleanas

Dependencias : Requiere el paquete python-sat ( uv pip install -e ".[pysat]" )

Configuración : Para ejecutar en modo PySAT, utilice:

Modo Z3

El modo Z3 proporciona acceso a las capacidades de resolución de Z3 SMT (teorías de módulo de satisfacción) con las siguientes características:

• Sistema de tipos enriquecido: booleanos, enteros, reales, vectores de bits, matrices
• Resolución de restricciones con cuantificadores
• Capacidades de optimización
• Biblioteca de plantillas para patrones de modelado comunes

Dependencias : Requiere el paquete z3-solver ( uv pip install -e ".[z3]" )

Configuración : Para ejecutar en modo Z3, utilice:

Cliente de prueba MCP

El solucionador MCP incluye un cliente MCP para fines de desarrollo, experimentación y diagnóstico, basado en el framework del agente ReAct . Este cliente actúa como intermediario entre un LLM y el servidor MCP, facilitando la traducción de enunciados de problemas en lenguaje natural a soluciones formales de programación con restricciones.

Instalación

El cliente requiere una clave API de un proveedor de LLM. Para Anthropic (el LLM predeterminado es Claude Sonnet 3.7), configure la variable de entorno ANTHROPIC_API_KEY . Puede configurarla en su entorno o incluirla en un archivo .env en la raíz del proyecto.

Uso

El cliente proporciona comandos especializados para cada solucionador backend:

Ejemplos

Ejemplo 1: Problema de fundición (MiniZinc)

Esto se basa en un ejemplo de George Johnson (NYT, 13 de julio de 1999).

Usuario

Supongamos que un director teatral se siente obligado a incluir en el reparto a su ingenua, la actriz Álvarez, o a su sobrino, el actor Cohen, en una producción. Pero la señorita Álvarez no quiere actuar con el señor Cohen (su antiguo amante) y exige que el reparto incluya a su nuevo amor, el actor Davenport. El productor, con sus propios favores que devolver, insiste en que el actor Branislavsky participe. Pero el señor Branislavsky no quiere actuar con la señorita Álvarez ni con el señor Davenport. ¿Puede el director incluir en el reparto a la obra?

Sistema: clear_model

Model cleared

Sistema: add_item (múltiple)

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;

Sistema: solve_model

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

La solución (elegir a Cohen y Branislavsky, pero no a Alvarez o Davenport) satisface todas las restricciones.

Ejemplo 2: Problema de N-Reinas (MiniZinc)

Usuario

Comprueba si puedes colocar n reinas en un tablero de ajedrez de nxn. Prueba con n = 10, 20, 30, 40 y compara los tiempos de resolución.

Sistema: clear_model

Model cleared

Sistema: add_item (múltiple)

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;

Sistema: solve_model (con n=10, 20, 30 y 40 cambiando el valor de n)

Comparación de tiempos de resolución: n=10: 0,001 s n=20: 0,005 s n=30: 0,040 s n=40: 0,043 s

Existen soluciones para todos los tamaños de placa probados. La complejidad temporal aumenta de forma no lineal, pero se mantiene manejable hasta n=40.

Ejemplo 3: Problema del viajante (MiniZinc)

Usuario

Una vendedora residente en Viena necesita planificar su próximo viaje por Austria, visitando cada capital de provincia una vez. Ayúdenme a encontrar la ruta más corta. Distancias en km: 1=Viena, 2=St. Pölten, 3=Eisenstadt, 4=Linz, 5=Graz, 6=Klagenfurt, 7=Salzburgo, 8=Innsbruck, 9=Bregenz.

[Tabla de matriz de distancias proporcionada en el mensaje del usuario]

Sistema: add_item (múltiple)

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;

Sistema: solve_model

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

Ruta óptima: Viena → St. Pölten → Linz → Salzburgo → Bregenz → Innsbruck → Klagenfurt → Graz → Eisenstadt → Viena con una distancia total de 1.564 km.

Comentario

Puede proporcionar comentarios al autor a través de este formulario .

Descargo de responsabilidad

Este solucionador MCP se encuentra en fase de prototipo y debe utilizarse con precaución. Se anima a los usuarios a experimentar, pero cualquier uso en entornos críticos es bajo su propia responsabilidad.

Licencia

Este proyecto está licenciado bajo la licencia MIT: consulte el archivo de LICENCIA para obtener más detalles.