グレーコード ― 1ビットずつ変化する数列を作る

グレーコード ― 1ビットずつ変化する数列を作る#

この章で学ぶこと#

グレーコードは、隣り合う値が1ビットだけ違うように並べた数列です。誤り訂正、エンコーディング、回路設計、アナログ-デジタル変換などで使われます。

  • 4ビットなら 0〜15 を1回ずつ並べ、隣どうしの差が1ビットだけになるようにする

  • 最初は Int（整数）で書き、そのあと BitVec に置き換えて速くする

  • 同じ問題でも、変数の型を変えるだけで100倍以上速くなることがある

OrToolsでグレーコードを解く

考え方#

\(n\) ビットのグレーコードは、\(0\) から \(2^n-1\) までの数を1回ずつ並べた列で、次の条件を満たします。

  • 隣り合う2つの数は、ちょうど1ビットだけ違う

  • 最後と最初も、ちょうど1ビットだけ違う（一周して戻れる）

Int で書くときは、x の i 番目のビットを取り出す必要があります。x % 2**(i+1) - x % 2**i を使うと、i 番目のビットが 0 なら 0、1 なら 2**i になります。この値が2つの数で違えば、そのビットが違う、と判定できます。

Int 変数で解く#

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: 10.5 s
Wall time: 11.1 s
0000
0001
1001
1011
0011
0111
1111
1110
1010
1000
1100
1101
0101
0100
0110
0010

0 から 15 までが1回ずつ並び、隣どうしが1ビットだけ違う列ができました。

ただし、Int で書くと Z3 は遅いです。この環境では数秒かかりました。ビットの操作を数の割り算で表しているので、Z3 が扱いにくい式になっているためです。

BitVec で速くする#

ビットを扱う問題なら、最初からビット列の型 BitVec を使うのが自然です。Int を BitVec に変えると、

  • ビットの取り出しが >> と & で書ける

  • 2つの数の違いが ^（XOR）1つで分かる

c1 ^ c2 は「違うビットだけが 1 になる」数です。グレーコードでは、これが2のべき乗（1が1つだけ立っている）になります。

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

diff & (diff - 1) == 0 は「diff が2のべき乗かどうか」を判定する定番のテクニックです。2のべき乗は、1から1を引くと、立っていたビットが全部 1 に変わり、元の数と AND すると 0 になります。diff != 0 は「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: 37.4 ms
0000
1000
1100
0100
0101
0111
0110
1110
1111
1101
1001
1011
1010
0010
0011
0001

こんどの BitVec 版は一瞬で終わりました。この環境では Int 版が10秒前後、BitVec 版が 0.03 秒ほどで、300倍以上の差です（Int 版の時間は実行のたびに数秒〜十数秒と変わりますが、桁が変わることはありません）。

出てきた並びは Int 版と違うことがありますが、どちらも正しいグレーコードです。条件を満たす並べ方は1通りではないからです。

まとめ#

  • グレーコードは「隣どうしが1ビットだけ違う」並べ方

  • Int では「差が2のべき乗」＋「違うビットがちょうど1つ」で書ける

  • ビットを扱う問題は BitVec にすると速い。XOR で違いが1つの式で書ける

  • diff & (diff - 1) == 0 は「2のべき乗か」の判定テクニック

  • 解は1通りではない。条件を満たす並べ方のうち、Z3 が最初に見つけたものが返る