なんかdocumentationに関するissueが立っていたのでちょっと英文を足して、 それだけではリリースにならないのでちょっと並列化を考えてみた。 SAT competitionのmain trackに参加する気ならそれはしない方がいいのだけど、 もはやどういう手段でもいいから高速化する方が、 そこそこいる利用者には喜ばれるのではなかろうか。
ということでpropagationの中の節ごとに新規リテラルを決定する部分を並列化してみた。 そうすると単位伝播が起きた時に一気にrollbackしないといけないので、 ちょっと単位伝播の「到達性」を緩めてやってrollbackの必要度を下げるような工夫までしたのだが、、、。
rayonを使った簡単便利な高速化が全然成果が出ない。 並列化する条件を変えてみたり、リストの長さを調整したりして並列化オーバーヘッドは克服する程度の粒度は確保できているはずなのに劇的に速度が落ちる。 挙げ句の果てに長さ2のリストをinto_par_mapしてみてもtopで見ると6から7スレッドが走っているtという意味不明な現象に悩まされる。 私の知る限りではこういうことはspin lockしてないと起きないはずなんだけどなあ。 で、tokio化に取り組んでみたり、multi-threaded runtime上でのasync/awaitを考えてみたりして、大変さにめげてしまった（上に成果が出ない）ところで休止中。
結局、今月たまたまredditに投稿されていたrayon並列化に対する質問によればやはりrayonはspin lockしているらしい。うーんそれでも効果がある場合にはあるのかあ。 なぜparallel propagationはその範疇に入らないのだろう。 謎だ。