solve_constraint_satisfaction
Find values that satisfy logical constraints for puzzles, reasoning, and optimization problems using Z3 SMT solver.
Instructions
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"
]
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| constraints | Yes | ||
| description | No | ||
| timeout | No | ||
| variables | Yes |
Input Schema (JSON Schema)
{
"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"
}