mcp-solver
If you are the rightful owner of mcp-solver and would like to certify it and/or have it hosted online, please leave a comment on the right or send an email to henry@mcphub.com.
A Model Context Protocol (MCP) server that exposes SAT, SMT, and constraint solving capabilities to Large Language Models.
The MCP Solver integrates SAT, SMT, and Constraint Solving with LLMs through the Model Context Protocol, enabling AI models to interactively create, edit, and solve constraint models in MiniZinc, SAT models in PySAT, and SMT formulas in Z3 Python. It provides a robust framework for integrating language models with constraint programming systems, allowing for the translation of natural language problem statements into formal constraint programming solutions. The system supports various operational modes, each tailored to specific solving backends, and includes a test client for development and experimentation.
Features
- Integration with MiniZinc, PySAT, and Z3 Python for constraint solving.
- Tools for model manipulation: clear, add, delete, replace, get, and solve.
- Support for multiple operational modes with specific dependencies.
- Includes a test client for development and experimentation.
- Facilitates translation of natural language into formal constraint solutions.
Tools
clear_model
Remove all items from the model
add_item
Add new item at a specific index
delete_item
Delete item at index
replace_item
Replace item at index
get_model
Get current model content with numbered items
solve_model
Solve the model (with timeout parameter)
