Batch watch-list cleanup when reducing the learnt database

[GregoryGelfond]

reduceLearnts() destroys selected constraints one at a time. Because it does not open a dirty-watch scope, removeWatch() takes the eager path — a linear watch-list search plus an order-preserving erase per deletion. When many removed learnts watch the same literal that is quadratic in the number removed.

destroyDB() already avoids this by wrapping its deletions in initDirty(), which defers per-list compaction to a single pass. This does the same for reduceLearnts(), so the two bulk-deletion paths are consistent.

This is a potential performance fix only: it bounds a quadratic worst case rather than a measured speedup. On typical instances the removed learnts spread their two watches across many literals, so there is no measurable change — a pigeonhole solve (117k conflicts, 104k learnt deletions) is bit-identical in search and runtime. Search is unchanged in all cases.

Verified on dev-20: Release and ASan/UBSan builds clean, all 62 tests pass in both; the pigeonhole solve above is sanitizer-clean.

[BenKaufmann]

@GregoryGelfond As you might have noticed, I recently reworked the lazy constraint removal (2f440a7). As part of this change, I of course also considered this change (it was basically the motivation for the rework in the first place). However, extensive benchmarking on relatively large set did not show any real advantage. On the other hand, the hash over constraint addresses that is used in the lazy scheme makes PGO builds non-reproducible. I therefore deliberately decided against this change for now. Once I have fixed the PGO-reproducible issue (by excluding the relevant functions from the PGO data) and maybe found some benchmarks where this change makes a real difference (or replaced the current deletion schedule), I might come back to it.

[GregoryGelfond]

Thanks for the detailed context — that lines up with what we saw (no measurable change on our end either), so we'll drop it.

The PGO-reproducibility point is interesting in its own right. If a fix there would be useful to you, I'd be glad to help look into it — whether that's excluding the relevant functions from the profile, or making the lazy scheme's membership check address-independent (e.g. keyed on a stable id rather than the constraint pointer) so the probe pattern is deterministic. Happy to follow your lead on the approach. Thanks again for taking the time to explain.

[BenKaufmann]

The PGO-reproducibility point is interesting in its own right. If a fix there would be useful to you, I'd be glad to help look into it — whether that's excluding the relevant functions from the profile, or making the lazy scheme's membership check address-independent (e.g. keyed on a stable id rather than the constraint pointer) so the probe pattern is deterministic.

Regarding the first part - excluding the relevant functions from the profile - no help needed. I already know how/what to do here just haven't done it yet. However, I'd be interested in ideas regarding the second part. I have (briefly) thought about it but couldn't easily come up with an approach that wouldn't either hurt performance (additional memory/virtual call) or require a large refactoring of the way how constraints are stored/represented.
Happy to discuss any ideas you have there.

[GregoryGelfond]

I went ahead and prototyped this against dev-20. The nondeterminism is the address-keyed probe in cleanupDirty — with the same seed the probe/branch count moves run-to-run (I saw 46–61 over four identical runs) while the result is unchanged, which is what would perturb a PGO profile.

Two things stood out. First, the path is cold — cleanupDirty fired once in the whole unit suite and never once in a 790k-deletion solve (reduce detaches eagerly; the dirty_ scheme is only destroyDB(detach) — enumeration/minimize/aux). Second, because it's cold, the cheapest deterministic fix is enough: drop the address hash and scan the collected deleted pointers linearly — they're already in dirty_ in deletion order, so control flow is address-independent. Probe count goes constant across runs, all 62 tests stay green, and the hot path is untouched (the change is ~a dozen lines).

The one caveat is that it's O(|D|) per query rather than O(1), so a large-|D| detach-teardown would feel it; if you have a workload where that's hot I'm happy to look at the O(1)-preserving route, but that one does need keeping the deleted constraints alive to cleanup (they're freed first today) plus a mark bit — the memory/refactor you were trying to avoid.

I've opened it as #123 against dev-20 so you can read the actual diff and judge for yourself. Release and ASan/UBSan builds are clean and all 62 tests pass.