Constraint Solving

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 block and grounds it in the 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:

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 <domain> binds a variable ranging over any iterable domain — a list or a range.
• constraint <expr> 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:

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.

When there is no solution

solve: raises Unsatisfiable when no assignment satisfies every constraint. Wrap it in expect … except Unsatisfiable: (see 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:

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:

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 and Contracts.

Run and verify

From the sema/ directory:

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)
• Control Flow · Error Handling
• Semantic Operations · Contracts