MCP Solver

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

------

Overview

The MCP Solver integrates constraint solving, SAT, SMT, and ASP 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
- Answer Set Programs in Clingo

For a detailed description of the MCP Solver's system architecture and theoretical foundations, see the accompanying research paper: Stefan Szeider, "Bridging Language Models and Symbolic Solvers via the Model Context Protocol", SAT 2025.

Available Tools

In the following, item refers to some part of the (MiniZinc/PySAT/Z3/ASP) 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 five 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

ASP Mode

ASP (Answer Set Programming) mode provides integration with ASP solvers (e.g., Clingo) for declarative problem solving with logic programs. Features include:

- Expressive logic programming for combinatorial and knowledge representation problems
- Support for constraints, choice rules, aggregates, and optimization statements
- Integration with the Clingo solver for efficient answer set computation
- Access to answer sets and model inspection

Dependencies: Requires the clingo package (uv pip install -e ".[asp]" or included in [all])

Configuration: To run in ASP mode, use:

mcp-solver-asp

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

```bash