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.179s1 つめは 3 分くらいで見つかるけど、2 つめは 2 時間くらい、チェック完了までは 3 時間弱かかった。 単純に 2^32 個を全チェックする方法なら、秒間 100 万個調べられるとして 1 時間ちょっとという計算。まあ、こんなもんなのかな。追記：shinh さんによると 1 分でできるらしい。残念。 ソースはこんな感じ。もっと綺麗に書けそう。 # coding: utf-8 from z3 import * # CRC-32 の生成多項式（の反転） POLY = 0xedb
