“ SCSat3によるラムゼーグラフ探索について ” https://kaigi.org/jsai/webprogram/2015/paper-213.html ソフト節による推論誘導の話が面白い。 ①ソフト節は偽になってもコンフリクトとはみなさない。 ②単位節になった時、単位節伝播をする代わりに伝播すべきだったリテラルを記録しておき、場合分け時に記録されたリテラルから割り当てを行う。 ③違反が繰り返されるソフト節は削除。