You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We encountered a few cases where the solver uses more than 1.5GB of RAM. Almost all memory usage seems to be related to clauses, specifically ForbidMultipleInstances.
Total number of solvables: 65335
Total number of watches: 68317 (1021 KiB)
Total number of clauses: 46291650 (1.4 GiB)
- Requires: 423637
- Constrains: 4882449
- Lock: 0
- Learned: 1
- ForbidMultiple: 40985343
- pyarrow: 22101276
- arrow-cpp: 9885681
- botocore: 1798356
- boto3: 1335795
- hypothesis: 1191196
...
This happens when there are a relatively large number of candidates to consider for a single version (a few thousand). The number of ForbidMultiple clauses that we allocate is O(n^2).
Possible solution
We could look at implementing commander encoding to encode these clauses differently which should be O(n). We already implemented binary encoding in #37 but with a number of other improvements this PR has fallen to the wayside.
The text was updated successfully, but these errors were encountered:
Description
We encountered a few cases where the solver uses more than 1.5GB of RAM. Almost all memory usage seems to be related to clauses, specifically
ForbidMultipleInstances
.This happens when there are a relatively large number of candidates to consider for a single version (a few thousand). The number of ForbidMultiple clauses that we allocate is
O(n^2)
.Possible solution
We could look at implementing commander encoding to encode these clauses differently which should be
O(n)
. We already implemented binary encoding in #37 but with a number of other improvements this PR has fallen to the wayside.The text was updated successfully, but these errors were encountered: