This server connects Claude to five constraint solving backends: MiniZinc for constraint programming, PySAT for boolean satisfiability, MaxSAT for optimization, Z3 for SMT solving, and Clingo for answer set programming. You get six core operations to build and manipulate models incrementally: add items, delete items, replace items, clear the model, inspect current state, and solve with timeout. Reach for this when you need Claude to tackle scheduling problems, resource allocation, logic puzzles, or any combinatorial optimization where you want to iteratively build constraint models through conversation rather than writing solver code directly.
claude mcp add --transport stdio szeider-mcp-solver uvx mcp-solver