Solve
Find variable bindings that satisfy a set of constraints.
Concept
The Solve pragmatic performs Constraint Satisfaction (CSP) over entity domains. It allows you to find "who" or "what" fits a specific set of rules using variables (e.g., ?X).
Syntax
Solve for <variables> [such that <constraints>].
Example
Solve for ?X and ?Y such that
?X is a User
?Y is a Server
?X manages ?Y.
Constraint Rules (DS21)
The solver supports a specific subset of logic to ensure determinism and performance:
- Allowed: Conjunctions (AND) of atomic conditions.
- Allowed: Unary membership (
?X is a type) and Binary relations (?X relates to ?Y). - Rejected: Disjunctions (OR) inside constraints.
- Rejected: Negated constraints (
it is not the case that...).
Execution Model
1. Domain Propagation (AC-3)
Initial domains are established for each variable. Constraints reduce these domains iteratively (e.g., if ?X manages ?Y, then ?X must be in the set of managers).
2. Backtracking Search (v2)
Propagation alone guarantees local consistency but not global solutions. The solver performs a bounded backtracking search to find valid assignments for all variables simultaneously.
Reference
Defined in DS21 - Constraint Solving.