Solver

What is MCP Solver?

MCP Solver is a Model Context Protocol (MCP) server designed to integrate SAT, SMT, and constraint solving with Large Language Models (LLMs). It allows AI models to interactively define, modify, and solve various types of constraint and optimization problems, bridging the gap between natural language problem descriptions and formal constraint programming solutions.

How to use MCP Solver?

To use MCP Solver, you need Python 3.11+ and the uv package manager. After cloning the repository, install the dependencies using uv venv and uv pip install -e ".[all]". The solver provides four operational modes, each integrating with a different constraint solving backend: MiniZinc, PySAT, MaxSAT, and Z3. You can run the solver in a specific mode using commands like mcp-solver-mzn or mcp-solver-pysat. An MCP test client is also available for development and experimentation, allowing interaction with the solver through an LLM. The client requires an API key from an LLM provider (e.g., Anthropic, OpenAI, Google).

Key Features of MCP Solver

• Integration with LLMs: Enables AI models to interactively create, edit, and solve constraint problems.
• Multiple Solving Backends: Supports MiniZinc, PySAT (for SAT and MaxSAT), and Z3 (for SMT).
• Constraint Modeling: Allows modeling of problems in MiniZinc, SAT models in PySAT, MaxSAT optimization problems, and SMT formulas in Z3 Python.
• Toolset for Model Manipulation: Provides tools like clear_model, add_item, delete_item, replace_item, get_model, and solve_model for managing model content.
• Optimization Capabilities: Supports optimization problems in MiniZinc, MaxSAT, and Z3 modes.
• Flexible Deployment: Can be run on macOS, Windows, and Linux.
• MCP Test Client: Includes a client for development and testing, facilitating natural language interaction with the solver via an LLM.

Use Cases of MCP Solver

• Automated Problem Solving: LLMs can be used to describe complex constraint problems in natural language, and MCP Solver can translate these into formal models and find solutions.
• Educational Tool: Demonstrating how LLMs can interact with symbolic solvers for constraint satisfaction and optimization.
• Research and Development: Exploring the integration of AI with constraint programming systems for various applications.
• Interactive Constraint Programming: Users can interactively build and solve constraint models with the assistance of an LLM.
• Resource Allocation and Scheduling: Solving problems related to resource allocation, scheduling, and logistics by defining constraints and optimizing objectives.

FAQ from MCP Solver

Q: What are the system requirements for MCP Solver? A: MCP Solver requires Python 3.11+ and the uv package manager. Mode-specific requirements include MiniZinc, PySAT, and Python Z3. It runs on macOS, Windows, and Linux.

Q: How do I install MCP Solver? A: After cloning the repository, navigate to the directory and run uv venv, then source .venv/bin/activate, and finally uv pip install -e ".[all]". Detailed instructions are available in INSTALL.md.

Q: What are the different operational modes available? A: MCP Solver provides MiniZinc, PySAT, MaxSAT, and Z3 modes, each integrating with a specific constraint solving backend and offering unique capabilities.

Q: How does the MCP Test Client work? A: The MCP Test Client acts as an intermediary between an LLM and the MCP server, translating natural language problem statements into formal constraint programming solutions. It requires an API key from an LLM provider.

Q: Is MCP Solver ready for production use? A: No, MCP Solver is currently in its prototype stage. Users are encouraged to experiment, but any use in critical environments is at their own risk.

---

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
• MaxSAT optimization problems in PySAT
• SMT formulas in Z3 Python

For a detailed description of the MCP Solver's system architecture and theoretical foundations, see the accompanying 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 (MinZinc/Pysat/Z3) code, and model to the encoding.

Tool Name	Description
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)

---

System Requirements

• Python and project manager uv
• Python 3.11+
• Mode-specific requirements: MiniZinc, PySAT, Python Z3 (required packages are 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).

For detailed installation instructions for Windows, macOS, and Linux, see INSTALL.md.

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 four distinct operational modes, each integrating with a different constraint solving backend. Each mode requires specific dependencies and offers unique capabilities for addressing different classes of problems.

MiniZinc Mode

MiniZinc mode provides integration with the MiniZinc constraint modeling language with the following features:

