CRC32 Quine を Z3 で解く

ref: http://shinh.hatenablog.com/entry/2014/12/25/013926

おー。

Z3 で再現してみた。

$ time python crc32.py 
86319a79    
58a8a1b9

real    151m1.375s
user    151m7.607s
sys     0m0.179s

1 つめは 3 分くらいで見つかるけど、2 つめは 2 時間くらい、チェック完了までは 3 時間弱かかった。
単純に 2^32 個を全チェックする方法なら、秒間 100 万個調べられるとして 1 時間ちょっとという計算。まあ、こんなもんなのかな。追記：shinh さんによると 1 分でできるらしい。残念。

ソースはこんな感じ。もっと綺麗に書けそう。

# coding: utf-8
from z3 import *

# CRC-32 の生成多項式（の反転）
POLY = 0xedb88320 * 2 + 1

# BitVec(1) の 0
ZERO = BitVecVal(0, 1)

# 求めたい CRC-32
answer_crc32 = BitVec("answer", 32)

# answer_crc32 をテキスト化する
text_crc32 = []
for i in range(8):
    d = ZeroExt(4, Extract(31 - i * 4, 28 - i * 4, answer_crc32))
    d = If(d < 10, d + 48, d - 10 + 97) # [0-9a-f] の ASCII コードに変換する
    text_crc32.append(d)
text_crc32.append(10) # 最後の改行
# テキスト化をしない場合はこっち
# for i in range(4):
#    d = Extract(31 - i * 8, 24 - i * 8, answer_crc32)
#    text_crc32.append(d)

# テキスト化したものの CRC-32 を求める
crc32 = BitVecVal(0xffffffff, 32)
for d in text_crc32:
    n = ZeroExt(32, Extract(7, 0, crc32) ^ d)
    for i in range(8):
        n = If(Extract(i, i, n) == ZERO, n, (POLY << i) ^ n)
    crc32 = Extract(39, 8, n) ^ ZeroExt(8, Extract(31, 8, crc32))
calculated_crc32 = ~crc32

# 元の CRC-32 と求めた CRC-32 が一致するケースを全列挙する
s = Solver()
s.add(calculated_crc32 == answer_crc32)
while s.check() == sat:
    found_crc32 = s.model()[answer_crc32].as_long()
    print("%08x" % found_crc32)
    s.add(answer_crc32 != found_crc32)

他のソルバでもやってみたかったけど、Z3 でも 3 時間かかるんじゃ無理かな。

追記：
テキスト化しない場合は 30 秒。これなら他のソルバとベンチマークできそうですね。

$ time python crc32.py 
cc4fbb6a
ffffffff

real    0m29.339s
user    0m29.327s
sys     0m0.032s