Constrained Optimization MCP Server

Solve constraint satisfaction problems using Z3 SMT solver. This tool is ideal for logical reasoning, puzzle solving, and constraint satisfaction problems where you need to find values that satisfy a set of logical constraints. Args: variables: List of variable definitions with 'name' and 'type' fields constraints: List of constraint expressions as strings description: Optional problem description timeout: Optional timeout in milliseconds Returns: Solution results including variable values and satisfiability status Example: variables = [ {"name": "x", "type": "integer"}, {"name": "y", "type": "integer"} ] constraints = [ "x + y == 10", "x - y == 2" ]

{ "properties": { "constraints": { "items": { "type": "string" }, "title": "Constraints", "type": "array" }, "description": { "default": "", "title": "Description", "type": "string" }, "timeout": { "default": null, "title": "Timeout", "type": "integer" }, "variables": { "items": { "additionalProperties": { "type": "string" }, "type": "object" }, "title": "Variables", "type": "array" } }, "required": [ "variables", "constraints" ], "type": "object" }