Multishot Application

Control structure for the multi-shot encoding to solve instances with unbounded cardinalities.

coomsuite.bounds.multi_application.COOMMultiSolverApp

Bases: COOMSolverApp

Application class for multi-shot solving extending the standard COOM application class

__init__(serialized_facts: List[str], algorithm: str = 'linear', initial_bound: int = 0, step: Optional[int] = 1, base: Optional[float] = 2.0, log_level: str = '', options: Optional[Dict[str, Any]] = None, istest: bool = False)

main(control: Control, files: Sequence[str]) -> None

Main function of the multishot application class

After returning the attribute max_bound is the minimal bound for which the instance is satisfiable.

Parameters:

Name	Type	Description	Default
control	Control	the clingo control object	required

Extending the input language

This section gives a general workflow for updating the multi-shot implementation for extensions of the input language. First, the multi-shot preprocessing and encodings need to be updated (see multi-shot encoding update workflow).

In the multi-shot application there are then several functions that need to be updated to handle extensions of the multi-shot preprocessing and the general extension of the input language _update_incremental_data, _remove_new_incremental_expressions, _get_incremental_prog_part, _get_prog_part.

First, _update_incremental_data updates internal data structures to store information from the multi-shot specific preprocessing. However, as long as any new facts produced by the preprocessing follow the current argument structure of incremental/4 no changes to _update_incremental_data should be necessary.

Second, _remove_new_incremental_expressions removes certain facts from the list of processed facts in order to add them using incremental program parts. If the language extension added new kinds of incremental expressions then an according check should be added in this function. E.g. for function this function defines a condition is_incremental_function.

Third, _get_incremental_prog_part handles the conversion of a fact to its respective incremental program part. The function determines the name of the program part based on the type of the fact (such as function or binary). In simple cases (such as unary or minimize) a new type can just be added to one of the existing cases. In more complex cases (such as function) a new case has to be added.

Fourth, _get_prog_part works similarly to _get_incremental_prog_part but for non-incremental program parts. The new program part needs to be added to the list of valid program parts. For some types of program parts (such as the parts for type or constraint) it is also necessary to add the current bound as an additional argument. This is handled by the boolean variable needs_bound defined in this function.