格雷码：构造每步只变一位的数列

本章的内容

格雷码是一种数列，相邻两项只差一位，常用于纠错编码、通信编码、电路设计与模数数模转换等场合。

• 4 位时把 0 到 15 各排一次，使相邻两项只有一位不同，并且首尾也相接

• 先用 Int 即整数来写，确认可行之后再换成 BitVec，速度会快很多

• 同一个问题，只改变变量的类型就可能快 100 倍以上

用 OrTools 解格雷码

思路

\(n\) 位的格雷码，是把 \(0\) 到 \(2^n-1\) 的数各排一次的序列，并满足下面的条件。

• 相邻的两个数只差一位

• 最后一个与第一个也只差一位，这样才能绕回起点

相邻只翻一位的好处是状态切换时的出错范围最小：一次只有一个位在变，读到的中间值要么是旧值，要么是新值。

用 Int 写的时候，需要取出 x 的第 i 位，这一位可以用 x % 2**(i+1) - x % 2**i 取出，第 i 位为 0 时结果是 0，为 1 时结果是 2**i。这个写法先丢掉第 i 位以上的部分，再减去第 i 位以下的部分，剩下的正好是第 i 位的值。两个数在这个值上不同，就说明这一位不同。

用整数变量求解

from z3 import *


def gray_code(nbits):
    """返回 nbits 位的格雷码（数的排列）"""
    n = 2 ** nbits
    codes = IntVector('code', n)
    solver = Solver()

    for c in codes:
        solver.add(0 <= c, c < n)
    solver.add(Distinct(codes))

    for c1, c2 in zip(codes, codes[1:] + codes[:1]):
        diff = Abs(c1 - c2)
        # 辅助条件：只差 1 位时，差值是 2 的幂
        solver.add(Or([diff == 2 ** bit for bit in range(nbits)]))
        # 真正的条件：不同的位恰好 1 个
        bit_diff = [c1 % 2**(i + 1) - c1 % 2**i != c2 % 2**(i + 1) - c2 % 2**i
                    for i in range(nbits)]
        solver.add(Sum(bit_diff) == 1)

    solver.add(codes[0] == 0)      # 为了消除旋转，把开头固定为 0

    assert solver.check() == sat
    model = solver.model()
    return [model[c].as_long() for c in codes]


nbits = 4
%time codes = gray_code(nbits)
for c in codes:
    print(f'{c:0{nbits}b}')

CPU times: total: 9.19 s
Wall time: 9.33 s
0000
0001
1001
1011
0011
0111
1111
1110
1010
1000
1100
1101
0101
0100
0110
0010

这样就得到了 0 到 15 各排一次、相邻两项只差一位的序列。

用 Int 写则慢得多，在这个环境里花了几秒：位运算被写成了取模与除法，Z3 只能按整数算术推理，缺少逐位的手段。

用 BitVec 提速

处理位的问题，一开始就用位向量的类型 BitVec 更为自然。把 Int 换成 BitVec 之后，

• 取位可以用 >> 与 & 写出

• 两个数的差别用一个 ^，即 XOR，就能看出

c1 ^ c2 是只在不同位上为 1 的数。在格雷码里，这个数必须是 2 的幂，即只有一个 1，例如 0101 ^ 1101 = 1000。

diff = c1 ^ c2
solver.add(diff & (diff - 1) == 0, diff != 0)

diff & (diff - 1) == 0 是判断 diff 是否为 2 的幂的常用技巧。它把“只有一位不同”换成了“差值是 2 的幂”，一次减法与一次按位与就完成了判断。2 的幂减去 1 之后，比它低的所有位都变成 1，再与原数做 AND 就得到 0。而 diff != 0 是为了排除两数相同、即没有任何一位不同的情形。

def gray_code_bv(nbits):
    """BitVec 版：用位运算解同一个问题"""
    codes = [BitVec(f'code_{i}', nbits) for i in range(2 ** nbits)]
    solver = Solver()
    solver.add(Distinct(codes))

    for c1, c2 in zip(codes, codes[1:] + codes[:1]):
        diff = c1 ^ c2                       # 只有不同的位为 1
        solver.add(diff & (diff - 1) == 0,   # 2 的幂
                   diff != 0)                # 不是 0

    solver.add(codes[0] == 0)

    assert solver.check() == sat
    model = solver.model()
    return [model[c].as_long() for c in codes]


%time codes = gray_code_bv(nbits)
for c in codes:
    print(f'{c:0{nbits}b}')

CPU times: total: 15.6 ms
Wall time: 22.5 ms
0000
1000
1100
0100
0101
0111
0110
1110
1111
1101
1001
1011
1010
0010
0011
0001

BitVec 版几乎立刻结束：在这个环境里 Int 版约十秒，BitVec 版约 0.03 秒，相差 300 倍以上。差距来自求解器可用的推理方式：位向量的每一位都是独立的布尔变量，求解器可以直接按位推理，不必先证明关于整数的结论。Int 版的耗时每次都在数秒到十几秒之间波动，但量级不会变。

得到的排列可能与 Int 版不同，但两者都是正确的格雷码，因为满足条件的排列并不只有一种。两种写法的分工也随之清楚：先用 Int 写对条件，再换 BitVec 提速。

小结

• 格雷码是相邻两项只差一位的排列方式

• 用 Int 时，要写成差为 2 的幂，并且只有一位不同

• 处理位的问题换成 BitVec 就快，用 XOR 可以把差别写在一个式子里

• diff & (diff - 1) == 0 是判断是否为 2 的幂的技巧

• 解不唯一，Z3 返回的是满足条件的最先找到的那一个