MCP server providing Z3 SMT solver capabilities
npm install yuwakisa-z3solver-mcpsolve_smtlib tool with the SMT-LIB code
npx - no manual setup required
bash
cd z3solver
npm install
`
This will install:
- @modelcontextprotocol/sdk - MCP protocol implementation
- z3-solver - Z3 SMT solver WASM bindings
- TypeScript and development tools
Running the Server
$3
`bash
npm run dev
`
$3
`bash
npm run build
npm start
`
$3
`bash
npx tsx src/index.ts
`
Claude Desktop Configuration
Add this configuration to your Claude Desktop config file:
Windows: %APPDATA%\Claude\claude_desktop_config.json
macOS: ~/Library/Application Support/Claude/claude_desktop_config.json
Linux: ~/.config/Claude/claude_desktop_config.json
$3
`json
{
"mcpServers": {
"z3_solver": {
"command": "npx",
"args": ["-y", "yuwakisa-z3solver-mcp"]
}
}
}
`
$3
`json
{
"mcpServers": {
"z3_solver": {
"command": "node",
"args": ["/path/to/mcp-wrappers/z3solver/build/index.js"]
}
}
}
`
Available MCP Tools
$3
Execute the Z3 solver on SMT-LIB input and return raw SMT-LIB results.
Parameters:
- smtlib (string): Valid SMT-LIB2 code
- timeout_ms (number, optional): Timeout in milliseconds (default: 30000)
Returns: SMT-LIB formatted string with status as comment
Example SMT-LIB Input:
`smtlib
(set-option :produce-unsat-cores true)
(declare-const x Int)
(declare-const y Int)
(assert (! (> x 0) :named x-positive))
(assert (! (> y 0) :named y-positive))
(assert (! (< (+ x y) 10) :named sum-less-than-10))
(check-sat)
`
Example Response (sat):
`smtlib
; sat
(model
(define-fun x () Int 3)
(define-fun y () Int 4)
)
`
Example Response (unsat):
`smtlib
; unsat
(x-positive y-positive sum-less-than-10)
`
Example Response (unknown):
`smtlib
; unknown
`
Usage Example
Once configured in Claude Desktop, you can interact with the solver through natural language:
`
You: I have 4 people (Alice, Bob, Carol, David) who need to be assigned to 2 teams.
Alice and Bob can't be on the same team. Each team needs at least one person.
Can you find a valid assignment?
Claude: I'll solve this constraint problem using the Z3 solver.
[Claude translates your problem to SMT-LIB]
[Claude calls solve_smtlib with the SMT-LIB code]
[Claude receives raw solver output]
[Claude interprets the results]
Claude: Here's a valid assignment:
- Team 1: Alice, Carol
- Team 2: Bob, David
This satisfies all constraints: Alice and Bob are on different teams,
and each team has at least one person.
`
Typical Workflow
1. You describe your constraint problem in natural language
2. Claude translates to SMT-LIB format (using its native capabilities)
3. Claude calls solve_smtlib with the SMT-LIB code
4. Server executes Z3 and returns raw SMT-LIB results (model or unsat core)
5. Claude interprets the raw results and explains the solution or conflict to you
The server is stateless and only provides Z3 solving capability. All translation and interpretation happens in Claude.
Development
$3
`
z3solver/
├── src/
│ ├── index.ts # Main entry point
│ ├── server.ts # MCP server setup
│ ├── tools/
│ │ └── solve.ts # solve_smtlib tool
│ └── solver/
│ └── z3wrapper.ts # Z3 solver wrapper
├── tests/ # Unit tests
├── package.json
├── tsconfig.json
├── README.md
└── SPEC.md
`
$3
`bash
npm run build
`
Output is generated in the build/ directory.
$3
`bash
npm test
`
$3
`bash
npm run typecheck
`
$3
`bash
npm run lint
`
Common Problems
$3
If the Z3 solver fails to initialize:
- Ensure z3-solver package is installed: npm install z3-solver
- Check Node.js version is 18 or higher
- Try reinstalling dependencies: rm -rf node_modules && npm install
$3
If you get syntax errors:
- Ensure your SMT-LIB code is valid SMT-LIB2 format
- Check that all variables are declared before use
- Verify parentheses are balanced
- For unsat cores, ensure you use (set-option :produce-unsat-cores true) and named assertions
$3
If the solver times out:
- Simplify your problem constraints
- Increase timeout in the tool call: solve_smtlib(smtlib, 60000) for 60 seconds
- Break the problem into smaller independent subproblems
- Consider if the problem size is too large for SMT solving
$3
If you see WASM memory errors:
- Check for syntax errors in your SMT-LIB code
- Verify you're not using unsupported Z3 features
- Try simplifying the problem
- Ensure you're using valid SMT-LIB2 syntax
Good Problems for SMT Solvers
SMT solvers excel at:
- Scheduling: Meeting times, resource allocation, shift scheduling
- Logic Puzzles: Sudoku, N-Queens, Einstein's riddle, graph coloring
- Configuration: Selecting compatible components, dependency resolution
- Planning: Sequencing tasks with constraints, route finding with rules
- Verification: Checking if a configuration satisfies all requirements
SMT solvers are less suitable for:
- Optimization problems (maximize/minimize) - use optimization solvers
- Continuous numerical problems - use numerical optimization
- Machine learning tasks - use ML frameworks
- Large-scale data processing - use databases or data pipelines
Dependencies
Core:
- @modelcontextprotocol/sdk - MCP protocol implementation
- z3-solver - Z3 SMT solver WASM bindings
Development:
- typescript - TypeScript compiler
- tsx - TypeScript execution runtime
- @types/node - Node.js type definitions
Runtime:
- Node.js 18+ with fetch API support
Related Documentation
- SPEC.md - Technical specification with detailed requirements
- Z3 SMT-LIB2 Guide - SMT-LIB2 syntax reference
- Model Context Protocol - MCP documentation
- Z3 GitHub - Z3 theorem prover
License
MIT License - see LICENSE file for details
Status
This project is under active development. The core functionality is implemented, but additional features and optimizations are planned.
Contributing
Contributions are welcome! Please:
1. Fork the repository
2. Create a feature branch
3. Add tests for new functionality
4. Ensure all tests pass
5. Submit a pull request
Acknowledgments
- Built with the Model Context Protocol
- Uses Z3 Theorem Prover via z3-solver npm package
- Inspired by the web-based SMT solver demo in example/solver/`