propagator

ConstraintHandlerPropagator

Bases: Propagator

Propagator that evaluates constraint_handler variables during solving.

The propagator maintains a mapping from clingo symbols and solver literals to variable objects (see constraint_handler.PropagatorVariables). During propagation/check it evaluates affected variables, checks ensure constraints, and can add nogoods for conflicts or for pruning based on optimization or reasoning mode(brave/cautious).

Attributes:

Name	Type	Description
symbol2var	VariableManager	Maps variable symbols to variable objects.
literal2var	dict[int, list[VariableType]]	Maps solver literals to variable objects.
evaluatevars	list[EvaluateVariable]	List of EvaluateVariable instances to evaluate.
optimization_sum	OptimizationHandler	Optimization handler tracking objective sums.
best_value	list[int | float]	Current best objective optimization vector.
using_optimization	bool	Whether optimization is active.
optimization_strength	OptimizationStrength	Whether equal quality solutions are allowed when optimizing.
environment	ImmutableList[constant]	Evaluation environment built from solver identifier.
check_only		If True, propagate becomes a no-op. Will only evaluate variables in check.
errors	propagator_warning_t	Warnings collected while evaluating variables or reading the input program.
reasoning_mode	ReasoningMode	STANDARD/BRAVE/CAUTIOUS mode.
python_model	set[ResultAtom] | None	Stores the python-level model for output.

__init__

__init__()

Initialize the propagator.

Parameters:

Name	Type	Description	Default
check_only		If True, do not perform propagation (only allow checks).	required

add_nogood_for_variable

add_nogood_for_variable(ctl: PropagateControl, var: VariableType | OptimizationHandler, extra_literals: Iterable[int] | None = None, conflict: bool = True) -> bool

Add a nogood blocking the current assignment for a variable.

The nogood is constructed from the literals that explain the variable's current value.

It is also possible to include extra literals that should be added to the nogood (e.g. to block only for the current optimization stage).

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
var	VariableType | OptimizationHandler	Variable (or optimization handler) to block.	required
extra_literals	Iterable[int] | None	Additional literals to include in the nogood.	None
conflict	bool	Whether to treat the nogood as a conflict.	True

Returns: bool: True if propagation must stop False otherwise Raises: AssertionError: If we expected the nogood to be a conflict but the solver did not detect it

add_nogoods_from_queue

add_nogoods_from_queue(ctl: PropagateControl) -> bool

Add queued nogoods until the queue is empty or clingo refuses one.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required

Returns:

Name	Type	Description
bool	bool	True if adding a nogood failed (propagation must stop).

add_optimization_helper_atoms

add_optimization_helper_atoms(ctl: PropagateInit) -> None

Register helper literals for optimization pruning.

If optimization is used, the encoding provides an atom that is true when we are still finding the optimal value and adds nogoods to prune worse solution than the current one. Then, we disable this atom and look for solutions with the SAME value so we find all optimal solutions Args: ctl: Clingo PropagateInit object.

add_reasoning_mode_helper_atoms

add_reasoning_mode_helper_atoms(ctl: PropagateInit) -> None

Register helper literals for brave/cautious reasoning.

In brave/cautious mode, the encoding provides stage atoms that separate (1) clingo reasoning for solver-handled variables and (2) propagator-side evaluation.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

add_shared_values

add_shared_values(model: Model)

Add optimization value atoms for optimization sums to the model. This uses the post_processor.py "_extend_optimize_values" function.

Parameters:

Name	Type	Description	Default
model	Model	Clingo model to extend.	required

add_watch

add_watch(lit: int) -> None

Add a watch literal to the set of watched literals if check_only is disabled

Parameters:

Name	Type	Description	Default
lit	int	Literal to watch.	required

add_watches_to_ctl

add_watches_to_ctl(ctl: PropagateInit) -> None

Register all watch literals

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

apply_preprocessing

apply_preprocessing(valuations: dict[Symbol, set[Any]], init: PropagateInit) -> None

Apply the preprocessed valuations to the propagator's variables.

Parameters:

Name	Type	Description	Default
valuations	dict[Symbol, set[Any]]	A dictionary mapping variable symbols to their possible values.	required

backward_prune

backward_prune(valuations: dict[Symbol, set[Any]], evaluation_order: list[Symbol]) -> bool

Prune the valuations of variables based on their dependencies.

Parameters:

