Solving and Results

Once your program is built, you ask clingo questions about it. The most common question is “what are the answer sets?”, which solve() answers with a stream of models that you read back as typed Python objects. This page covers that stream, how to read models, two questions you can ask about every answer set without listing them all (brave() and cautious()), optimization, and grounding a program once so that you can ask it many questions cheaply.

The model stream

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

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, which is a lazy stream of Model objects. Rendering and grounding happen right away when you call solve(), so any errors in your program show up there. Searching for models is lazy: clingo only computes the next model when you ask for it.

That means you should take only what you need. Use first() for one answer, itertools.islice for N of them, or a for-loop with a break when you’re looking for something in particular. Reading the whole stream (list(result), or a for-loop that runs to the end) computes every model, and an underconstrained program can have more answer sets than you could ever enumerate. This program has no choices, so it has exactly one answer set, and reading all of it is safe:

>>> 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 are final once the search ends, whether it ran to the end, you called close(), or you left a with block.

first() returns the first model and closes the search. If there are no models at all, it raises UnsatisfiableError. If having no answer set is a normal outcome for your program, use next(iter(result), None) instead, which gives you None rather than an exception.

Here’s a program with more than one answer set:

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() starts from scratch, so repeated solves never interfere with each other, and statements you add after a solve take effect on the next one. If you want to pay for grounding once and then solve many times, see Ground once, solve many.

Timeouts and interrupts

Everywhere on this page, timeout= is a wall-clock limit in seconds, counted from when the search starts. If a model stream times out after finding some models, it just ends: the models you already have are real answer sets, and exhausted stays False to tell you the search didn’t finish. If the timeout comes before any model was found, you get a SearchTimeoutError, because an empty stream would look like the program has no answer sets.

You can also stop a search from another thread (a stop button, say) by calling interrupt() on a grounding’s control. That works the same way: the stream ends quietly if you have models, with the result’s interrupted flag set, and raises SearchInterruptedError if you don’t. Both errors derive from SearchIncompleteError, so one except catches either. Neither one tells you anything about your program, unlike UnsatisfiableError.

Reading models

A Model holds the atoms of one answer set. atoms(Cls) returns the atoms of one predicate class as typed instances, atoms() with no argument returns all of them, and you can test membership (atom in model) and iterate as you’d expect. Fields come back as plain Python values: a str field is a real str, an int field is a real int, and a PredicateArg field gives you whichever of those the atom holds. The full story on field types is in Declaring predicates.

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

The other results on this page (the consequences from brave() and cautious(), and the Optimum from optimize()) are read exactly the same way.

Hidden atoms (from a show=False class that is never shown) are not read back into results at all, which is what keeps reading models fast. Asking for a hidden class raises an error, rather than returning an empty list that would look like nothing was 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.

atoms(Cls) looks up the exact class, so an in_namespace() clone counts as a different class. If your program uses classical negation, atoms(Cls) returns both the positive and negated atoms; filter on .negated to separate them.

Brave and cautious

There are 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() answers the first, and cautious() the second:

>>> possible = menu.brave()                             # true in AT LEAST ONE answer set
>>> sorted(atom.name for atom in possible.atoms(Chosen))
['a', 'b', 'c']
>>> possible.complete                                   # the search 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
[]

Clingo answers these questions by refining a guess: the brave answer grows until it covers every answer set, and the cautious answer shrinks. .path holds each of those steps, and .complete tells you whether the refinement finished. You can cap the work with timeout= (seconds) or max_iterations= (refinement steps), in which case you may get an incomplete answer, and you need to read it carefully:

  • An atom in an incomplete brave result is definitely possible. An atom that’s missing might still be possible.
  • An atom missing from an incomplete cautious result is definitely not certain. An atom that’s present might still turn out not to be.

Both raise UnsatisfiableError when the program has no answer sets.

If you want to watch the refinement step by step, brave_iter() and cautious_iter() on a grounding yield each step as it is found, so you can stop as soon as your question is answered. If the iteration runs to the end, the last step is the final answer. If it yields nothing, the program has no answer sets. A timeout raises SearchTimeoutError (and an interrupt raises SearchInterruptedError), so an unfinished refinement can never pass for a finished one.

On a program with an objective, all four of these refuse with an error, because clingo would refine over its search for the optimum rather than over the answer sets. Pass ignore_optimization=True to treat the program as if it had no objective (see Optimization).

Optimization

There are two ways to give a program an objective. minimize() and maximize() state one directly: a weight, the terms that make each contribution distinct, an optional condition=, and a priority= (higher priorities are optimized first). penalize() is a soft constraint: it reads like forbid(), but instead of ruling out each match, it adds weight to the cost. The two mean exactly the same thing to clingo, so pick whichever reads better: penalize() for “try to avoid this”, minimize() for “make this small”. Like forbid(), penalize() also works as a when() closer.

