What is Z3 Solver Mcp Server

The z3-solver-mcp-server is a Model Context Protocol (MCP) server that utilizes the Z3 theorem prover to provide SMT (Satisfiability Modulo Theories) solving capabilities. It enables clients like Claude to address complex constraint satisfaction problems, mathematical equations, logic puzzles, and optimization challenges.

Use cases

Use cases include solving age-related problems, algebraic equations, logic puzzles, and optimization scenarios such as maximizing areas with given constraints.

How to use

To use the z3-solver-mcp-server, clone the repository, install dependencies using ‘uv’ or ‘pip’, and configure the server in the Claude Desktop configuration file. After setup, you can input various problems for the server to solve.

Key features

Key features include SMT-LIB2 support for standard problem formats, integration with Microsoft’s Z3 theorem prover, capabilities for solving mathematical problems including algebra and optimization, and a simple interface for input and output.

Where to use

The z3-solver-mcp-server can be used in fields such as computer science, mathematics, artificial intelligence, and operations research, where complex problem-solving is required.

Z3 SMT Solver MCP Server

A Model Context Protocol (MCP) server that provides SMT (Satisfiability Modulo Theories) solving capabilities using the Z3 theorem prover. This server allows Claude and other MCP clients to solve complex constraint satisfaction problems, mathematical equations, logic puzzles, and optimization problems.

Features

• SMT-LIB2 Support: Accepts problems in the standard SMT-LIB2 format
• Z3 Integration: Powered by Microsoft’s Z3 theorem prover
• Mathematical Problem Solving: Handle algebra, logic, optimization, and constraint satisfaction
• Simple Interface: Single tool with string input/output

Installation

Prerequisites

• Python 3.8 or higher
• uv (recommended) or pip

Setup

1. Clone this repository:

git clone <repository-url>
cd z3-mcp-server

2. Install dependencies:

uv sync

Or with pip:

pip install z3-solver mcp

3. Make the server executable:

chmod +x src/z3_mcp_server/main.py

Usage

With Claude Desktop

Add the server to your Claude Desktop configuration file:

macOS: ~/Library/Application Support/Claude/claude_desktop_config.json
Windows: %APPDATA%/Claude/claude_desktop_config.json

{
  "mcpServers": {
    "z3-solver": {
      "command": "uv",
      "args": [
        "--directory",
        "/path/to/z3-mcp-server",
        "run",
        "main.py"
      ],
      "env": {}
    }
  }
}

Example Problems

Once configured, you can ask Claude to solve various types of problems:

Age Problems:

“Joey is 20 years younger than Becky. In two years, Becky will be twice as old as Joey. How old are they?”

Algebra:

“Find integers x and y such that 2x + 3y = 17 and both are positive.”

Logic Puzzles:

“Three people have ages 21, 22, and 23. Alice is not 21, and Bob is older than Alice. What are their ages?”

Optimization:

“A farmer has 100 feet of fencing. What rectangular dimensions maximize the enclosed area?”

Tool Reference

solve_smt_lib2

Solves constraint problems specified in SMT-LIB2 format.

Parameters:

• problem (string): The constraint problem in SMT-LIB2 syntax

Returns:

• String containing the solver result:
  • sat + model if satisfiable
  • unsat if no solution exists
  • unknown if solver cannot determine
  • Error message if parsing fails

Example SMT-LIB2 Input:

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (= (* x y) 21))
(check-sat)
(get-model)

SMT-LIB2 Quick Reference

Basic Syntax

• (declare-const name Type) - Declare a variable
• (assert condition) - Add a constraint
• (check-sat) - Check if constraints are satisfiable
• (get-model) - Get variable assignments (if sat)

Types

• Int - Integers
• Real - Real numbers
• Bool - Boolean values

Operations

• Arithmetic: +, -, *, /, mod
• Comparison: =, <, >, <=, >=
• Logic: and, or, not
• Special: distinct (all different)

Transport Support

Currently supports:

• stdio: For use with Claude Desktop and similar local clients

Planned:

• HTTP/WebSocket: For web-based integrations

Troubleshooting

Common Issues

1. Server not starting: Ensure Python and z3-solver are properly installed
2. Permission denied: Make sure the main.py file is executable
3. Import errors: Verify all dependencies are installed in the correct environment

Debug Mode

Run the server directly in the Inspector:

npx @modelcontextprotocol/inspector src/z3_mcp_server/main.py uv --directory /path/to/z3-mcp-server run main.py

Contributing

Contributions are welcome! Please:

1. Fork the repository
2. Create a feature branch
3. Add tests for new functionality
4. Submit a pull request