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.

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.