半年でやることやった後のがんばりについて
- https://gitlab.com/shnarazk/SAT/splr/issues/90
- global control of restart 'global'は大局観ってやつ。
restart_step
の存在はやはり気になる。今のソルバーはまだ何かに気づけていない。 - [solved by 0.1.5] a better bounded var-rewarding mechanism ASIDS, CHBどちらも確認済みではあるのだが。ただやる意味あるのかちょっと疑問に思ってきた。 時間変化するのだから、求解直後の値を見てもそこには最終ステップを解くのに必要だった情報しか残っていないと考えるべきだろう。 従って、最適な値分散なんてものは存在しない。そこに至るまでの履歴も重要。 もう一つ、zero-sum rewardingについても検討のこと。
- new category of problems based on something like FUP, CNF
- investigate the reason why satcoin groups require 'deep search' to be solved. これは1に関係するのだろう。FUPのデータも必要かも。 ただし0.1.5では0.1.4で見られたきれいなセパレーションがなくなっている。
2019-10-27: A better bounded var-rewarding mechanismに関する意外な展開
夏から9月にかけてリスタートを掛けても意外に割り当て対象が限定されているという話を散々やってきていた のだが、よくわからぬregressionの解消に取り組んでいてとんでもないことがわかった。結局、CHBという strictly bounded var-rewardingはやはりいい結果につながっていたようだ。あまりによい成果が出たので一旦 計画を延期して0.1.5をリリースすることにしよう。0.1.5がなぜいいのかはリリース後に検討。ここの話に戻っ てくるのはさらにその後で十分ということになった。
2019-11-29: 0.2.0のリリース
パラメータチューニングの消耗戦の合間にHaskellでいうところの実行速度に影響を及ぼさないnewtype的な型安全性を導入してみた。 実際にRustでも速度低下が見られなかったので内部構造の変更は大きな変更だろうということで0.2.0に格上げ。 パラメータチューニングの方は変数活性度の減衰係数でわずか1問の進展が見られたのでそれも入れて0.2.0をリリース。
- 1:大局観は進展見られず
- 3:問題のカテゴライズは全く手付かず
- 4:deep search問題は進展見られず