nvars (≤ ~15k). Fastest per-sample access.nvars is large
and clauses are short (k ≤ ~5), so most variables stay unset.nvars
(≥ ~50k). Per-sample memory is bounded by clause length, not
nvars. Limitations: assumes default 1/2
weights, and clauses must be ≤ 64 literals.