2020-08-25

もしかしたら、1UIP を用いた節学習についてとても勘違いしていたことがあったかもしれないことに気づいた

というかこれがバグの原因では？……

今まで、1UIP の否定そのものを学習していたわけだったが、これはたまたま 1UIP cut として機能する場合が多かっただけであって、正しいやり方ではなかった。正しくは、「1UIP の successors の predecessors かつトポロジカルソートをしたときに 1UIP と同じ階層に存在するノードの否定の節」を学習すべきである。

いやこれもおかしくない？

おかしいね

「1UIP の successors の predecessors で、1UIP から到達できないノードかつ 1UIP の否定の節」なら……

……ということで、コードを書きなおす。

（この勘違いは、1UIP を用いた節学習ならば毎回 asserting clause が学習されるという勘違いから来ていたものでもある。正確には、「その学習節は backtrack 先で即座に asserting clause として機能する」ということだった）