BDD, ZDD

[shnarazk]

clause vivificationすると思った以上に冗長節が生成されている（この時点でなにかおかしいのかもしれない）。
clause vivificationで簡略化させているのだけど、それが同一節を生成することはないのだろうか？
節の同一性を低コストで調べる方法はないからなあ。
うむ！？ここでBDD/ZDDを使えばいいのか！？