Add ZDD-based N-queens solver benchmark #478
Open
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a benchmark that solves the N-queens problem using ZDDs. The
ZDD data structure code is based on the existing ZDD benchmark. The
motivation for this benchmark is that its performance benefits greatly from
the memoization of the ZDD operations, while the existing benchmark is
faster without memoization. In this sense, this benchmark is more
representative of actual use cases where the sharing introduced and enforced
by hash-consing is used to share subcomputations using memoization to give
polynomial-time algorithms that would be exponential-time without
sharing. (Although note that some ZDD operations are polynomial time with
sharing, others still have worst-case exponential time even if in practice
they are often fast.) Additionally, this benchmark shows Ephemeron-based
caching outperforming (simplistic) Hashtbl-based caching.
Compile:
Usage example:
The argument (8 above) indicates the size of the chess board and number of
queens to place. The correct numbers of solutions are given in
https://oeis.org/A000170.
In addition to the problem size argument, three environment variables are
read:
Exploring this parameter space a bit, the first observation is that
disabling node hash-consing or operation memoization is much slower:
Another observation is that a lot of time can be spent resizing tables, and
the initial sizes make a significant difference:
Here MEMO_SCALE=0 sets the initial tables to the minimum allowed by Weak or
Hashtbl, 1 is small, and 192 is large enough to avoid needing to resize.
Finally, Ephemeron-based caching is more efficient than Hashtbl-based
caching, and this is true for OCaml 4 and 5:
For the record, "trunk" here is from commit 137dd26adc of Sat Jan 18, 414 is
the official 4.14.2 release, with flambda enabled for both.
Signed-off-by: Josh Berdine [email protected]