MCP Solver
¿Qué es este MCP?
Este servidor MCP (Protocolo de Contexto de Modelo) integra capacidades de SAT, SMT y resolución de restricciones con Modelos de Lenguaje Grandes (LLMs), permitiendo que los modelos de IA creen, editen y resuelvan problemas complejos de restricciones a través de una interfaz estandarizada.
Cómo usar este MCP
El Solucionador MCP opera en tres modos (MiniZinc, PySAT, Z3) con diferentes backends. Los usuarios pueden interactuar con él mediante comandos como add_item, delete_item, replace_item, get_model y solve_model para construir y resolver modelos de restricciones de manera programática.
Para qué se puede usar este MCP
Este MCP puede utilizarse para resolver diversos problemas de satisfacción de restricciones, incluyendo puzzles lógicos (como N-Reinas), problemas de optimización (como el Viajante de Comercio) y escenarios del mundo real que requieran solucionadores SAT/SMT o programación con restricciones.
