Skip to main content

Walkthrough — Module 13: Bitwise Tricks and Binary Decision Diagrams

Read this AFTER a stage is green — it explains how the reference solution is built and why.

Stage 1: Ruler function, sideways addition, Gosper's hack​

The reference builds RULER_TABLE at compile time with a const block: a while loop fills t[(DEBRUIJN << a) >> 58] = a for a in 0..64. That is worth stealing — it means the table costs nothing at runtime and is provably correct by construction (the reference tests separately verify all 64 windows are distinct, which is exactly the de Bruijn property that makes the inversion well-defined). ruler then isolates b = x & x.wrapping_neg() and reads RULER_TABLE[(b.wrapping_mul(DEBRUIJN) >> 58)]. The multiply is a left shift by a (since b = 2^a), so the product's top window is the a-th slice of the cycle — one multiply and one table lookup replace a loop.

sideways_addition is the classic SWAR cascade, and the comments pin down why each masked step is exact: after S1 each 2-bit field holds v - floor(v/2) = nu(v) (check all four values of a 2-bit field); S2/S3 fold counts into nibbles then bytes; S4's multiply by 0x0101... sums the eight byte-lanes into the top byte, safe because the grand total is at most 64 < 256 so no carry crosses a lane. next_same_weight (Gosper) is three lines with a precise domain contract: it panics on x==0 and documents that the top-of-weight case overflows in the x+u carry — the reference is honest that the trick is partial rather than silently returning garbage. Note the use of wrapping_neg/wrapping_sub throughout: these identities are defined on the two's-complement wrap, and using checked arithmetic would panic on x==0 in the wrong place.

Stage 2: Building reduced ordered BDDs​

Everything funnels through mk(v, lo, hi), and that is the single most important design choice: reduction rule 1 (lo == hi → return lo) and rule 2 (unique-table lookup) live in exactly one function, so no other code can ever create an unreduced node. variable, apply, and the sinks all go through it. This is why the tests can assert == on Refs to mean semantic equality — canonicity is an invariant maintained by construction, not checked after the fact. The arena is Vec<Node> with Ref(u32) indices rather than Rc<RefCell>; sinks are stored first with var = TERMINAL_VAR = u32::MAX so that level(sink) = u32::MAX sits below every real variable and the min(level(f), level(g)) in apply naturally never picks a sink.

apply is textbook memoized Shannon expansion, but three details make it fast and correct. First, step A1 special-cases the sink identities per operator so recursion bottoms out early (e.g. 0 ∧ g = 0, f ⊕ f = 0). Second, the memo key is commutativity-normalized (if f.0 <= g.0 { (op,f,g) } else { (op,g,f) }) so and(f,g) and and(g,f) share a cache entry — halving the memo and guaranteeing the same Ref. Third, an operand that does not test the top variable v is split as (f, f) rather than descended, so a function independent of v is handled without spurious nodes. The result is O(|f|·|g|) apply, the bound that makes BDDs practical; a version that re-expanded without the memo would be exponential.

Stage 3: Model counting and the ordering problem​

count_models is Algorithm 7.1.4C with the level-skip weighting made explicit. The reference splits it into count_rec (the memoized recursion returning the count below a node) and a final shift c << level_at(f, n_vars) in count_models that pays for the variables above the root. Inside, each child's contribution is shifted by level_at(child) - v - 1: the number of variables the edge jumps over, each free to take either value. Pinning a sink's level to n_vars via level_at is the trick that makes the arithmetic uniform — the ⊤ sink "at level n_vars" means an edge into it from level v skips n_vars - v - 1 variables, exactly the tail freedom. Using u128 matters: over 16 variables the count in the ordering experiment is 2^16 - 3^8, and larger instances overflow u64.

The stage's real lesson is that BDD size is not intrinsic to the function but to the variable order. The reference's ordering_experiment test builds the same OR-of-8-pairs function two ways: pairing variables adjacently gives B(f) = 2k+2 = 18 nodes, while listing all "first" variables before all "second" gives 2^(k+1) = 512 — a 28× blowup for an identical boolean function (identical model count, 2^16 - 3^8, confirming they are the same function). That is why node_count (a simple DFS over a visited HashSet) is a first-class operation here: it is the instrument you use to see the ordering problem, which is undecidable to optimize in general.

Stage 4: BDDs at work: independent sets and queens​

Both functions are declarative: they state constraints as boolean formulas and let the shared arena do the work, so the "algorithm" is really just conjunction plus stage-3 counting. independent_set_count folds f = f AND not(and(x_u, x_v)) over the edges — "no edge has both endpoints chosen" — and returns count_models(f, n). Because the BDD is canonical and hash-consed, the order you add edges in doesn't affect the answer, only intermediate size. The reference validates against closed forms the theory predicts: P_4 → F_6 = 8, C_5 → L_5 = 11, empty graph → 2^n.

queens_bdd_count is the same recipe scaled up: n^2 cell variables, an AND of not(a AND b) over every attacking pair (same row, column, or abs_diff equal on both axes for diagonals), plus a per-row OR forcing at least one queen. The comment records the crucial modeling insight — the at-least-one-per-row clauses together with the no-attack clauses force exactly one queen per row, so the BDD's models are precisely the classical solutions, no over- or under-counting. The honest caveat is also in the code: this variable order makes the BDD grow exponentially, so the function is capped at small n (answers 2, 10, 4 for n = 4, 5, 6) rather than pretending BDDs make n-queens easy.