# Constraint Solving > Search over discrete choices in Sema with the native solve block — variables over finite domains, boolean constraints, first-solution or all-solutions. Sema's claim to be *neurosymbolic* rests on both halves being native. The neural half is `~=`, `semantics()`, and models; the symbolic half is the computer-algebra engine and — for **search over discrete choices** — a native finite-domain constraint solver. When a decision is "pick an assignment that satisfies these rules", you shouldn't hand-roll nested loops with early-exit flags. You declare the variables and constraints and let the runtime search. This guide covers the [`solve`](/language/control-flow/) block and grounds it in the [`crisis-logistics`](/reference/examples-api/crisis-logistics/) domain, where scarce resources must be assigned to incidents under hard rules. ## The `solve` block A `solve:` block declares variables over finite domains and constraints, and the runtime searches for a satisfying assignment, binding it into the enclosing scope: ```sema solve: var x in range(1, 10) var y in range(1, 10) constraint x + y == 10 constraint x < y # binds x = 1, y = 9 into the enclosing scope (the first solution) ``` - `var name in ` binds a variable ranging over any iterable domain — a `list` or a `range`. - `constraint ` is an ordinary boolean Sema expression over the variables. - `solve:` binds the **first** solution's variables into scope, raising `Unsatisfiable` if there is none. The solver is **backtracking search with forward checking** — a constraint is tested as soon as all its variables are bound, so the search prunes early instead of enumerating the full product of the domains. :::note The constraint expressions reuse the full evaluator, so *any* pure Sema expression — arithmetic, comparisons, and therefore any `equation` result — is a legal constraint. ::: ## All solutions Use `solve all:` to bind a `solutions` list of every satisfying assignment instead of just the first: ```sema solve all: # binds `solutions` = list[dict] of every model var a in range(1, 6) var b in range(1, 6) constraint a + b == 6 constraint a <= b # solutions == [{a:1,b:5}, {a:2,b:4}, {a:3,b:3}] ``` Each entry is a `dict` mapping variable names to their values, in solver order. :::caution[When there is no solution] `solve:` raises `Unsatisfiable` when no assignment satisfies every constraint. Wrap it in `expect … except Unsatisfiable:` (see [Error Handling](/language/error-handling/)) to fall back to a relaxed plan or an "unfilled" outcome rather than aborting. ::: ## A worked domain: assigning scarce resources The `crisis-logistics` example dispatches scarce resources — ambulances, rescue boats, generators — to incidents. Its `domain` models the pieces `solve` reasons over: ```sema enum ResourceKind: ambulance | rescue_boat | water_truck | generator | shelter_bed | drone | debris_team struct Resource: sem "A scarce deployable response resource" id: str kind: ResourceKind base: GeoPoint capacity: int available_epoch_s: i64 owning_agency: str invariant capacity >= 0 ``` Suppose you have three incidents and a pool of resource *slots*, and you must choose exactly one slot per incident such that no slot is used twice and total capacity is respected. That is a finite-domain search — a perfect fit for `solve`: ```sema def assign_slots(n_incidents: int, n_slots: int) -> None !{}: # Pick a distinct slot for each of three incidents from the available pool. solve: var i0 in range(0, n_slots) var i1 in range(0, n_slots) var i2 in range(0, n_slots) constraint i0 != i1 constraint i0 != i2 constraint i1 != i2 log.info("assignment", incident0=i0, incident1=i1, incident2=i2) ``` Because `constraint` expressions are ordinary Sema, you can express real rules — `constraint capacities[i0] >= demand0`, `constraint kind_of(i0) == ResourceKind.ambulance` — as long as every referenced variable is one of the `var` bindings or a value in scope. Forward checking rejects a partial assignment the moment a constraint over its bound variables fails, so an infeasible branch is pruned early. ### Solve, then verify semantically The power of a neurosymbolic language is that the symbolic result feeds the neural side and vice versa. Solve the *hard* combinatorial constraints with `solve`, then run the chosen plan through a `check semantics(…)` guard for the *soft* judgments a solver can't encode — as `crisis-logistics` does when it drafts and gates a public briefing built from the dispatch plan. The solver guarantees feasibility; the semantic guard guarantees the human-facing framing is safe. See [Semantic Operations](/neurosymbolic/semantic-operations/) and [Contracts](/neurosymbolic/contracts/). ## Run and verify From the `sema/` directory: ```bash sema check examples/crisis-logistics SEMA_STRICT=1 sema run examples/crisis-logistics sema assure examples/crisis-logistics --grade silver ``` `sema check` will flag a misplaced `var`/`constraint` line (outside a `solve` block it is an inert directive — a silent no-op the checker refuses to let pass). ## Variations - **Enumerate before you optimize.** Use `solve all:` to get every feasible plan, then rank them with a Sema expression (or a semantic score) and pick the best. - **Domains from data.** `var r in resources` ranges over a `list` you built at runtime — the domain need not be a `range`. - **Relax on failure.** Catch `Unsatisfiable`, drop the least-critical constraint, and re-solve — a common "best-effort dispatch" pattern. ## See also - [crisis-logistics example (generated)](/reference/examples-api/crisis-logistics/) - [Control Flow](/language/control-flow/) · [Error Handling](/language/error-handling/) - [Semantic Operations](/neurosymbolic/semantic-operations/) · [Contracts](/neurosymbolic/contracts/)