Name	Type	Description	Default
valuations	dict[Symbol, set[Any]]	Current valuations of variables.	required
evaluation_order	list[Symbol]	Order in which variables were evaluated.	required

Returns:

Name	Type	Description
bool	bool	True if any valuations were pruned, False otherwise.

check

check(control: PropagateControl) -> None

Perform a full consistency check using the current solver assignment.

This evaluates all variables, checks ensure constraints and forbidden warnings, and applies optimization pruning by adding nogoods when necessary.

Parameters:

Name	Type	Description	Default
control	PropagateControl	Clingo PropagateControl object.	required

check_ensures

check_ensures(valuations: dict[Symbol, set[Any]]) -> dict[Symbol, set[Any]]

Check ensure constraints for all variables and update their possible values.

Parameters:

Name	Type	Description	Default
valuations	dict[Symbol, set[Any]]	Current valuations of variables.	required

check_evaluate

check_evaluate(ctl: PropagateControl)

Evaluate evaluate atoms against the current assignments.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required

check_shared_values

check_shared_values(ctl: PropagateControl)

Evaluate evaluate atoms against the current assignments.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required

check_total

check_total(control: PropagateControl) -> None

Handle a total assignment.

This evaluates evaluate atoms, updates the python-side model for brave/cautious reasoning, and updates the incumbent objective value.

Parameters:

Name	Type	Description	Default
control	PropagateControl	Clingo PropagateControl object.	required

ensure_pairs

ensure_pairs(valuations: dict[Symbol, set[Any]]) -> dict[EnsureVariable, dict[Symbol, dict[Any, set[Any]]]]

Return a dictionary mapping ensure to a list of dicts X

Only works with ensure with 2 variables

A dict X maps a symbol, that is a variable used in the ensure, to a dict of possible values for that variable and the possible values for the other variable in the ensure that can work with the first variable's value. E.g. d["ensure_1"] = { "var1": { 1: [2,3], 2: [3,4] }, "var2": { 2: [1], 3: [1,2], 4: [2] } }

evaluate_model

evaluate_model(ctl: PropagateControl) -> bool

Update and (if needed) refine the accumulated python model.

In STANDARD mode this only rebuilds the python model and never backtracks. In BRAVE/CAUTIOUS mode, the model is accumulated across models and nogoods may be enqueued to force progress between stages.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo propagation control.	required

Returns:

Name	Type	Description
bool	bool	True if nogoods were added and propagation should stop.

evaluate_optimization_sum

evaluate_optimization_sum(ctl: PropagateControl) -> bool

Evaluate the current objective value and optionally prune.

If the objective is already worse than the incumbent and the relevant parts are fully assigned, a nogood is added to exclude the current partial/total assignment.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo propagation control.	required

Returns:

Name	Type	Description
bool	bool	True if a nogood was added requiring a backtrack.

evaluate_variable

evaluate_variable(ctl: PropagateControl, var: VariableType, expr_lits: set[int] | None = None) -> bool | None

Evaluate one variable against the current assignment.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
var	VariableType	Variable to evaluate.	required

Returns:

Type	Description
bool | None	bool | None: - True if the variable's value changed. - False if it did not change. - None if evaluation detected a conflict (nogood added).

evaluated_solver_assignment

evaluated_solver_assignment(ctl: PropagateControl, to_evaluate: dict[VariableType, set[int] | None]) -> bool

Evaluate a set of variables under the current solver assignment.

If a variable changes, its parents are scheduled for evaluation.

Parameters:

Name	Type	Description	Default
ctl	PropagateControl	Clingo PropagateControl object.	required
to_evaluate	dict[VariableType, set[int] | None]	Variables that may have been affected by recent changes.	required

Returns:

Name	Type	Description
bool	bool	True if propagation should stop (conflict/forbidden warning),
	bool	False otherwise.

forward_prune

forward_prune(valuations: dict[Symbol, set[Any]], evaluation_order: list[Symbol]) -> bool

Forward prune the valuations of variables based on their dependencies.

This is useful when during backward pruning a variable's domain is reduced, which may allow for further pruning of dependent variables. E.g. y = x+1, z = x-1 x domain is {1,2,3} y domain is {2,3,4} z domain is {0,1,2} due to an ensure, y domain is now {2,3} backward pruning will reduce x domain to {1,2} now forward pruning will reduce z domain to {0,1} since x can only be 1 or 2.

Parameters:

Name	Type	Description	Default
valuations	dict[Symbol, set[Any]]	Current valuations of variables.	required
evaluation_order	list[Symbol]	Order in which variables were evaluated.	required