• 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 (uv pip install -e ".[mzn]")

Configuration: To run in MiniZinc mode, use:

mcp-solver-mzn

PySAT Mode

PySAT mode allows interaction with the Python SAT solving toolkit with the following features:

• Propositional constraint modeling using CNF (Conjunctive Normal Form)
• Access to various SAT solvers (Glucose3, Glucose4, Lingeling, etc.)
• Cardinality constraints (at_most_k, at_least_k, exactly_k)
• Support for boolean constraint solving

Dependencies: Requires the python-sat package (uv pip install -e ".[pysat]")

Configuration: To run in PySAT mode, use:

mcp-solver-pysat

MaxSAT Mode

MaxSAT mode provides specialized support for optimization problems with PySAT, featuring:

• Weighted Conjunctive Normal Form (WCNF) support
• Integration with the RC2 MaxSAT solver
• Optimization capabilities with objective tracking
• Support for both hard and soft constraints

Dependencies: Requires the python-sat package (uv pip install -e ".[pysat]")

Configuration: To run in MaxSAT mode, use:

mcp-solver-maxsat

Z3 Mode

Z3 mode provides access to Z3 SMT (Satisfiability Modulo Theories) solving capabilities with the following features:

• 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 (uv pip install -e ".[z3]")

Configuration: To run in Z3 mode, use:

mcp-solver-z3

MCP Test Client

The MCP Solver includes an MCP client for development, experimentation, and diagnostic purposes, based on the ReAct agent framework. This client serves as an intermediary between an LLM and the MCP server, facilitating the translation of natural language problem statements into formal constraint programming solutions.

Installation

# Install client dependencies
uv pip install -e ".[client]"

# Verify client installation and configuration
uv run test-setup-client

The client requires an API key from an LLM provider. For Anthropic (the default LLM is Claude Sonnet 3.7), set the ANTHROPIC_API_KEY environment variable. This can be set in your environment or included in a .env file in the project root.

The client also supports other LLM providers including OpenAI, Google (Gemini), OpenRouter, and even local models via LM Studio. You can specify which model to use with the --mc command line flag. See INSTALL.md for details on model code formats.

Usage

The client provides specialized 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>

# MaxSAT mode
uv run run-test maxsat --problem <path/to/problem.md>

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

---

Examples

Example 1: Casting Problem (MiniZinc)

This is based on an example by George Johnson (NYT, July 13, 1999).

User

Suppose that a theatrical director feels obligated to cast either his ingenue, Actress Alvarez, or his nephew, Actor Cohen, in a production. But Miss Alvarez won't be in a play with Mr. Cohen (her former lover), and she demands that the cast include her new flame, Actor Davenport. The producer, with her own favors to repay, insists that Actor Branislavsky have a part. But Mr. Branislavsky won't be in any play with Miss Alvarez or Mr. Davenport. Can the director cast the play?

System: clear_model

Model cleared

System: add_item (multiple)

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;

System: solve_model

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

The solution (cast Cohen and Branislavsky, but not Alvarez or Davenport) satisfies all constraints.

Example 2: N-Queens Problem (MiniZinc)

User

Check whether you can place n Queens on an nxn chessboard. Try n=10,20,30,40 and compare the solving times

System: clear_model

Model cleared

System: add_item (multiple)

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;

System: solve_model (with n=10, 20, 30, and 40 by changing the value of n)

Solve 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. Time complexity increases non-linearly but remains manageable up to n=40.

Example 3: Traveling Salesperson Problem (MiniZinc)

User

A saleswoman based in Vienna needs to plan her upcoming tour through Austria, visiting each province capital once. Help find the shortest route. Distances in km: 1=Vienna, 2=St. Pölten, 3=Eisenstadt, 4=Linz, 5=Graz, 6=Klagenfurt, 7=Salzburg, 8=Innsbruck, 9=Bregenz

[Distance matrix table provided in user message]

System: add_item (multiple)

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;

System: solve_model

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

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

Feedback

You can provide feedback to the author via this form.

Disclaimer

This MCP Solver is in its prototype stage and should be used with caution. Users are encouraged to experiment, but any use in critical environments is at their own risk.

---

License

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

---