Generalize data-based synthesis options for variable ordering algorithms
Initial idea
Data-based synthesis only allows DCSH to be applied before FORCE and FORCE before sliding window (after #196 (closed)). The order is fixed. I think the options should be generalized, to allow for instance: choice(dcsh, sequence(force, sliding-window(9)))
etc. This gives more flexibility for testing different configurations (#375 (closed), #376 (closed), #377 (closed)). Actual testing would require more benchmark models though (#364).
We may even want to allow specifying the metric (total span vs WES) and sub-algorithms (e.g., pseudo-peripheral node finders) they use (#379 (closed)).
Current options
We currently have the following options that influence the BDD variable order:
- The initial variable ordering is determined by:
-
--var-order=normal/reverse-normal/sorted/reverse-sorted/random/random:<some seed>/custom
, with custom the names of variables and automata, separated by,
for interleaving and;
for non-interleaving, with*
a wildcard.
-
- This may be optimized by automatic algorithms that can be enabled independently (order is fixed, in the order they are given here):
--dcsh-order=yes/no
--force-order=yes/no
--sliding-window-order=yes/no
- Some settings influence these algorithms:
-
--sliding-window-size=<some number>
(only affects sliding window) -
--hyper-edge-algo=legacy/linear
(affects the hyper-edges, and thus the graph, and thus all 3 algorithms)
-
Goals
The goals include:
- Allow any order for the algorithms.
- Allow choosing between multiple options, for instance to try multiple initial orders, or multiple different algorithms with different settings.
- Allow customizing all settings for each algorithm separately.
- Allow reproducing the DCSH algorithm from the paper (see #376 (closed)).
- Allow a better default for variable ordering (see #379 (closed)).
Proposal for the option to configure variable ordering
I propose the following design for the value of a new variable ordering option:
- General design:
- Orders and algorithms are identified by name.
- They can have parameters. All parameters are mandatory, but may be given a default. Arguments must be given for parameters without a default, and may be given for parameters with a default, to override the default.
- If arguments are given, the name is postfixed with
(...)
with the arguments in the...
part. - Each argument is a key/value pair, e.g.
arg=value
. - Multiple arguments are separated by commas.
- If an argument includes a comma, use double quotes around the argument value, e.g.
arg="a,b,c"
.
- Base orders:
-
model
,sorted
,random
remain as they are, and produce a basic/initial variable ordering. - No specific reverse options are provided. To reverse
model
usereverse(input=model)
, see below. - To specify a seed for random, use
random(seed=...)
. E.g.random(seed=5)
. - To specify a custom order,
custom(order="...")
is used, with the current syntax of specifying a custom ordering as argument to theorder
argument of thecustom
order. E.g.custom(order="a,b;c,d*")
.
-
- Algorithmic orderers:
-
or(name=..., metric=span|wes, hyperedges=legacy|linear, choices=...)
allows to choose between multiple choices, based on a chosen metric on chosen hyper-edges. It may optionally be given a name, to identify it as such. For instance,or(name=MyName, metric=span, hyperedges=linear, choices="model,random(seed=23),sloan(input=model)")
. -
reverse(input=...)
reverses a given input order. E.g.reverse(input=model)
. -
dcsh(input=...)
equalsor(name=DCSH, metric=wes, hyperedges=linear, choices="weighted-cm(input=...), sloan(input=...), reverse(weighted-cm(input=...)), reverse(sloan(input=...))")
. -
weighted-cm(graph=legacy|linear, nodefinder=george-liu|sloan, input=...)
optimizes a giveninput
order, based on agraph
created from chosen hyper-edges, and using the configured pseudo-peripheral node finder algorithm. -
sloan(graph=legacy|linear, input=...)
optimizes a giveninput
order, based on agraph
created from chosen hyper-edges. It uses a pseudo-peripheral node pair finder algorithm, of which we currently have only one, so that is not configurable. -
force(metric=span|wes, hyperedges=legacy|linear, input=...)
optimizes the giveninput
order, based on chosenhyperedges
and givenmetric
. -
slidwin(metric=span|wes, hyperedges=legacy|linear, input=..., size=...)
optimizes the giveninput
order, based on chosenhyperedges
and givenmetric
, for a window of maximum sizesize
.
-
The current default variable order would be slidwin(metric=span, hyperedges=legacy, size=4, input=force(metric=span, hyperedges=legacy, input=sorted))
. If we use suitable defaults, we can reduce this to slidwin(input=force(input=sorted))
.
We could consider alternative syntaxes:
- Using a real syntax and parser may allow for more than is currently proposed.
- The current proposal has as benefit that through
input=...
you must specify an input order, as in the code API. However, it also means that you wrap things that are applied later, around the thing that it is applied after. This reverses the order of application from the order to specify. For instance, the default as described above hassorted
last andslidwin
first. While the order issorted
->force
->slidwin
. With a more free syntax, we could actually allow this->
syntax. This would essentially be direct syntax for the sequence variable orderer, which is now implicit in the nested structure.
Regarding backward compatibility:
- There are several solutions to choose from:
- This new option could replace all the current options. But that is backward incompatible.
- We could try to integrate the new configuration options it into
--var-order
, keeping all the current options, but adding additional syntax for new configurations. Not sure whether that is feasible. Likely we should then forbid the new configurations with combinations of existing options. But that may be tricky, because how do you know whether someone that keeps the defaults actually wants the default explicitly, or doesn't care. If they specify something non-default, that is more clear. - Keep the old options, just adding a new option, and deprecate the old options.
- Keep the old options, just adding a new option, and support both the old and the new options. We may reconsider things later then.
- For now, the proposal is to support both the old options, and the new one:
- If default old options are used, and default new option is used, use the default variable order (make sure the defaults are in sync).
- if default old options are used, and non-default new option is used, use the new option.
- If non-default old options are used, and default new option is used, use the old options (don't warn or give an error, for now just supports both old and new).
- If non-default old options are used, and non-default new option are used, give an error and stop.
Proposal for code changes to variable orders themselves
We need changes to allow more flexibility in the code, to allow for instance DCSH and FORCE to use different hyper-edge implementations. That is mostly independent of the options/syntax to allow to configure that. Even if users can't configure anything more advanced than they can now, then still we want to be able to configure in the code a more advanced / better default than we can do now.
I propose the following changes:
- Allow configuring more settings for the various variable orderers.
-
ChoiceVarOrderer
: hyperedges -
DcshVarOrderer
: (nothing extra to configure) -
ForceVarOrderer
: metric, hyperedges -
ReverseVarOrderer
: (nothing extra to configure) -
SequentialVarOrderer
: (nothing extra to configure) -
SlidingWindowVarOrderer
: metric, hyperedges -
SloanVarOrderer
: graph -
WeightedCuthillMcKeeVarOrderer
: graph, nodefinder
-
- Turn base orders into variable orderers as well, but with a slightly different interface, not having an input order. This separates the code a bit from the way too long
CifToSynthesisConverter
class. But mostly, it allows easily invoking it multiple times, for instance to allow using them as the starting point of multiple sequential orderers.
Step by step changes/status
-
Variable ordering algorithms get more parameters. (!434 (merged)) -
Base orders become variable orderers. (!457 (merged)) -
Variable ordering and automatic/algorithmic reordering in one go. (!472 (closed), !477 (merged)) -
Add new option for more powerful variable ordering configurations. (!498 (merged))
Edits
- 2022-12-06: More goals added.
- 2022-12-06: Considerations for syntax alternatives added.
- 2022-12-06: Some fixes in the proposals.
- 2022-12-06: Multiple options for old vs new options.
- 2022-12-06: Added proposal for changes to variable orders themselves.
- 2022-12-10: New ideas for old vs new options.
- 2022-12-10: Added phased changes (step by step).
- 2022-12-10: Improve explanation of why base orders become variable orders as well.
- 2023-01-05: Updated status with progress.
- 2023-01-08: An extra intermediate step added.
- 2023-01-29: Small textual fix.
- 2023-01-29: Progress updated.
- 2023-02-06: Progress updated.