Solving and Results

solve() is one call, but what it returns is a stream — and everything on this page follows from taking that seriously: how to consume models lazily and stop early, how to read typed atoms out of them, the two questions (brave(), cautious()) you can ask about every answer set without enumerating them, optimization with an honest anytime contract, and grounding once to ask one program many questions — assumptions in, unsat cores out. The one scale limit worth knowing in advance is at the end.

The model stream

The examples on this page need a program to solve. Here is a small one — the verbs are covered in Statements and Terms; if this is your first ASPAlchemy program, start with Your First Program instead.

from aspalchemy import ASPProgram, Field, Predicate, PredicateArg, Variable

class Person(Predicate):
    name: Field[PredicateArg]
    age: Field[PredicateArg]

class Adult(Predicate):
    name: Field[str]

X, Y = Variable("X"), Variable("Y")

program = ASPProgram()
program.fact(Person(name="john", age=30), Person(name="mary", age=25))
program.when(Person(name=X, age=Y), Y >= 18).derive(Adult(name=X))

solve() returns a SolveResult: a lazy, unbounded stream of Model objects. Rendering, grounding — instantiating every rule over the actual data, the step that turns your program into the solver’s input — and their error checks run eagerly at the call; only model enumeration is lazy — clasp, clingo’s search engine, computes the next model when you resume, so nothing runs ahead of your consumption. Take what you need: first() for one answer, itertools.islice for N, a for-loop with break for a condition. A whole-stream read (list(result), a bare for-loop) enumerates every model, which an underconstrained program can make effectively endless. This program has no choices, so it provably has exactly one answer set and enumerating it all is safe — and the exact transcript below is legitimate:

>>> result = program.solve()
>>> for model in result:
...     for adult in sorted(model.atoms(Adult), key=lambda atom: atom.render()):
...         print(adult)
adult("john")
adult("mary")
>>> result.satisfiable and result.exhausted and result.models_yielded == 1
True

satisfiable, exhausted, and models_yielded update as models arrive and finalize when iteration ends on any path — natural exhaustion, an explicit close(), or leaving a with-block. first() is the one-answer sugar: it returns the first model and closes the search, raising UnsatisfiableError when there is no model at all. If UNSAT is an expected outcome for your program, use next(iter(result), None) instead, which gives None rather than raising.

from itertools import islice
from aspalchemy import Choice

class Dish(Predicate, show=False):
    name: Field[str]

class Chosen(Predicate):
    name: Field[str]

N = Variable("N")
menu = ASPProgram()
menu.fact(*(Dish(name=n) for n in ["a", "b", "c"]))
menu.choose(Choice(Chosen(name=N), condition=Dish(name=N)) >= 1)

>>> result = menu.solve()
>>> some = list(islice(result, 2))   # take two models; the rest are never computed
>>> len(some), result.models_yielded, result.exhausted
(2, 2, False)
>>> result.close()                   # finalizes the flags and statistics
>>> len(list(menu.solve()))          # all non-empty subsets of three dishes
7

Every call to solve() renders and grounds a fresh clingo Control, so repeated solves on one program never interfere, and statements added after a solve take effect on the next call. (When you want to pay for grounding once and solve many times, see Ground once, solve many.)

The timeout contract, stated once here: everywhere on this page, timeout= is a wall-clock limit in seconds, counted from the start of iteration. On a model stream, timing out is quiet — the models found so far have already been yielded and exhausted stays False, since every yielded model was a true answer. A timeout before any model raises TimeoutError, because a silent empty stream would read as unsatisfiable. (Consequence refinements are stricter — see Brave and cautious.)

Reading models

Every result type on this page — Model, the consequences, Optimum — is an AtomCollection: one shared reading surface that makes no claim about what the atoms mean — only the subclass says that (a Model’s atoms are one answer set; a Consequences’ are a statement about every answer set). atoms(Cls) returns typed instances of one predicate class, atoms() with no argument returns everything, membership (atom in model) and iteration work as you’d expect. Reads are plain Python: a str field comes back as a real str, an int field as a real int, and a polymorphic (PredicateArg) slot the same way — the full field contract lives in Declaring predicates.

>>> model = program.solve().first()
>>> sorted(adult.name for adult in model.atoms(Adult))   # typed instances, plain str fields
['john', 'mary']
>>> {type(person.age) for person in model.atoms(Person)}
{<class 'int'>}

