2020-08-26

1UIP そのものを学習するということは、いわば枝刈りがちょっとうまくできている DPLL のようなものであり、正しくない。本当に学習すべきなのは、1UIP を用いた cut を参考にしなければならなかった。このように実装を変更したところ、うまく動くようになった。（なぜか release ビルドだとうまく動かず、debug ビルドだと正常に動くのだが……）

状況

ICFP の話を少しした

CDCL バグっている

議題

（あまり喋ることができず……）

DPLL よりも高速かどうかを比較した