2020-12-09
状況
ソルバーの内部に「まだ充足されていない節の ID の集合」を入れていた(availClauses)が、これの代わりに Clause に isAvail フィールドを追加してみたところ、一部のテストケースでは高速になったが、それと同時に2倍ほど遅くなったテストケースもあった
遅くなったケースに関しては decideNextBranch が実行された回数が多いせいで、やはり基本的にはコピーに際して実行時間が大幅に増えていることがわかった
これの裏付けとして Clause に無駄なフィールドを複数個付けてベンチマークしたところ全てのテストケースで十数倍遅くなった
「内部状態が可視化された SAT ソルバーの実装」を発表題目にすることを決定