Hidden atoms (show=False and never shown) are never read back into results at all — skipping them is what keeps model reads fast — so asking for a hidden class raises with the remedy instead of returning an [] that would read as “none were derived”:

>>> menu.solve().first().atoms(Dish)      # Dish is show=False
Traceback (most recent call last):
  ...
ValueError: dish/1 is hidden (show=False and never shown): hidden atoms are not read back into results ... show() the class, or define it with show=True, to read it.

Lookup is by exact class (an in_namespace() clone is a distinct class), and both signs of a classically negated predicate come back from the same atoms(Cls) call — filter on .negated if your program uses classical negation.

Brave and cautious

Two questions you can ask without enumerating every model: what is possible — true in at least one answer set — and what is certain — true in every answer set. brave() computes the union of all answer sets, cautious() the intersection; each returns eagerly:

>>> possible = menu.brave()                             # true in AT LEAST ONE answer set
>>> sorted(atom.name for atom in possible.atoms(Chosen))
['a', 'b', 'c']
>>> possible.complete                                   # a PROOF the refinement finished
True
>>> certain = menu.cautious()                           # true in EVERY answer set
>>> certain.complete
True
>>> certain.atoms(Chosen)   # something must be chosen, but no one item is forced
[]

BraveConsequences and CautiousConsequences carry their evidence: .path holds every successive approximation clasp computed (brave grows toward the union, cautious shrinks toward the intersection), and .complete is a proof of exhaustion, not a guess. A bounded run — timeout= seconds or max_iterations= refinement steps — returns an incomplete result whose knowledge is one-sided: every atom a partial brave result contains is certified possible (absence proves nothing yet), and every atom a partial cautious result lacks is certified not-forced (presence proves nothing yet). Both eager verbs raise UnsatisfiableError when the program has no answer set, carrying the unsat core and the solve’s messages.

For stepwise control, brave_iter()/cautious_iter() on a grounding return RefinementSteps: iterate for successive approximations and stop the moment your question is answered — each step is a full solver search, so control between steps is control over real work. Iteration ending naturally means the last approximation is the true union/intersection; zero yields means unsatisfiable; and a timeout raises TimeoutError from within iteration, so a timed-out refinement can never impersonate a completed one.

On an optimizing program, all four verbs refuse with a teaching error: the refinement would be computed against the solver’s cost-descent path, not the set of answer sets. Pass ignore_optimization=True to refine over all answer sets as if there were no objective (see Optimization, which owns that switch).

Optimization

Objectives enter the program two ways. minimize()/maximize() state an objective directly: a weight, the tuple terms that make each contribution distinct, an optional condition=, and a priority= tier (higher tiers dominate lower ones lexicographically). penalize() is the soft-constraint spelling — a forbid() that charges instead of forbidding: each ground match of the conditions adds weight to the cost, rendered as a weak constraint (:~ ... [w@p, terms]). The two are semantically identical, so the spelling is intent: penalize() for soft constraints, minimize() for objectives. penalize() also works as a when() closer, like forbid().

Solving an objective is optimize(), which returns the best answer set as an Optimum — a model carrying its cost and its certificate:

class Task(Predicate, show=False):
    name: Field[str]

class Slot(Predicate, show=False):
    n: Field[int]

class Assigned(Predicate):
    task: Field[str]
    slot: Field[int]

T, S = Variable("T"), Variable("S")
chores = ASPProgram()
chores.fact(*(Task(name=t) for t in ["wash", "dry", "fold"]))
chores.fact(*(Slot(n=s) for s in [1, 2, 3]))
chores.when(Task(name=T)).derive(
    Choice(Assigned(task=T, slot=S), condition=Slot(n=S)) == 1
)
chores.penalize(Assigned(task=T, slot=S), weight=S, terms=[T])  # earlier slots are cheaper

best = chores.optimize()

>>> best.cost                                      # all three tasks land in slot 1
(3,)
>>> best.proven                                    # optimality was PROVED, not assumed
True
>>> {atom.slot for atom in best.atoms(Assigned)}
{1}

cost has one entry per surviving priority level, highest first (a maximization’s cost is reported negated — lower is better in every sense). .path holds every emission of the descent, each a genuine answer set — so an interrupted search’s best is still a real solution: a timeout= or max_iterations= cap returns the best model found so far with proven=False, the anytime reading, and TimeoutError fires only when the deadline lands before any model at all. optimize(all_optima=True) continues past the optimality proof and collects every certified optimum in .optima (with .complete true, len(optimum.optima) == 1 answers uniqueness). strategy=OptStrategy.USC swaps clasp’s algorithm — often dramatically faster when branch and bound stalls, at the price of a sparse emission stream — and bound= starts the search from a known cost, with the caveat that a too-tight bound is reported as unsatisfiable (clasp cannot tell the difference). The stepwise form, optimize_iter(), lives on a grounding you keep and yields each strictly-better CostedModel as it is found.

