A Model Context Protocol server that provides language models with constraint solving, SAT, SMT, and ASP problem-solving capabilities, enabling AI models to interactively create, edit, and solve constraint models in MiniZinc, PySAT, Z3, and Clingo.

Installation

From Source Code

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

MiniZinc Mode

uv pip install -e ".[mzn]"
mcp-solver-mzn

PySAT Mode

uv pip install -e ".[pysat]"
mcp-solver-pysat

MaxSAT Mode

uv pip install -e ".[pysat]"
mcp-solver-maxsat

Z3 Mode

uv pip install -e ".[z3]"
mcp-solver-z3

Available Tools

Tool	Description
clear_model	Remove all items from the model
add_item	Add a new item at a specific index
delete_item	Delete an item by index
replace_item	Replace an item by index
get_model	Get the current model contents with numbered items
solve_model	Solve the model (with timeout parameter)

Features

• Constraint models in MiniZinc with rich constraint expressions and global constraints
• SAT models in PySAT with propositional constraint modeling via CNF
• MaxSAT optimization problems with weighted CNF support
• SMT formulas in Z3 Python with a rich type system (booleans, integers, reals, bit vectors, arrays)
• Answer Set programs in Clingo for declarative problem solving with logic programs
• Integration with multiple solver backends (Chuffed, Glucose3/4, Lingeling, RC2, Z3, Clingo)
• Optimization capabilities across all modes
• Interactive model creation, editing, and solving
• MCP test client with ReAct agent framework for development and experimentation

Environment Variables

Optional

• ANTHROPIC_API_KEY - API key for Claude Sonnet 3.5 (default LLM for the test client)

Usage Examples

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?

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

A saleswoman based in Vienna needs to plan her upcoming tour through Austria, visiting each province capital once. Help find the shortest route.

Notes

Requires Python 3.11+, the uv package manager, and dependencies for specific solvers. Available on macOS, Windows, and Linux. This is a prototype-stage project—use with caution in mission-critical environments. Includes a reference to the research paper: Stefan Szeider, 'Bridging Language Models and Symbolic Solvers via the Model Context Protocol', SAT 2025.