やっぱり捨てた方がいい

[shnarazk]

マイクロベンチマークで使っている SC21/p*.cnf が鬼門。色々と手を回して小細工を考えてみる。
その途中で、頻度を上げたreduceを使って cnf/a_*.cnf を解いてみると十数秒でbiclauseが1100台まで生成される。なぜこうなるのか全く不明。大事な節も捨てているはずなのだが。

仮説

節があると決定レベルが戻らずに探索が進み、そこから生成される（最初に見つかった矛盾を解消する）矛盾解消節の大きさは大きいとも小さいともどちらに転ぶかわからない。
一方、捨てまくるとnon-chronological backtrackで戻される。そこから生成される矛盾のレベルは相対的に小さくなり、そこから生成される矛盾解消節のLBDも当然小さくなる。

。。。。詭弁くさい。