2020-07-15
状況
（他の人のが読みやすかったのでそれを参考に実装している旨も伝えた）
議題
これを理解する必要はなくて、まずどのようにlboolが利用されているかというアルゴリズム的な観点で把握することがすることで、それができてからこのような高度な最適化に関するコード片を理解するのが正しい流れである、との話だった
中間報告書の話
やる
1UIP の定義確認
This nice flipping property holds in general for all unique implication points (UIPs). A UIP of an implication graph is a node at the current decision level d such that every path from the decision variable at level d to the conflict variable or its negation must go through it. Intuitively, it is a single reason at level d that causes the conflict.
UIP は unique implication point の略
implication graph の UIP とは、現在の decision level d におけるすべての decision variable から conflict variable やその否定への path で、必ず通ることになる node のこと。
直感的には、level d における conflict を引き起した単一の理由となる reason のこと。
Unit Propagation ですぐに利用できるような conflict clause のことを asserting clause という。