2020-07-29

状況

CDCL のバグを取ることができた

Graphviz で Implication Graph を可視化した

議題

CDCL が DPLL より遅い

すべてのケースを一斉にテストしたとき、DPLL より CDCL が遅いことはわかっている

各ケースにおける実行時間を計測し、表に実験結果を張って追跡するとデバッグがしやすい

Google Documents とかでまとめる(先生の研究室ではそのようになっている)

Implication Graph の可視化について

他の人に CDCL の原理を説明するときにとてもわかりやすくていいですね

論理と形式化の授業では Implication Graph は見せなかったので、これを授業で使ってみたいぐらい

「節をエッジではなくて四角のノードとして用意して、リテラル→エッジ→リテラルのような繋がりになっているグラフを描いてみると大きいケースではわかりやすくなるかもしれない」

このグラフを用いて、先生に CDCL の仕組みの説明をすることになって、した

うまく説明ができていた