clingo.solve

Functions and classes related to solving.

Examples

The examples below show various ways to intercept models. The asynchronous variants leave room for additional computation before calling blocking functions like SolveHandle.get or SolveHandle.model.

The following example shows how to intercept models with a callback:

>>> from clingo.core import Library
>>> from clingo.control import Control
>>>
>>> lib = Library()
>>> ctl = Control(lib, ["0"])
>>> ctl.parse_string("1 { a; b } 1.")
>>> ctl.ground()
>>> with ctl.solve(on_model=print) as hnd:
...     print(hnd.get())
...
a
b
SAT

The following example shows how to yield models:

>>> from clingo.core import Library
>>> from clingo.control import Control
>>>
>>> lib = Library()
>>> ctl = Control(lib, ["0"])
>>> ctl.parse_string("1 { a; b } 1.")
>>> ctl.ground()
>>> with ctl.solve(yield_=True) as hnd:
...     for mdl in hnd:
...         print(mdl)
...     print(hnd.get())
...
a
b
SAT

The following example shows how to solve asynchronously:

>>> from clingo.core import Library
>>> from clingo.control import Control
>>>
>>> lib = Library()
>>> ctl = Control(lib, ["0"])
>>> ctl.parse_string("1 { a; b } 1.")
>>> ctl.ground()
>>> with ctl.solve(on_model=print, async_=True) as hnd:
...     print(hnd.get())
...
a
b
SAT

This example shows how to solve both iteratively and asynchronously:

>>> from clingo.core import Library
>>> from clingo.control import Control
>>>
>>> lib = Library()
>>> ctl = Control(lib, ["0"])
>>> ctl.parse_string("1 { a; b } 1.")
>>> ctl.ground()
>>> with ctl.solve(yield_=True, async_=True) as hnd:
...     while mdl := hnd.model():
...         print(mdl)
...         hnd.resume()
...     print(hnd.get())
...
b
a
SAT

class Model:

A view on the solver's current solution.

def contains(self, atom: clingo.symbol.Symbol) -> bool:

Check if the model contains the given atom.

Arguments:

atom: The atom to look up.

Returns:

Whether the atom is contained.

def extend(self, symbols: Sequence[clingo.symbol.Symbol]) -> None:

Extend a model with the given symbols.

This only has an effect if there is an underlying clingo application, which will print the added symbols.

Arguments:

symbols: The symbols to add to the model.

def is_consequence(self, literal: int) -> bool | None:

Check if the given program literal is a consequence.

The function returns True, False, or None if the literal is a consequence, not a consequence, or it is not yet known whether it is a consequence, respectively.

While enumerating cautious or brave consequences, there is partial information about which literals are consequences. The current state of a literal can be requested using this function. If this function is used during normal model enumeration, it simply returns whether the literal is true or false in the current model.

Arguments:

literal: The given program literal.

Returns:

Whether the given program literal is a consequence.

def is_true(self, literal: int) -> bool:

Check if the given program literal is true.

Arguments:

literal: The given program literal.

Returns:

Whether the given program literal is true.

def symbols( self, shown: bool = False, atoms: bool = False, terms: bool = False, theory: bool = False) -> Sequence[clingo.symbol.Symbol]:

Get the symbols in the model.

Arguments:

shown: Include shown atoms and terms.
atoms: Include all true atoms, including hidden ones.
terms: Include shown terms.
theory: Include terms added by external theories.

Returns:

A sequence of symbols present in the model.

control: SolveControl

Get the associated solve control object.

cost: Sequence[int]

Return a sequence of integer cost values of the model.

number: int

Get the running number of a model.

optimality_proven: bool

Whether the optimality of the model has been proven.

priorities: Sequence[int]

Get the associated priorities of the cost values.

thread_id: int

Get the thread/solver id the model was found in.

type: ModelType

Get the type of a model.

class ModelType:

Enumeration of model types.

ModelType(value: int)

BraveConsequences: ClassVar[ModelType] = ModelType.BraveConsequences

The model stores the set of brave consequences.

CautiousConsequences: ClassVar[ModelType] = ModelType.CautiousConsequences

The model stores the set of cautious consequences.

StableModel: ClassVar[ModelType] = ModelType.StableModel

The model captures a stable model.

name: str

value: int

class SolveControl:

A control object to add clauses while solving.

def add_clause(self, clause: Sequence[tuple[clingo.symbol.Symbol, bool] | int]) -> None:

Add a clause that applies to the current solving step during the search.

Arguments:

clause: The literals of the clause.

def add_nogood(self, nogood: Sequence[tuple[clingo.symbol.Symbol, bool] | int]) -> None:

Add a nogood that applies to the current solving step during the search.

Arguments:

nogood: The literals of the nogood.

base: clingo.base.Base

Get the atom/term bases of the program.

class SolveHandle:

An object to interact with a running search.

It can be used to control solving, like, retrieving models or cancelling a search.

A SolveHandle is a context manager and must be used with Python's with statement.

Blocking functions in this object release the GIL. They are not thread-safe though.

def cancel(self) -> None:

Cancel the running search.

def core(self) -> Sequence[int]:

Get the subset of assumptions that made the problem unsatisfiable.

def get(self) -> SolveResult:

Get the solve result.

This is always the last function to be called on a handle to ensure that the search is properly terminated. It might be preceded by a call to cancel to stop the search.

def last(self) -> Model | None:

Get the last computed model, if any.

If the search is not completed yet or the problem is unsatisfiable, the function returns None.

def model(self) -> Model | None:

Get the current model if there is any.

def resume(self) -> None:

Discards the last model and starts searching for the next one.

If the search has been started asynchronously, this function starts the search in the background.

def wait(self, timeout: typing.SupportsFloat | None = None) -> bool:

Wait for the solve call to finish or the next result with an optional timeout.

If a timeout is provided, the function blocks for the given duration or until a result is ready. A positive timeout blocks for that amount of time. A negative timeout blocks until a result is available, and a zero timeout allows polling for a result.

Arguments:

timeout: The maximum time to block in seconds.

Returns:

Whether the solve call has finished or the next result is ready.

class SolveResult:

A solve result captures information about a solve call.

exhausted: bool

Whether all models have been enumerated.

interrupted: bool

Whether the search was interrupted.

satisfiable: bool

Whether at least one model was found.

unknown: bool

Whether the satisfiablity could be determined.

unsatisfiable: bool

Whether there was no model.