Encodings for multi-shot solving

This section gives an overview of the encodings for solving an instance with unbounded cardinalities using multi-shot solving. These encodings mostly just reorganize the main COOM encoding into specific program parts for multi-shot solving.

For example usage information see the Cargo bike example.

We start by explaining some general concepts using a simplified version of the Cargo bike example.

product {
         num 0-20 numBags
    0..* Bag      bags
}

structure Bag {
    Color color
}

enumeration Color { Red Blue }

behavior {
    require numBags = count(bags)
}

behavior Bag {
    require color = Blue
}

Preprocessing

The preprocessing removes the cardinality on Bags by instatiating a number of bags based on the max_bound parameter of the preprocessing encoding. Using one of the bounds strategies we step-wise increase this parameter until a solution is found.

To avoid regrounding and resolving the same part of a problem over and over, we employ multi-shot solving here: we add the new facts generated by the preprocessing of a new max_bound as new program parts.

The facts added by a new step of the preprocessing can be divided into two groups: object and constraint facts.

Object Facts

Facts of the first group are the predicates parent, index, set, and type describing a new object. These are added through respective program parts in the new-object encoding.

Constraint Facts

The second group of facts is made up of facts describing new constraints as well as their components (i.e. binaries, unaries, and functions). The constraints (and their components) are further divided into two categories: simple constraints and incremental constraints.

Simple Constraints

An example for a simple constraint is the constraint on the color of a Bag. This constraint will be added for each new instance of Bag but is not affected by the addition of further instances later on. The additions of this kind of constraint (and its components) is handled by the new simple constraint encodings

Incremental Constraints

An example for an incremental constraint is the constraint on numBags: it uses a count aggregate over all instances of Bag. This constraint is added once (at the beginning) but its evaluation changes over time: with each step of the preprocessing new instances of Bag are added and need to be taken into account when evaluating this constraint. These kinds of constraint (and their components) are handled by the new incremental constraint encodings

Note that also a table constraint can be incremental. Consider the following example.

product {
    0..* Bag      bags
}

structure Bag {
         Color color
    0..* Pocket pockets
}

enumeration Color { Red Blue }

enumeration Pocket { Small Large }

behavior Bag {
    combinations (color pockets)
    allow        (Red   Small  )
    allow        (Blue  Large  )
}

With max_bound of 1, a first instance of the table constraint is added constraining bags[0].pockets[0]. When the max_bound is increased to 2 a new instance of the same table is added constraining bags[0].pockets[1]. The different instantiations of a table are distinguished by the second argument of the column/4 predicate. However, note that each instance of the table constraints itself behaves like a simple constraint from above. This is used in the evaluation of incremental constraints in the respective encoding.

Multi-Shot Specific Preprocessing

The classification of which constraints and expressions are incremental is handled by a multi-shot specific addition to the preprocessing encoding.