Hugging Face's logo

Spaces:
JavadBayazi
/
SolverSphere
Sleeping

App Files Community
SolverSphere / README.md
JavadBayazi's picture
JavadBayazi
Update README.md
f311f85 verified
preview code
|
raw
history blame contribute delete
7.83 kB

A newer version of the Gradio SDK is available: 6.13.0

Upgrade
metadata 
title: SolverSphere — MCP Constraint Solver
emoji: 🧩
colorFrom: purple
colorTo: blue
sdk: gradio
sdk_version: 6.2.0
app_file: app.py
pinned: false
python_version: '3.11'
tags:
  - mcp
  - constraint-solving
  - sat
  - smt
  - asp
  - optimization
  - model-context-protocol

🧩 SolverSphere — MCP Constraint Solving & Optimization

MCP Compatible Gradio License: MIT

This is an MCP-enabled Hugging Face Space for SolverSphere by Javad Bayazi — an open-source Model Context Protocol (MCP) server that exposes constraint solving, SAT, SMT, and ASP capabilities to Large Language Models. This Space can be added as an MCP tool to Claude Desktop, Cursor, or any other MCP-compatible client with a single click!

🌟 What is MCP Solver?

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:

Maintainer: Javad Bayazi (Hugging Face: https://huggingface.co/JavadBayazi)

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.

🔧 Supported Solvers

🎯 MiniZinc Mode

MiniZinc mode provides integration with the MiniZinc constraint modeling language:

  • Rich constraint expression with global constraints
  • Integration with the Chuffed constraint solver
  • Optimization capabilities
  • Access to solution values

🔬 Z3 SMT Mode

Z3 mode allows interaction with the Z3 theorem prover:

  • Satisfiability Modulo Theories (SMT)
  • Support for integers, reals, bit-vectors, arrays, and more
  • Theory combination and quantifiers
  • High-performance theorem proving

✅ PySAT Mode

PySAT mode allows interaction with the Python SAT solving toolkit:

  • 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

📊 MaxSAT Mode

MaxSAT mode provides optimization over SAT formulas:

  • Weighted partial MaxSAT solving
  • Hard and soft constraints
  • Multiple MaxSAT solver backends
  • Optimization objectives

💡 ASP Mode

Answer Set Programming mode using Clingo:

  • Logic programming with stable model semantics
  • Choice rules and aggregates
  • Multi-shot solving capabilities
  • Ground and solve ASP programs

🚀 Quick Start

Option 1: Use Hugging Face Space as MCP Tool

  1. Install an MCP Client:

  2. Add MCP Solver to Your Client:

    • Click the MCP badge on this Space
    • Select "Add to MCP tools"
    • Confirm when prompted
    • The tools will be available instantly in your MCP client!

  3. Use MCP Solver in Your AI Assistant:

    Ask Claude: "Create a SAT problem to solve graph coloring"
Ask Cursor: "Build a Z3 model to verify array bounds"

Option 2: Install from GitHub (Local MCP Server) 

# Install MCP Solver
git clone https://github.com/szeider/mcp-solver.git
cd mcp-solver
uv venv
source .venv/bin/activate  # On Windows: .venv\Scripts\activate
uv pip install -e ".[all]"  # Install all solvers

# Configure Claude Desktop (macOS)
# Edit: ~/Library/Application Support/Claude/claude_desktop_config.json
{
  "mcpServers": {
    "mcp-solver-z3": {
      "command": "mcp-solver-z3"
    },
    "mcp-solver-pysat": {
      "command": "mcp-solver-pysat"
    }
  }
}

# Restart Claude Desktop and start using MCP Solver!

See INSTALL.md for detailed installation instructions.

Option 3: Use Web Interface

  1. Select a solver tool (MiniZinc, Z3, PySAT, MaxSAT, or ASP)
  2. Build your model by adding items
  3. Click "Solve Model" to run
  4. View results in JSON format

📖 Example Usage

In MCP Clients (Claude Desktop, Cursor, etc.) 

# SAT solving with PySAT
add_item(index=0, content="cnf.append([1, 2, -3])")
add_item(index=1, content="cnf.append([-1, -2])")
solve_model(timeout=60)

# SMT solving with Z3
add_item(index=0, content="x = Int('x')")
add_item(index=1, content="y = Int('y')")
add_item(index=2, content="solver.add(x + y == 10)")
add_item(index=3, content="solver.add(x > y)")
solve_model(timeout=60)

# ASP solving with Clingo
add_item(index=0, content="bird(tweety).")
add_item(index=1, content="flies(X) :- bird(X), not abnormal(X).")
solve_model(timeout=60)

In Web Interface

  1. Go to the desired solver tab (e.g., Z3 SMT)
  2. Add items using the "Add Item" interface
  3. Enter index (e.g., 0) and content (e.g., x = Int('x'))
  4. Click "Add Item"
  5. Repeat for all constraints
  6. Click "Solve Model" with a timeout
  7. View the solution in JSON format

🎯 Available Tools

All solvers support these MCP tools:

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)

💻 Development

Deploy Your Own Space

  1. Fork this repository or create a new Space
  2. Copy the contents of the hf-space folder
  3. Upload to your Hugging Face Space
  4. The Space will automatically install dependencies and launch!

Running Locally 

cd hf-space
pip install -r requirements.txt
python app.py

🔗 Resources

📄 License

MIT License - See LICENSE file for details

🙏 Acknowledgments

🏅 Credits

This Space provides both a web interface for interactive use and MCP server capabilities for AI assistants. Add it to your MCP client and let AI solve complex constraint problems!