MCP HubMCP Hub
szeider

mcp-solver

by: szeider

Model Context Protocol (MCP) server for constraint optimization and solving"

54created 14/12/2024
Visit
optimization
solving

📌Overview

Purpose: The MCP Solver aims to integrate MiniZinc constraint programming capabilities with Large Language Models (LLMs) via the Model Context Protocol, facilitating AI-driven model management and solution processes.

Overview: The MCP Solver provides an interface for LLMs to create, edit, validate, and solve constraint models while managing solution insights and model modifications through a memo system. It is designed for use with MiniZinc and supports various operating systems, making it versatile for different environments.

Key Features:

  • Finite Domain and Global Constraint Support: Enables the use of diverse constraints in model creation and solving.

  • Asynchronous Solving with Configurable Timeouts: Improves performance and allows for flexible solving depending on the complexity of constraints.

  • Item-based Model Editing: Enhances robustness by validating each model item individually, ensuring accurate and reliable modifications.

  • Solution State Management: Keeps track of the current state of solutions to facilitate updates and validations in real-time.

  • Knowledge Base Maintenance: Manages insights and solver information effectively through a memo system, aiding in the process of continuous learning and adaptation for the AI.

MCP Solver

A Model Context Protocol (MCP) server that exposes SAT, SMT and constraint solving capabilities to Large Language Models.

Overview

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
  • SMT formulas in Z3 Python

For a detailed description of the MCP Solver's system architecture and theoretical foundations, see the research paper: Stefan Szeider, "MCP-Solver: Integrating Language Models with Constraint Programming Systems", arXiv:2501.00539, 2024.

Available Tools

In the following, item refers to some part of the (MiniZinc/PySAT/Z3) code, and model to the encoding.

Tool NameDescription
clear_modelRemove all items from the model
add_itemAdd new item at a specific index
delete_itemDelete item at index
replace_itemReplace item at index
get_modelGet current model content with numbered items
solve_modelSolve the model (with timeout parameter)

System Requirements

  • Python 3.11+ and project manager uv
  • Mode-specific requirements: MiniZinc, PySAT, Python Z3 (installed via pip)
  • Operating systems: macOS, Windows, Linux (with appropriate adaptations)

Installation

MCP Solver requires Python 3.11+, the uv package manager, and solver-specific dependencies (MiniZinc, Z3, or PySAT).

Quick start:

git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv
source .venv/bin/activate
uv pip install -e ".[all]"  # Install all solvers

Available Modes / Solving Backends

The MCP Solver provides three distinct operational modes, each integrating with a different constraint solving backend.

MiniZinc Mode

  • Rich constraint expression with global constraints
  • Integration with the Chuffed constraint solver
  • Optimization capabilities
  • Access to solution values via get_solution

Dependencies: Requires the minizinc package

Run command:

mcp-solver-mzn

PySAT Mode

  • Propositional constraint modeling using CNF
  • Access to various SAT solvers (Glucose3, Glucose4, Lingeling, etc.)
  • Cardinality constraints support
  • Boolean constraint solving

Dependencies: Requires the python-sat package

Run command:

mcp-solver-pysat

Z3 Mode

  • Rich type system: booleans, integers, reals, bitvectors, arrays
  • Constraint solving with quantifiers
  • Optimization capabilities
  • Template library for common modeling patterns

Dependencies: Requires the z3-solver package

Run command:

mcp-solver-z3

MCP Test Client

The MCP Solver includes an MCP client for development and diagnostics, based on the ReAct agent framework. This client translates natural language problem statements into formal constraint programming solutions.

Installation

uv pip install -e ".[client]"
uv run test-setup-client

The client requires an API key from an LLM provider (default: Anthropic Claude Sonnet 3.7). Set ANTHROPIC_API_KEY in your environment or in a .env file.

Usage

Commands for each solver backend:

# MiniZinc mode
uv run run-test mzn --problem <path/to/problem.md>

# PySAT mode
uv run run-test pysat --problem <path/to/problem.md>

# Z3 mode
uv run run-test z3 --problem <path/to/problem.md>

Examples

Example 1: Casting Problem (MiniZinc)

Problem:

A theatrical director must cast either Actress Alvarez or Actor Cohen. Alvarez won't work with Cohen and demands that Actor Davenport be cast. The producer insists on Actor Branislavsky, who won't work with Alvarez or Davenport. Can the play be cast?

Model:

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;

Solution:

Cast Cohen and Branislavsky, but not Alvarez or Davenport.

Example 2: N-Queens Problem (MiniZinc)

Problem:

Place n Queens on an nxn chessboard so that none attacks another. Test for n=10,20,30,40.

Model:

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;

Solving times comparison:
n=10: 0.001s
n=20: 0.005s
n=30: 0.040s
n=40: 0.043s

Solutions exist for all tested board sizes.

Example 3: Traveling Salesperson Problem (MiniZinc)

Problem:

A saleswoman based in Vienna needs to plan a tour visiting all 9 provincial capitals once. Distances (km) between cities are provided.

Model:

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;

Solution:

Optimal route and total distance 1,564 km:
Vienna → St. Pölten → Linz → Salzburg → Bregenz → Innsbruck → Klagenfurt → Graz → Eisenstadt → Vienna.

Feedback

Provide feedback via this form: https://form.jotform.com/szeider/mcp-solver-feedback-form

Disclaimer

This MCP Solver is in prototype stage. Use with caution. Any critical use is at own risk.

License

This project is licensed under the MIT License - see the LICENSE file for details.