perf: encode shared constraints with an auxiliary variable per version set

[baszalmstra]

Summary

This pull request replaces the pairwise Constrains clause encoding with a shared auxiliary-variable encoding. Previously every (parent, version set) constraint pair emitted one binary clause per candidate excluded by the version set, so the same excluded-candidate list was re-emitted for every parent sharing a constraint. On conda-forge style workloads these clauses dominate the clause database.

Key Changes

Constraints whose version set excludes at least 4 candidates now share one auxiliary variable per version set, meaning "a candidate excluded by this version set is installed":

• ConstrainsExcluded: (¬candidate ∨ aux), emitted once per version set;
• ConstrainsParent: (¬parent ∨ ¬aux), one clause per (parent, version set) pair.

This reduces the constrains clause count from O(parents × candidates) to O(parents + candidates). Constraints excluding fewer than 4 candidates keep the pairwise encoding, which is smaller and propagates in a single hop for short lists.

Performance Results

Benchmarked on the conda-forge dataset (linux-64 + noarch snapshot, 1000 randomized problems per seed, two seeds, identical problem sequences on both sides, clean release builds, 60s timeout):

Speedup (2000 problems)
mean	1.27×
median	1.13×
p75	1.29×
p95	1.27×
p99	1.50×
timeouts	6 → 3

The gains extend the solvable frontier: main hits the 60s timeout on 6 problems, this PR on 3 (a strict subset), so 3 problems become solvable that previously were not. The largest single-problem improvement is 42.8s (a main timeout solved in 17.2s); the worst regression is +10.8s (40.9s vs 30.1s, both completing).

Clauses & memory (cumulative, 2000 problems)	main	this PR
total clauses	5,359M	975M	5.5× fewer
constrains clauses	4,659M	275M	16.9× fewer
clause memory	171.5 GB	31.2 GB	5.5× less
per-solve solver memory, p50	85.6 MiB	26.8 MiB	3.2× less
per-solve solver memory, max	510 MiB	100 MiB	5.1× less
variables	53.0M	54.3M	+2.6%

Not a single problem of the 2000 uses more clauses or memory with the new encoding. Search effort drops as well: 1.39× fewer conflicts and 1.27× fewer clause visits in aggregate, and the smaller database also makes encoding 1.32× faster.

Technical Rationale

Propagation strength is preserved, in two hops instead of one: parent = true propagates aux = false which propagates ¬candidate for every excluded candidate, and conversely candidate = true propagates aux = true which propagates ¬parent. Only one implication polarity is needed because the auxiliary variable is never decided directly; it only takes values through propagation. This is the one-sided (polarity-aware) variant of the Tseytin transformation, due to Plaisted and Greenbaum (1986).

Conflict reporting reconstructs the original parent → candidate edges by pairing the two clause kinds through their shared auxiliary variable, so rendered conflict messages are identical to the pairwise encoding on the entire existing test suite.

Correctness

• Every explicitly requested package resolves identically on all 2000 problems. 98.4% of solutions are byte-identical; the rest differ only in transitive picks, and both sides' picks are valid (CDCL learning takes a different path and transitive choices are greedy in decision order).
• 93% of unsat messages are byte-identical; the rest are valid alternative unsat cores produced by the unchanged renderer. Conflict-graph dumps confirmed that the edge reconstruction neither drops nor fabricates edges in the diverging cases.
• Known trade-off: on a ~0.5% tail of conflict-heavy problems, learning over the coarser auxiliary chain needs more conflicts and runs up to ~5× slower in ratio (worst observed +10.8s absolute); the aggregate distribution absorbs this comfortably, with p99 still 1.4-1.9× faster per seed.

New clause-count shape tests assert the M + N encoding (and N × M for the pairwise small case), and new unsat snapshot tests cover the shared encoding in forward, reverse, and multi-parent conflict directions; their snapshots are byte-identical to the pairwise encoding's output.