Advanced variable ordering configuration

The CIF data-based synthesis performance depends greatly on the variable ordering. After selecting an initial ordering, it can subsequently be improved by algorithms for automatic variable ordering. This may be configured using basic options, but they offer only limited flexibility. For the most flexibility, variable ordering can be configured using the BDD advanced variable ordering option (see the options section). Advanced ordering allows configuring which orderers, such as predefined orders and ordering algorithms, to use. It also allows configuring the order in which the various orderers are applied, as well as the settings to use for each orderer.

Variable ordering may be configured using either the basic options or using the advanced option. It is not supported to configure variable ordering using both basic and advanced configuration at the same time.

Examples

The predefined initial variable orderings can be expressed using the advanced syntax as follows:

Predefined initial ordering Advanced syntax

model

model

reverse-model

model(effect=var-order) → reverse(effect=both)

sorted

sorted

reverse-sorted

sorted(effect=var-order) → reverse(effect=both)

random

random

random:SEED

random(seed=SEED)

<custom-order>

custom(order="<custom-order>")

Some other examples of advanced variable orderings:

  • model -> dcsh -> force -> slidwin: Start with model order as initial order, and then apply the DCSH, FORCE and sliding window algorithms with their default settings.

  • sorted -> dcsh(relations=linearized): Start with sorted order as initial order, and then apply the DCSH algorithm with linearized variable relations.

  • random -> or(choices=[dcsh,force]): Start with a random order as initial order, and then apply the DCSH and FORCE algorithms, choosing the best order from the ones produced by the two algorithms.

  • force -> reverse: Start with the default initial model order, then apply the FORCE algorithm, and finally reverse the variable order.

Syntax

The syntax to specify advanced variable ordering generally works as follows:

  • Orderers are specified by their name.

  • Arguments to configure orderers may optionally be given after the name of the orderer between parentheses: (...).

  • It is allowed to provide empty parentheses, e.g., model() is equivalent to specifying model.

  • Each argument is given by a name and a value: name=value.

  • To specify multiple arguments, separate them with a comma. After the last argument, optionally a comma may be specified as well.

  • To apply multiple algorithms in sequence, separate them with an arrow (->).

  • If needed, a sequence of orderers may be enclosed in parentheses: (... -> ... -> ...).

  • Spaces, tabs, and newline characters are generally ignored, but can be used to improve readability.

Orderers

