Skip to main content
Glama

USolver

by sdiehl

USolver

A Model Context Protocol server that exposes tools for solving combinatorial, convex, integer programming, and non-linear optimization problems. Exposes interfaces to the following solvers:

  • ortools - Combinatorial optimization solver
  • cvxpy - Convex optimization solver
  • z3 - SMT solver over booleans, integers, reals, and strings

To install run the install.py script. This will install the MPC server for Claude Desktop and/or Cursor.

uv run install.py

Then open Claude or Cursor and you should see the MCP tool usolver available in the tool list.

Examples

To run the individual solver examples. You can invoke the individual examples. Below are example prompts that you can feed to the language model for these specific problems.

uv run examples/example_z3.py uv run examples/example_cvxpy.py uv run examples/example_ortools.py uv run examples/example_z3_simple.py

Logic Puzzle

You and a friend pass by a standard coin operated vending machine and you decide to get a candy bar. The price is US $0.95, but after checking your pockets you only have a dollar (US $1) and the machine only takes coins. You turn to your friend and have this conversation: You: Hey, do you have change for a dollar? Friend: Let's see. I have 6 US coins but, although they add up to a US $1.15, I can't break a dollar. You: Huh? Can you make change for half a dollar? Friend: No. You: How about a quarter? Friend: Nope, and before you ask I cant make change for a dime or nickel either. You: Really? and these six coins are all US government coins currently in production? Friend: Yes. You: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back? Friend: Sorry, I would like to but I can't with the coins I have. What coins are your friend holding?

This can be fed into usolver and it will generate a constraint system:

Loading... is the collection of the six unknown coin values, Loading... through Loading..., each of which must be a positive whole number representing cents.

Loading...

Loading... is the collection of every possible way you could choose two or more of your six coins.

Loading...

Exclude the 50 cent coin from being used in the vending machine.

Loading...

Constraint 0: The sum of the values of all six coins is 115 cents.

Loading...

Constraint 1: Cannot make change for a dollar.

Loading...

Constraint 2: Cannot make change for half a dollar.

Loading...

Constraint 3: Cannot make change for a quarter.

Loading...

Constraint 4: Cannot make change for a dime.

Loading...

Constraint 5: Cannot make change for a nickel

Loading...

Constraint 6: Cannot buy the candy bar for 95 cents if half dollar is excluded.

Loading...

If you feed this to solver it will synthesize the above constraint system, solve it with Z3, and return the solution.

Your friend has: 1 half dollar, 1 quarter, and 4 dimes This totals 50¢ + 25¢ + 40¢ = 115¢ = $1.15 ✓ This is exactly 6 coins ✓

Z3

A chemical engineering example:

Use usolver to design a water transport pipeline with the following requirements: * Volumetric flow rate: 0.05 m³/s * Pipe length: 100 m * Water density: 1000 kg/m³ * Maximum allowable pressure drop: 50 kPa * Flow continuity: Q = π(D/2)² × v * Pressure drop: ΔP = f(L/D)(ρv²/2), where f ≈ 0.02 for turbulent flow * Practical limits: 0.05 ≤ D ≤ 0.5 m, 0.5 ≤ v ≤ 8 m/s * Pressure constraint: ΔP ≤ 50,000 Pa * Find: optimal pipe diameter and flow velocity

CVXPY

A simple convex optimization problem minimizing the 2-norm of a linear system:

Use usolver to solve the following convex optimization problem: Minimize: ||Ax - b||₂² Subject to: 0 ≤ x ≤ 1 where A = [1.0, -0.5; 0.5, 2.0; 0.0, 1.0] b = [2.0, 1.0, -1.0]

OR-Tools

A classic worker shift scheduling problem:

Use usolver to solve a nurse scheduling problem with the following requirements: * Schedule 4 nurses (Alice, Bob, Charlie, Diana) across 3 shifts over (Monday, Tuesday, Wednesday) * Shifts: Morning (7AM-3PM), Evening (3PM-11PM), Night (11PM-7AM) * Each shift must be assigned to exactly one nurse each day * Each nurse works at most one shift per day * Distribute shifts evenly (2-3 shifts per nurse over the period) * Charlie can't work on Tuesday.

Chained Examples

A chained example that uses both OR-Tools to optimize for table layout and CVXPY to optimize for staff scheduling.

Use usolver to optimize a restaurant's layout and staffing with the following requirements in two parts. Use combinatorial optimization to optimize for table layout and convex optimization to optimize for staff scheduling. * Part 1: Optimize table layout - Mix of 2-seater, 4-seater, and 6-seater tables - Maximum floor space: 150 m² - Space requirements: 4m² (2-seater), 6m² (4-seater), 9m² (6-seater) - Maximum 20 tables total - Minimum mix: 2× 2-seaters, 3× 4-seaters, 1× 6-seater - Objective: Maximize total seating capacity * Part 2: Optimize staff scheduling using Part 1's capacity - 12-hour operating day - Each staff member can handle 20 seats - Minimum 2 staff per hour - Maximum staff change between hours: 2 people - Variable demand: 40%-100% of capacity - Objective: Minimize labor cost ($25/hour per staff)

Docker Usage

Can also run the MCP server directly from the GitHub Container Registry.

docker run -p 8081:8081 ghcr.io/sdiehl/usolver:latest

Then add the following to your client:

{ "mcpServers": { "sympy-mcp": { "command": "docker", "args": [ "run", "-i", "-p", "8081:8081", "--rm", "ghcr.io/sdiehl/usolver:latest" ] } } }

License

Released under the Apache License 2.0. See the LICENSE file for details.

-
security - not tested
A
license - permissive license
-
quality - not tested

A best-effort universal logic and numerical solver interface using MCP that implements the 'LLM sandwich' model to process queries, call dedicated solvers (ortools, cvxpy, z3), and verbalize results.

  1. Examples
    1. Logic Puzzle
    2. Z3
    3. CVXPY
    4. OR-Tools
    5. Chained Examples
  2. Docker Usage
    1. License

      Related MCP Servers

      • -
        security
        A
        license
        -
        quality
        MCP-Logic is a server that provides AI systems with automated reasoning capabilities, enabling logical theorem proving and model verification using Prover9/Mace4 through a clean MCP interface.
        Last updated -
        20
        MIT License
        • Linux
        • Apple
      • -
        security
        F
        license
        -
        quality
        A Model Context Protocol (MCP) server that provides mathematical calculations and operations using NumPy, enabling users to perform numerical computations like matrix operations, statistical analysis, and polynomial fitting directly through Claude.
        Last updated -
        1
        Python
        • Linux
        • Apple
      • A
        security
        F
        license
        A
        quality
        A lightweight MCP server that provides a unified interface to various LLM providers including OpenAI, Anthropic, Google Gemini, Groq, DeepSeek, and Ollama.
        Last updated -
        6
        218
        Python
      • A
        security
        A
        license
        A
        quality
        A Model Context Protocol server that provides basic calculator functionality for LLMs, enabling them to perform mathematical operations like addition, subtraction, multiplication, division, modulo, and square root.
        Last updated -
        6
        125
        12
        TypeScript
        MIT License
        • Linux

      View all related MCP servers

      MCP directory API

      We provide all the information about MCP servers via our MCP API.

      curl -X GET 'https://glama.ai/api/mcp/v1/servers/sdiehl/usolver'

      If you have feedback or need assistance with the MCP directory API, please join our Discord server