To solve for the best answer set, call optimize(). It returns an Optimum, which is a model that also carries its cost and whether it was proven optimal:

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                                    # clingo proved nothing is cheaper
True
>>> {atom.slot for atom in best.atoms(Assigned)}
{1}

cost has one entry per priority level, highest priority first. A maximize() objective is reported negated, so lower is always better.

Clingo finds the optimum by finding a model and then repeatedly looking for a cheaper one, and .path holds every model it found along the way. Each of those is a real answer set, which is what makes a capped search useful: if you set timeout= or max_iterations=, you get the best model found so far, with proven=False. SearchTimeoutError (or SearchInterruptedError) is only raised if the search stops before finding any model at all.

A few more options:

  • optimize(all_optima=True) keeps going after the optimum is proven, and collects every optimal model in .optima. When .complete is true, len(best.optima) == 1 tells you the optimum is unique.
  • strategy=OptStrategy.USC switches clingo to a different optimization algorithm. It can be much faster when the default one stalls, but it finds fewer intermediate models along the way.
  • bound= starts the search from a cost you already know is achievable. If you set it too tight, the result reads as unsatisfiable, because clingo can’t tell the difference.
  • optimize_iter(), on a grounding, yields each better model as it is found.

Plain solve() on a program with an objective refuses with an error, rather than quietly listing answer sets that 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 mentions two other ways to solve() a program with an objective. ignore_optimization=True lists answer sets as if there were no objective, for that one solve (it raises on a program that has no objective to ignore). cost_bound= keeps the objective, but uses it as a filter instead of a goal: you get every answer set whose cost is within the bound, best or not.

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

The models from a bounded solve each carry their cost:

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

Bounding at the cost optimize() proved gives you every model that is exactly as good as the optimum.

With one priority level, the bound is just an int. With several, pass a dict of {priority: value} covering the top priority, or the top two, and so on; the levels you leave out are unconstrained. Costs are compared the same way clingo ranks them: highest priority first, and a model that beats the bound at a higher priority is admitted no matter what it costs at lower ones. The bound is inclusive.

There are two things to watch out for. First, a bound that no model meets looks exactly like an unsatisfiable program. Second, because maximize() costs are negated, so is your bound: “every model achieving at least 4” is cost_bound=-4, not cost_bound=4 (which would admit everything).

If all you have is a budget, and no objective you want to optimize, then you don’t need any of this: the budget is just a constraint. Use a Sum with no objective at all:

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)

Plain solve() then lists every basket that fits the budget:

>>> 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

Every solve() on an ASPProgram grounds the program from scratch. If you want to ask one program lots of questions, ground() does the grounding once and returns a GroundedProgram. It’s a snapshot: it always solves the program as it was when you grounded it, even if you add more statements to the ASPProgram afterwards.

A grounding has all the verbs from this page (solve, brave, cautious, optimize), plus the step-by-step versions (brave_iter, cautious_iter, optimize_iter). Each of them takes assumptions=, which fix atoms for that one call: an atom is assumed true, and ~atom is assumed false.

>>> 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

ASPProgram.solve() and the other program-level verbs accept assumptions too. A grounding just makes asking lots of questions cheap, since it doesn’t ground again each time.

Solves on a grounding have to happen one at a time. Starting a new solve while a previous result is still open raises an error:

>>> 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

A grounding plus assumptions also covers a lot of what people use clingo’s incremental solving for. Full incremental solving (clingo’s #program parts) is not supported yet.

Unsat cores

When a solve with assumptions has no answer sets, clingo tells you which assumptions were to blame: a set of them that can’t all be true together. This is the unsat core, and it comes back on the exception as UnsatisfiableError.unsat_core, as the same objects you passed in:

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

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

A SolveResult also has an unsat_core. It is None until the search has proven there are no answer sets (and stays None for a satisfiable program), and () if the program has no answer sets even without any assumptions. The UnsatisfiableError raised by brave(), cautious() and optimize() carries one too. The core is guaranteed to contain a conflict, but it isn’t necessarily the smallest one.

Statistics and messages

Every result keeps a copy of clingo’s statistics from its search. .statistics is clingo’s own dict, plus a wall_time key, and format_statistics() prints it the way the clingo command line does. See clingo’s documentation for what the numbers mean.

Messages that clingo emits while solving never stop the search (stop_on_log_level only applies to parsing and grounding). They are collected on the result’s .messages, and on each model’s Model.messages. What these messages look like, and how they point back to your Python source, is covered in Clingo’s messages.

A note on scale

Reading models is built for puzzle-sized programs. It’s comfortable up to around 10^4 shown atoms per model, and gets slow somewhere in 10^5 to 10^6. If you have a lot of atoms, the fix is to show less: hidden atoms are never read back at all, so hundreds of thousands of intermediate atoms cost nothing once you hide() them. Show only what you actually use.