[ 2013 年 9 月 27 日のhttps://codegolf.stackexchange.com/questions/12664/implement-superoptimizer-for-additionに関連]
スーパーオプティマイザーの書き方に興味があります。特に、ビットの合計の小さな論理式を見つけること。これは、以前は codegolf の課題として設定されていましたが、想像以上に難しいようです。
バイナリ 0/1 変数 y の合計が値 x に等しいかどうかを確認するために、可能な限り最小の命題論理式を見つけるコードを書きたいと思います。変数を x1、x2、x3、x4 などと呼びましょう。最も単純なアプローチでは、論理式は合計に相当するはずです。つまり、合計が x に等しい場合に限り、論理式は真になります。
これを行うための単純な方法を次に示します。y=15 と x = 5 とします。5 つの変数を選択する 3003 の異なる方法をすべて選び、それぞれについて、それらの変数の AND と残りの変数の否定の AND で新しい節を作成します。最終的に、それぞれの長さがちょうど 15 の 3003 句になり、合計コストは 45054 になります。
ただし、ソリューションに新しい変数を導入することが許可されている場合は、一般的な部分式を削除することで、これを大幅に削減できる可能性があります。したがって、この場合、論理式は y バイナリ変数、x、およびいくつかの新しい変数で構成されます。変数 y の合計が x に等しい場合にのみ、式全体が満足されます。許可されている演算子はand、orおよびのみnotです。
x =1 の場合、少なくとも理論上は、この問題を解決する賢い方法があることがわかりました。ただし、小さなソリューションを検索するための計算集約的な方法を探しています。
How can you make a superoptimizer for this problem?
例。例として、合計が 1 になるときに真になる論理式が必要な 2 つの変数を取り上げます。考えられる答えの 1 つは次のとおりです。
(((not y0) and (y1)) or ((y0) and (not y1)))
z0表すなどの式に新しい変数を導入するにy0 and not y1は、新しい節 を導入して、式の残りの部分全体で(y0 and not y1) or not z0置き換えるy0 and not y1ことができます。z0もちろん、これは式を長くするため、この例では無意味です。