Returns:

Name	Type	Description
bool	bool	True if any valuations were pruned, False otherwise.

get_configuration

get_configuration(ctl: Control)

Read clingo configuration and initialize reasoning-mode settings.

For brave/cautious modes, this configures the solver heuristic and adds a helper program to facilitate the reasoning stages.

Parameters:

Name	Type	Description	Default
ctl	Control	Clingo control instance.	required

get_engine_variables

get_engine_variables(ctl: PropagateInit)

Load atoms that represent the values of variables from the input program.

This reads _se_value, _set_contains, and Multimap_value atoms and updates the corresponding variables with the assigned values. This is used for variables whose values are defined by other engines

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_ensure

get_ensure(ctl: PropagateInit)

Load ensure constraints from ASP facts and create EnsureVariable instances.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_evaluate

get_evaluate(ctl: PropagateInit)

Load evaluate atoms into EvaluateVariable instances. Also load "bool_evaluate" atoms and create the corresponding variables.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_forbidden_warnings

get_forbidden_warnings(ctl: PropagateInit) -> None

Load warning_forbid atoms.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo propagation initializer.	required

get_multimap_declarations

get_multimap_declarations(ctl: PropagateInit)

Load multimap (dict) declarations and assignments from ASP facts.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_optimization_sums

get_optimization_sums(ctl: PropagateInit)

Load optimization sum declarations from ASP facts and create OptimizationSum instances.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_reasoning_mode_nogoods

get_reasoning_mode_nogoods(variables: set[ResultAtom], first_call: bool) -> list[Iterable[int]]

Create nogoods used to drive brave/cautious reasoning.

• BRAVE: force the next model to differ in at least one variable so the accumulated model can grow.
• CAUTIOUS: on first call behaves like brave; on subsequent calls, block exactly the changes observed to converge to the intersection.

Parameters:

Name	Type	Description	Default
variables	set[ResultAtom]	Result atoms relevant for the current step.	required
first_call	bool	Whether this is the first stage-2 call for the run.	required

Returns:

Type	Description
list[Iterable[int]]	list[Iterable[int]]: Nogoods to add (each is a collection of solver literals).

get_reasons

get_reasons(var: VariableType | OptimizationHandler, seen: set[VariableType] | None = None) -> set[int]

Compute the set of literals explaining a variable's current value.

This is used when constructing nogoods for conflicts, forbidden warnings, and optimization pruning.

Parameters:

Name	Type	Description	Default
var	VariableType | OptimizationHandler	Variable whose reasons should be collected.	required

Returns:

Type	Description
set[int]	set[int]: Set of signed solver literals.

get_set_declarations

get_set_declarations(ctl: PropagateInit)

Load set declarations and assignments from ASP facts.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo propagation initializer.	required

get_shared_values

get_shared_values(ctl: PropagateInit)

Load shared value declarations from ASP facts and create SharedValueVariable instances.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_solver_identifier

get_solver_identifier(ctl: PropagateInit)

Initialize the Python evaluation environment using the solver identifier.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

get_variable_ranks

get_variable_ranks() -> None

Variable get a rank based on rank of dependencies

get_variables

get_variables(ctl: PropagateInit)

Load base variable declarations/definitions/domains from ASP facts.

Reads variable-related atoms and creates/extends Variable instances. Note that nogoods are added to prevent True assignments to values that are parts of domains that are assigned False.

Parameters:

Name	Type	Description	Default
ctl	PropagateInit	Clingo PropagateInit object.	required

handle_on_model_dict

handle_on_model_dict(var: Symbol, final_value: dict)

Add atoms for a dict/multimap-typed variable to the python model.

Parameters:

Name	Type	Description	Default
var	Symbol	Variable symbol.	required
final_value	dict	Mapping value (may be a multimap.Multimap).	required

handle_on_model_normal_type

handle_on_model_normal_type(var: Symbol, final_value: bool | float | str | Symbol | tuple[Any, ...])

Add atoms for a variable (bool/int/float/string/symbol) to the python model.

Parameters:

Name	Type	Description	Default
var	Symbol	Variable symbol.	required
final_value	bool | float | str | Symbol | tuple[Any, ...]	Scalar value.	required

handle_on_model_set

handle_on_model_set(var: Symbol, final_value: set | frozenset)

Add atoms for a set-typed variable to the python model.

Parameters:

