Constrained Optimization MCP Server

Instructions

Implementation Reference

• constrained_opt_mcp/server/main.py:61-61 (registration)

  Tool registration decorator associating the function with the name 'solve_constraint_satisfaction'.
  @app.tool("solve_constraint_satisfaction")
• constrained_opt_mcp/server/main.py:62-156 (handler)

  The primary MCP tool handler: parses user inputs into Z3 models, delegates to Z3 solver, formats results as JSON text content.
  async def solve_constraint_satisfaction( variables: List[dict[str, str]], constraints: List[str], description: str = "", timeout: int = None, ) -> List[TextContent]: """ 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" ] """ try: # Convert to Z3 problem problem_variables = [] for var in variables: if "name" not in var or "type" not in var: return [ TextContent( type="text", text="Each variable must have 'name' and 'type' fields", ) ] try: from ..models.z3_models import Z3VariableType var_type = Z3VariableType(var["type"]) except ValueError: return [ TextContent( type="text", text=( f"Invalid variable type: {var['type']}. " f"Must be one of: integer, real, boolean, string" ), ) ] problem_variables.append(Z3Variable( name=var["name"], type=var_type, description=var.get("description", "") )) problem_constraints = [Z3Constraint(expression=expr) for expr in constraints] problem = Z3Problem( variables=problem_variables, constraints=problem_constraints, description=description, timeout=timeout, ) # Solve the problem result = solve_z3_problem(problem) match result: case Success(solution): return [ TextContent( type="text", text=json.dumps( { "values": solution.values, "is_satisfiable": solution.is_satisfiable, "status": solution.status, "solve_time": solution.solve_time, } ), ) ] case Failure(error): return [TextContent(type="text", text=f"Error solving problem: {error}")] except Exception as e: return [TextContent(type="text", text=f"Error in solve_constraint_satisfaction: {e!s}")]
• constrained_opt_mcp/models/z3_models.py:76-115 (schema)

  Pydantic schema/model for Z3Problem used by the handler to structure the constraint satisfaction problem.
  class Z3Problem(BaseProblem): """Complete Z3 constraint satisfaction problem.""" model_config = {"arbitrary_types_allowed": True} variables: List[Z3Variable] = Field(..., description="Problem variables") constraints: List[Z3Constraint] = Field(..., description="Problem constraints") description: str = Field(default="", description="Problem description") # Z3-specific properties problem_type: ProblemType = Field(default=ProblemType.CONSTRAINT_SATISFACTION, description="Problem type") sense: OptimizationSense = Field(default=OptimizationSense.SATISFY, description="Optimization sense") objective: Optional[str] = Field(default=None, description="Objective function expression") # Solver options timeout: Optional[int] = Field(default=None, description="Timeout in milliseconds") random_seed: Optional[int] = Field(default=None, description="Random seed for reproducibility") def get_variables(self) -> List[BaseVariable]: """Get all variables in the problem.""" return self.variables def get_constraints(self) -> List[BaseConstraint]: """Get all constraints in the problem.""" return self.constraints def validate(self) -> bool: """Validate the problem definition.""" if not self.variables: return False if not self.constraints: return False # Check that all variable names are unique var_names = [var.name for var in self.variables] if len(var_names) != len(set(var_names)): return False return True
• constrained_opt_mcp/solvers/z3_solver.py:260-298 (helper)

  Core helper function implementing the Z3 solver logic: creates Z3 variables/constraints, solves with z3.Solver, extracts solution values.
  def solve_z3_problem(problem: Z3Problem) -> Result[Z3Solution, str]: """Orchestrates the complete process of solving a Z3 problem. Args: problem: The problem definition containing variables and constraints. Returns: Result: A Result containing either a Solution object or a failure with error details. """ try: # Validate problem if not problem.validate(): return Failure("Invalid problem definition") start_time = time.time() vars_result = create_variables(problem.variables) if isinstance(vars_result, Failure): return vars_result variables = vars_result.unwrap() constraints_result = create_constraints(problem.constraints, variables) if isinstance(constraints_result, Failure): return constraints_result z3_constraints = constraints_result.unwrap() solve_result = solve(variables, z3_constraints, problem.timeout) if isinstance(solve_result, Failure): return solve_result result_tuple = solve_result.unwrap() solve_time = time.time() - start_time return extract_solution(result_tuple[0], result_tuple[1], variables, solve_time) except Exception as e: return Failure(f"Error solving problem: {e!s}")
• constrained_opt_mcp/models/z3_models.py:28-54 (schema)

  Pydantic schema for Z3Variable defining variable types and bounds used in problems.
  class Z3Variable(BaseVariable): """Typed variable in a Z3 problem.""" name: str = Field(..., description="Variable name") type: Z3VariableType = Field(..., description="Z3 variable type") description: str = Field(default="", description="Variable description") # Z3-specific properties lower_bound: Optional[float] = Field(default=None, description="Lower bound") upper_bound: Optional[float] = Field(default=None, description="Upper bound") domain: Optional[List[Any]] = Field(default=None, description="Discrete domain values") def get_bounds(self) -> tuple[Optional[float], Optional[float]]: """Get variable bounds (lower, upper).""" return self.lower_bound, self.upper_bound def get_var_type(self) -> VariableType: """Convert to base variable type.""" mapping = { Z3VariableType.INTEGER: VariableType.INTEGER, Z3VariableType.REAL: VariableType.REAL, Z3VariableType.BOOLEAN: VariableType.BOOLEAN, Z3VariableType.STRING: VariableType.STRING, } return mapping[self.type]