Z3 Solver

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