Name	Type	Description	Default
var	Symbol	Variable symbol.	required
final_value	set | frozenset	Set/frozenset value.	required

handle_on_model_value

handle_on_model_value(var: Symbol, final_value: Any)

Dispatch model export based on the final value type.

Parameters:

Name	Type	Description	Default
var	Symbol	Variable symbol.	required
final_value	Any	Evaluated value for the variable.	required

handle_on_model_warning

handle_on_model_warning(errors: propagator_warning_t)

Add warning atoms to the python model.

Parameters:

Name	Type	Description	Default
errors	propagator_warning_t	Iterable of warning atoms.	required

infer_domain

infer_domain(valuations: dict[Symbol, set[Any]], eval_order: list[Symbol]) -> None

Loop over all variables and calculate domains for the ones that have all dependencies known. This function must be called repeatedly to do get the domain for all variables.

Parameters:

Name	Type	Description	Default
valuations	dict[Symbol, set[Any]]	Current valuations of variables. This is modified in-place to add new possible values for variables.	required
eval_order	list[Symbol]	List of variable symbols in the order they were evaluated. This is modified in-place to add new variables that were evaluated.	required

init

init(init: PropagateInit) -> None

Function implementing the init method of a Propagator. See clingo Propagator documentation for more details.

Parameters:

Name	Type	Description	Default
init	PropagateInit	Clingo PropagateInit object	required

on_model

on_model(model: Model)

Extend the clingo model using python-side result atoms.

Parameters:

Name	Type	Description	Default
model	Model	Current clingo model.	required

preprocess

preprocess(cycles: int = -1) -> dict[Symbol, set[Any]]

Preprocess the propagator before solving.

This finds the possible domains for all variables, checks the ensures to see which ones are the possible ones and prunes the variables based on their ability to be used in variables that depend on them.

Returns:

Type	Description
dict[Symbol, set[Any]]	dict[Symbol, set[Any]]: A dictionary mapping variable symbols to their possible values.

preprocess_variable

preprocess_variable(valuations: dict[Symbol, set[Any]], var: Symbol, current_vars: set[Symbol]) -> bool

Preprocess a single variable to calculate its possible domain.

Parameters:

Name	Type	Description	Default
valuations	dict[Symbol, set[Any]]	Current valuations of variables.	required
var	Symbol	The variable symbol to preprocess.	required
current_vars	set[Symbol]	Set of variable symbols that can contain the dependencies of the variable being preprocessed.	required

Returns:

Name	Type	Description
bool	bool	True if the variable was preprocessed, False if var does not exist or is already in valuations.

propagate

propagate(control: PropagateControl, changes: Sequence[int]) -> None

Propagate after a solver assignment change. Checks which variables are affected by the change, evaluates them, and applies optimization pruning if enabled.

Parameters:

Name	Type	Description	Default
control	PropagateControl	Clingo propagation control.	required
changes	Sequence[int]	Sequence of (signed) solver literals that changed.	required

set_optimization_best_value

set_optimization_best_value(value: list[int | float]) -> None

Set the best (incumbent) optimization value used for pruning.

Parameters:

Name	Type	Description	Default
value	list[int | float]	Objective vector ordered by priority.	required

set_optimization_check_strength

set_optimization_check_strength(strength: Literal['lt', 'le']) -> None

Configure whether optimization pruning requires strict improvement.

Parameters:

Name	Type	Description	Default
strength	Literal['lt', 'le']	Comparison mode. - "lt": only strictly better solutions are accepted. - "le": better or equal solutions are accepted.	required

Raises:

Type	Description
ValueError	If strength is not one of "lt" or "le".

set_parents

set_parents()

Populate parent relationships between variables.

Parents are variables that depend on another variable's value; if a child changes, parents are scheduled for re-evaluation.

undo

undo(thread_id: int, assignment: Assignment, changes: Sequence[int]) -> None

Undo propagator state on backtracking.

This resets variable evaluations whose decision level is higher or equal to the current backtracking level and clears derived optimization state.

Parameters:

Name	Type	Description	Default
thread_id	int	Clingo thread id (unused).	required
assignment	Assignment	Current assignment after backtracking.	required
changes	Sequence[int]	Literals undone by clingo.	required

update_python_model

update_python_model()

Build the python-side model representation from current variable values.

Populates self.python_model with result atoms (values, sets, multimaps, evaluated atoms) and warning atoms. This is used by on_model to extend the clingo model and by brave/cautious reasoning to accumulate results.