USolver

Takes a structured problem definition and returns a solution using Z3 solver. Handles both satisfiability and optimization problems. Args: problem: Problem definition containing variables and constraints Returns: Solution results as TextContent list, including values and satisfiability status

A more direct way to solve Z3 problems without full model structure. Just provide variables and constraints as simple lists. Args: variables: List of dicts with 'name' and 'type' for each variable constraints: List of constraint expressions as strings description: Optional problem description Returns: Solution results as TextContent list

This tool takes a HiGHs optimization problem defined with variables, objective, and constraints, and returns a solution if one exists. HiGHs is a high-performance linear programming solver that supports: - Linear programming (LP) - Mixed-integer programming (MIP) - Both dense and sparse constraint matrices - Various solver algorithms (simplex, interior point, etc.) Example problem structure: { "problem": { "sense": "minimize", "objective": { "linear": [1.0, 2.0, 3.0] }, "variables": [ {"name": "x1", "lb": 0, "ub": 10, "type": "cont"}, {"name": "x2", "lb": 0, "ub": null, "type": "cont"}, {"name": "x3", "lb": 0, "ub": 1, "type": "bin"} ], "constraints": { "dense": [ [1, 1, 0], [0, 1, 1] ], "sense": ["<=", ">="], "rhs": [5, 3] } }, "options": { "time_limit": 60.0, "output_flag": false } } Args: problem: The HiGHs problem definition with variables, objective, and constraints Returns: A list of TextContent containing the solution or an error message

This tool provides a more straightforward interface for HiGHs problems, without requiring the full HiGHSProblem model structure. Args: sense: Optimization sense, either "minimize" or "maximize" objective_coeffs: List of objective function coefficients variables: List of variable definitions with optional bounds and types constraint_matrix: 2D list representing the constraint matrix (dense format) constraint_senses: List of constraint directions ("<=", ">=", "=") rhs_values: List of right-hand side values for constraints options: Optional solver options dictionary description: Optional description of the problem Returns: A list of TextContent containing the solution or an error message

This tool takes a CVXPY optimization problem defined with variables, objective, and constraints, and returns a solution if one exists. Example: Solve the following problem: minimize ||Ax - b||₂² subject to: 0 ≤ x ≤ 1 where A = [1.0, -0.5; 0.5, 2.0; 0.0, 1.0] and b = [2.0, 1.0, -1.0] Should be this tool call: simple_cvxpy_solver( variables=[{"name": "x", "shape": 2}], objective_type="minimize", objective_expr="cp.sum_squares(np.array(A) @ x - np.array(b))", constraints=["x >= 0", "x <= 1"], parameters={"A": [[1.0, -0.5], [0.5, 2.0], [0.0, 1.0]], "b": [2.0, 1.0, -1.0]} ) Args: problem: The problem definition with variables, objective, and constraints Returns: A list of TextContent containing the solution or an error message

This tool provides a more straightforward interface for CVXPY problems, without requiring the full CVXPYProblem model structure. Args: variables: List of variable definitions, each with 'name' and 'shape' objective_type: Either 'minimize' or 'maximize' objective_expr: The objective function expression as a string constraints: List of constraint expressions as strings parameters: Dictionary of parameter values (e.g., matrices A, b) description: Optional description of the problem Returns: A list of TextContent containing the solution or an error message

This tool takes a constraint programming problem defined with variables, constraints, and an optional objective, and returns a solution if one exists. Important Note: Each constraint expression must be a single evaluable Python statement. You cannot use Python control flow (loops, if statements) in the expressions. Instead, you need to generate separate constraints for each case. Example: Nurse Scheduling Problem: ```python # Schedule 4 nurses across 3 shifts over 3 days shifts_var = Variable( name="shifts_var", type=VariableType.BOOLEAN, shape=[4, 3, 3], # [nurses, days, shifts] description="Binary variable indicating if a nurse works a shift", ) constraints = [] # INCORRECT - This will fail: # Constraint( # expression=( # "for d in range(3): for s in range(3): " # "model.add(sum([shifts_var[n][d][s] for n in range(4)]) == 1)" # ) # ) # CORRECT - Add each constraint separately: # Each shift must have exactly one nurse for d in range(3): for s in range(3): constraints.append( Constraint( expression=f"model.add(sum([shifts_var[n][{d}][{s}] for n in range(4)]) == 1)", description=f"One nurse for day {d}, shift {s}", ) ) # Each nurse works at most one shift per day for n in range(4): for d in range(3): constraints.append( Constraint( expression=f"model.add(sum([shifts_var[{n}][{d}][s] for s in range(3)]) <= 1)", description=f"Max one shift for nurse {n} on day {d}", ) ) # Each nurse works 2-3 shifts total for n in range(4): constraints.append( Constraint( expression=f"model.add(sum([shifts_var[{n}][d][s] for d in range(3) for s in range(3)]) >= 2)", description=f"Min shifts for nurse {n}", ) ) problem = Problem( variables=[shifts_var], constraints=constraints, description="Hospital nurse scheduling problem", ) ``` Args: problem: The problem definition with variables, constraints, and optional objective Returns: A list of TextContent containing the solution or an error message