Plain solve() on an optimizing program refuses with a teaching error, rather than silently enumerating answer sets the objective was supposed to rank:

>>> chores.solve()
Traceback (most recent call last):
  ...
ValueError: This program optimizes (#minimize/#maximize present). Solve it with optimize(); or pass cost_bound= to enumerate every answer set within a cost; or pass ignore_optimization=True to enumerate as if there were no objective.
>>> len(list(chores.solve(ignore_optimization=True)))   # three slots per task, objective ignored
27

The error names the two other things an objective can do for a solve(). ignore_optimization=True (clasp’s opt-mode=ignore) enumerates answer sets as if the program had no objective, for that solve only — and it requires an objective to ignore, raising on a program without one rather than passing vacuously. cost_bound= keeps the objective but demotes it from a goal to an admission rule: every answer set whose cost is within the bound streams back, best or not, and nothing is optimized.

>>> len(list(chores.solve(cost_bound=4)))       # the optimum costs 3; one step of slack admits 4 models
4
>>> sorted(atom.slot for atom in chores.solve(cost_bound=3).first().atoms(Assigned))
[1, 1, 1]

Every admitted model carries the price clasp computed for it: bounded solves yield CostedModels, one cost entry per surviving tier, never proven — nothing was optimized:

>>> sorted(model.cost for model in chores.solve(cost_bound=4))
[(3,), (4,), (4,), (4,)]

The bound is clasp’s own rule, lexicographic and inclusive: tiers are compared from the dominant one down, and a model that beats a tier’s bound is admitted no matter what the lower tiers cost — it is not “each tier within its budget” (the receipt for that distinction lives in the test suite). It takes the same shapes as optimize(bound=): a bare int when one tier survived grounding, otherwise {priority: value} naming a dominant-first prefix of the surviving levels (optimization_levels) — the first tier, the first two, or all of them, with tiers below the prefix unconstrained (bound only the dominant tier and every tie is admitted whatever the lower tiers cost; a lower tier without every tier above it refuses, because that shape has no lexicographic meaning). Unlike optimize(bound=), which is a pruning hint that cannot change the answer, an enumeration bound decides which answer sets you get, so it is validated strictly rather than best-effort — and, same honest caveat as the hint: a bound nothing meets reads as unsatisfiable, because clasp cannot tell the difference. One sign trap, inherited from clasp: a maximize() objective is compiled as negated minimization, so its costs — and therefore your bound — live in negated space, exactly as optimize() reports them: “every model achieving at least 4” is cost_bound=-4 (the naive +4 bounds nothing, since every negated cost is already below it — the receipt is in the test suite). The two compose: bound a solve at an optimize()’s proven cost and you enumerate every model exactly as good as the one it proved.

A budget on a single measure needs none of this. When the budget is the whole question — not a bound on an objective you also care to optimize — it is a hard constraint, and a Sum guard with no objective at all is the sharper tool:

from aspalchemy import ANY, Sum

class Item(Predicate, show=False):
    """An available item and what it costs."""
    name: Field[str]
    cost: Field[int]

class Picked(Predicate):
    """The solver put this item in the basket."""
    name: Field[str]

item_costs = {"anchovies": 1, "basil": 2, "capers": 3}
BUDGET = 3

pantry = ASPProgram()
pantry.fact(*(Item(name=n, cost=c) for n, c in item_costs.items()))

N, C = Variable("N"), Variable("C")
pantry.choose(Choice(Picked(name=N), condition=Item(name=N, cost=ANY)))

# The budget is a hard constraint, not an objective:
pantry.forbid(Sum((C, N), condition=[Picked(name=N), Item(name=N, cost=C)]) > BUDGET)

No #minimize, nothing for a bound to price — plain solve() enumerates every basket inside the budget, and only those:

>>> baskets = {frozenset(a.name for a in model.atoms(Picked)) for model in pantry.solve()}
>>> sorted(sorted(basket) for basket in baskets)
[[], ['anchovies'], ['anchovies', 'basil'], ['basil'], ['capers']]

Ground once, solve many

ground() renders and grounds the program once and returns a GroundedProgram: an independent, immutable snapshot that solves exactly that program forever, unaffected by later mutation of the ASPProgram it came from — like a compiled regex and its pattern. Every verb above lives on it (solve, brave, cautious, optimize), each eager verb has a lazy twin (brave_iter, cautious_iter, optimize_iter — the findall/finditer pairing), and assumptions parameterize any of them per call: a grounded atom assumes it true, ~atom assumes it false, for that solve only.

>>> grounding = menu.ground()       # grounding is paid once
>>> len(list(grounding.solve()))
7
>>> len(list(grounding.solve(assumptions=[Chosen(name="a")])))    # the subsets containing "a"
4
>>> len(list(grounding.solve(assumptions=[~Chosen(name="a")])))   # the non-empty subsets of {"b", "c"}
3

Assumptions are also accepted directly by ASPProgram.solve() and the other program-level verbs — the grounding is not what enables them, it is just where asking many questions of one program gets cheap, since each program-level call re-grounds from scratch.

One contract, enforced loudly: solves on a grounding are sequential. A Control cannot run overlapping searches, so starting a new solve while a previous result is unconsumed raises instead of silently corrupting either:

>>> open_result = grounding.solve()
>>> grounding.solve()
Traceback (most recent call last):
  ...
RuntimeError: The previous solve on this grounding is still open; a Control cannot run overlapping searches. Consume the previous result, close() it, leave its with-block, or call abandon() on this grounding.
>>> open_result.close()                 # or consume it, or leave its with-block
>>> len(list(grounding.solve()))        # the snapshot solves the same program forever
7

ground() + assumptions is also the interim answer to incremental solving: true multi-shot (clingo’s #program parts) is honestly a future design project.

Unsat cores

When a solve under assumptions comes back UNSAT, the search leaves evidence: the set of assumptions clasp reports as jointly unsatisfiable. It rides the exception as UnsatisfiableError.unsat_core, in the shapes the assumptions were given:

from aspalchemy import UnsatisfiableError

class Guest(Predicate, show=False):
    name: Field[str]

class Invited(Predicate):
    name: Field[str]

G = Variable("G")
party = ASPProgram()
party.fact(*(Guest(name=g) for g in ["alice", "bob", "cara"]))
party.choose(Choice(Invited(name=G), condition=Guest(name=G)))
party.forbid(Invited(name="alice"), Invited(name="bob"))    # rivals

rivals = [Invited(name="alice"), Invited(name="bob")]
core = None
try:
    party.ground().solve(assumptions=rivals).first()
except UnsatisfiableError as e:
    core = e.unsat_core          # the evidence rides the exception

assert core and set(core) <= set(rivals)

The same evidence is available as SolveResult.unsat_core once a search has proven unsatisfiability (None before then and for satisfiable programs; () when UNSAT needed no assumptions at all), and the eager verbs — cautious(), brave(), optimize() — carry it on their UnsatisfiableError too. It is a core, not necessarily a minimal one: clasp promises it contains a conflict, nothing more. A core only exists relative to assumptions — which is why this section lives beside the grounding story, where assumption-driven questioning is the workflow.

Statistics and messages

Every search handle snapshots clingo’s statistics as it finishes: .statistics is the raw dict (a copy, plus a wall_time key spanning the handle’s creation to the end of iteration), and format_statistics() renders it in clingo’s native output style. The eager results (Optimum, the consequences) carry the same snapshot, so nothing is lost by not using the _iter twin. (There is nothing to show that clingo’s own documentation doesn’t own: .statistics is clingo’s dict, passed through.)

Clingo’s own statistics reflect the most recent search on the shared Control — snapshotting at finish is what makes each handle’s numbers its own. Diagnostics emitted during the solve phase never halt solving (the stop_on_log_level threshold applies to parsing and grounding only); they are captured on the handle’s .messages and, per model, on Model.messages. What the messages look like, and how grounding diagnostics map back to your Python source, is covered in Clingo’s messages.

A note on scale

An honest note: the model-read path is tuned for puzzle-sized models. Atom equality goes through rendering and membership checks are linear scans, so reading models is comfortable at 10^4 atoms and will hurt at 10^5–10^6. The one lever that matters is visibility: hidden atoms are never read back at all — hundreds of thousands of scaffolding atoms cost nothing if you hide() them — so show only what you actually consume.