[lifthrasiir]

It would be more like an SAT-guided program synthesis---you can exhaustively generate all functions with at most n operations, and you can describe that particular operation as a boolean formula, so you can feed all of them to filter ones that are provably equivalent.

As for the actual boolean formula, I believe that he used his own creation, Haroldbot [1] which can evaluate bitwise expressions and enumerate all cases where the expression evaluates to true. Since simple formulas for previous and next integer with the same popcount, it should be doable. I've even constructed a concrete formula with the suggested formula:

    let n = (let t = x + (x & -x) in let u = x & ~t in t ^ ((u >>s tzcnt(u)) >>s 1)) in
    let p = (let v = x - (~x & (x + 1)) in let w = ~x & v in v ^ ((w >>s tzcnt(w)) >>s 1)) in
    let c = (let y = -x & (x + 1) in x ^ y ^ (y >> 1)) in
    (n == -1) || (p == 0) || (
        (p < x) && (popcnt(p) == popcnt(x)) &&
        (x < n) && (popcnt(x) == popcnt(n)) &&
        ((x - p > n - x) && (c == n)) || ((x - p <= n - x) && (c == p)))
    )

...where `n` is for the next such integer (or all 1s), `p` is for the previous such integer (or all 0s), `c` is for the closest such integer, and assuming that both `p` and `n` exists, `c` should be the closest of either `p` or `n`. This expression can be mechanically translated to a single boolean formula, which Haroldbot internally does for complicated formulas [2].

[1] http://haroldbot.nl/

[2] It apparently uses binary decision diagrams for simpler cases: http://haroldbot.nl/how.html