The following orderers can be specified:

  • Basic ordering

    Uses the configuration as configured by the basic variable ordering options.

    • Name: basic

    • Arguments: n/a

    • Example: basic

  • Model order

    Uses the predefined model order.

    • Name: model

    • Arguments:

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: both

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: model, model(effect=var-order)

  • Sorted order

    Uses the predefined sorted order.

    • Name: sorted

    • Arguments:

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: both

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: sorted, sorted(effect=var-order)

  • Random order

    Uses the predefined random order.

    • Name: random

    • Arguments:

      • seed

        • Description: a seed for the random order

        • Mandatory: no

        • Default: use a random seed

        • Type: number

        • Constraints: seed must be in the range [0 .. 264 - 1]

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: both

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: random, random(seed=123), random(seed=123, effect=var-order)

  • Custom order

    Uses a custom order.

    • Name: custom

    • Arguments:

      • order

        • Description: the custom order, with the same syntax as for the basic configuration option

        • Mandatory: yes

        • Default: n/a

        • Type: string

        • Constraints: the order must be complete in that it contains all variables, and must not contain any duplicate variables

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: both

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: custom(order="a,b;c,d"), custom(order="a,b;c,d", effect=var-order)

  • DCSH

    Applies the DCSH algorithm.

    • Name: dcsh

    • Arguments:

      • node-finder

        • Description: the node finder algorithm to use for the Weighted-Cuthill-McKee orderer

        • Mandatory: no

        • Default: george-liu

        • Type: enum (george-liu or sloan)

        • Constraints: none

      • metric

        • Description: the metric to use to compare orders

        • Mandatory: no

        • Default: wes

        • Type: enum (total-span or wes)

        • Constraints: none

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: dcsh, dcsh(metric=wes), dcsh(node-finder=george-liu, metric=wes, relations=configured, effect=both)

  • FORCE

    Applies the FORCE algorithm.

    • Name: force

    • Arguments:

      • metric

        • Description: the metric to use to compare orders

        • Mandatory: no

        • Default: total-span

        • Type: enum (total-span or wes)

        • Constraints: none

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: force, force(metric=total-span), force(metric=total-span, relations=configured, effect=both)

  • Sliding window

    • Name: slidwin

    • Arguments:

      • size

        • Description: the maximum size of the window

        • Mandatory: no

        • Default: 4 (as configured by the BDD sliding window size option)

        • Type: number

        • Constraints: size must be in the range [1 .. 12]

      • metric

        • Description: the metric to use to compare orders

        • Mandatory: no

        • Default: total-span

        • Type: enum (total-span or wes)

        • Constraints: none

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: slidwin, slidwin(size=5), slidwin(size=5, metric=total-span, relations=configured, effect=both)

  • Sloan

    • Name: sloan

    • Arguments:

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: sloan, sloan(relations=configured, effect=both)

  • Weighted Cuthill-McKee

    • Name: weighted-cm

    • Arguments:

      • node-finder

        • Description: the node finder algorithm to use

        • Mandatory: no

        • Default: george-liu

        • Type: enum (george-liu or sloan)

        • Constraints: none

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: weighted-cm, weighted-cm(relations=configured), weighted-cm(node-finder=george-liu, relations=configured, effect=both)

  • Choice

    Applies multiple algorithms to the same variable order and chooses the best resulting order.

    • Name: or

    • Arguments:

      • choices

        • Description: the orderers to apply

        • Mandatory: yes

        • Default: n/a

        • Type: list of orderers

        • Constraints: at least two orderers must be specified

      • metric

        • Description: the metric to use to compare orders

        • Mandatory: no

        • Default: wes

        • Type: enum (total-span or wes)

        • Constraints: none

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: or(choices=[dcsh,force]), or(choices=[(force -> dcsh), (dcsh -> force)], metric=wes, relations=configured, effect=both)

  • Reverse

    Reverses the variable order.

    • Name: reverse

    • Arguments:

      • relations

        • Description: the kind of relations to use when computing metric values

        • Mandatory: no

        • Default: configured (per the BDD hyper-edge creation algorithm option)

        • Type: enum (configured, legacy or linearized)

        • Constraints: none

      • effect

        • Description: the effect of the variable orderer

        • Mandatory: no

        • Default: var-order

        • Type: enum (var-order, representations or both)

        • Constraints: none

    • Examples: reverse, +reverse(relations=configured, effect=both)

Node finders

Orderers that work on graphs may use a pseudo-peripheral node finder algorithm while computing a variable order. Multiple such node finders can be used:

Metrics

To compare different orders, and choose the best one, metric values are used. Multiple metrics can be used:

Relations

Metric value can be computed using different variable relations derived from the CIF specification. Multiple metrics can be used:

  • Legacy

    Use the legacy relations.

    Name: legacy

  • Linearized

    Use the linearized relations.

    Name: linearized

  • Configured

    Use the relations as configured using the BDD hyper-edge creation algorithm option.

    Name: configured

Effects

A variable orderer produces a variable order. The effect of a variable orderer determines what happens with the produced order:

  • It may be used as the new variable order. The produced variable order then becomes the variable order to be used as input to the next orderer, or the final order in case it is the effect of the last orderer. If the produced variable order is not used as the new variable order, the variable order remains unchanged by the orderer.

  • It may be used to compute new representations of the variable relations. Subsequent orderers will then use these new representations as input to algorithms and for computing metrics. If the produced variable order is not used to create new representations, the representations remain unchanged by the orderer.

The following effects can be configured:

  • Variable order

    Uses the produced variable order as the new variable order. Does not update the representations.

    Name: var-order

  • Representations

    Updates the representations. Does not use the produced variable order as the new variable order.

    Name: representations

  • Both

    Uses the produced variable order as the new variable order, and updates the representations.

    Name: both