: SATソルバーを作っていた
やったこと SAT CDCLソルバを一通り形にした。 のだけど、微妙にバグっている気がする。 直すのがしんどい‥‥。
if you wanna break free you better listen to me
やったこと SAT CDCLソルバを一通り形にした。 のだけど、微妙にバグっている気がする。 直すのがしんどい‥‥。
やったこと 日常 まだまだ疲れているなぁ、という印象。 さすがに数日ではどうにもならない部分もある。 休もう‥‥、と言って眠りすぎな気もする。 がんばっていこう。 あとQuineを書こうと思っていた言語が、すでにQuineを書いていた言語だった。 そういうこともあるらしい。
やったこと バナンザ 100%クリアした。 バナナ1000本にするためのバナチップ集めがただの作業だった。 普通にやってて集まらない量要求しないでくれ。 とはいえ、最後の一枚絵には満足感があった。 次は何やろうか。 MD シンクロフェス最終日だった。 ようやくDLv Maxに到…
やったこと 帰宅 飛行機の中ではバナンザをやっていた。 ボスラッシュっぽいのが妙に強化されたボスで、そこまでの経験があまり生きない形だったのが普通に残念だった。 何をさせたいんだ。 北京空港に着いたのは4時30分くらいだった。 予定よりもかなり早かった。 早く着いても暇なだけな…
やったこと Marktoberdorf 真の最終日。 朝食のあとバスで空港まで連れていってもらい、北京経由で日本へと帰る。 空港で色々お土産を買った。 アイスワインを見つけたけれど49ユーロで悩んだが、せっかくなので買っていくことにする。 あとはプレッツェルとか無駄にデカいハリ…
やったこと 終戦 平和を祈って。 Marktoberdorf 実質的な最終日。 講義よりも手元でCDCLについての理解を深めることに集中していた。 かなり理解できたと思う。 と同時に、よくできたアルゴリズムだなぁと感心していた。 最後のFarewell Partyで出た巻き寿司…
やったこと Marktoberdorf 昨日のexcursionであまりに消耗したため、完全にダメになっていた。 苦手なことはやるべきではない。 あと全体的に詳細すぎる話が多くてあまり学びがなかった。 しいて言うならsimplification orderingという言葉は覚え…
やったこと Marktoberdorf 今日はexcursionがあった。 バスで南の方まで移動して、そのあとは徒歩でここに向かった。 https://kaiserschmarrn-alm.de 結構遠くて1時間半くらいかかったのではないかと思う。 途中、川沿いに洞窟のようなと…
やったこと Marktoberdorf 2週目の2日目。 2週目の方が丁寧な講義が多くて分かりやすいような気がする。 久し振りにSAT Solverを作りたい気持ちになっている。 やってみるべきかもしれない。 Bolt Boltというプログラミング言語がある。 実行速度をウリに…
やったこと Marktoberdorf https://x.com/make_now_just/status/1954798283739529675 2週目。 講師陣が入れ替わり内容が一新される。 個人的に興味深かったのは、コンパイラのテストをする話かもしれない。 わりと実践的…
やったこと Marktoberdorf 日曜日なので休日。 どこかに行くか悩んでいたのだけど、32ユーロでバイエルン州内の周遊チケットがあることに気付いたので、ダッハウに行くことにした。 ミュンヘンから北に少し行ったところ。ダッハウには強制収容所の跡地がある。 多分それしかない…
やったこと Marktoberdorf LPに関する直感が足りてないときにそういう話を色々されても分からんなぁ、と思いながら聞き流していた。 大まかな流れはイメージできるのだが、細かい話は全く分からない。 諦めも肝心だろう。 NetKATに関しては、逆に予習しすぎてあまり講義で…
やったこと Marktoberdorf superpositionの気持ちが分かりそうで分かっていない。 とりあえず、first-orderならどうにかなるのが、higher-orderになるとすごく難しくなるということは分かった。 SAT関連というか、resolutionの話…
やったこと Marktoberdorf 引き続きSAT関連の話が多い。 ただ、より詳細に踏み込んできたので面白くなってきた気がする。 とくに、グラフっぽい問題をSATにエンコードして解決する話は興味深かった。 点が何個あれば凸n角形 (-gon) が作れるかという問題や、逆に何…
やったこと Marktoberdorf SAT関連の話が多かった気がする。 何にしても裏にSATが使われているので、意識せざるを得ないということなのかもしれない。 個人的にはクレカの決済プロトコルを検証した話が興味深かった。 Tamarinは本当に使われているんだなぁ、という気…
やったこと 北京首都国際空港 北京首都国際空港で、トランジットのための検査があったのだけど、やたらチェックされてちょっと怖かった。 やはり恐ろしい‥‥。 北京首都国際空港には無料のWi-Fiがあるのだけど、謎の機械にパスポートを入れてアカウントを発行してもらう仕組みで面白かった…
やったこと 日常 さすがに昨日の疲れが残っている。 休みたいが動かねばならない。 がんばれ! 出国 日本を出てドイツへ。 成田空港にやって来た。 なんとなく第2ターミナルかと思っていたら第1ターミナルだった。 やりがちなミスなので気を付けたい。 第1ターミナルでもウイングの北と…
やったこと NEVER END IDOL!!!!!!!!!!!!! DAY 2 12:30頃に家を出て会場に向かう。 途中日高屋で昼飯を食べていたのだけど、餃子をラー油だけで食べていてかなりの疲労を感じた。大丈夫だろうか。 会場に着いたのは15:00頃。 やはり横浜は遠い。 と…
やったこと 準備 ドイツ行きの準備をしていた。 色々と買うものがある。大体100均か無印で揃うので、探していった。 パスポートケースが便利そうだと思っている。 というかパスポートを裸で仕舞っておくのは怖い。 しかしドイツの天気がよく分からんなぁ。
やったこと 研究 論文の調整をしていた。 ArXiv版もおそらく必要になるので、そのための準備。 とりあえず簡単に切り替えられるようにはしたので、提出には間に合うのではないかと思う。 あとはいつ教授とmtgできるのか‥‥。 マジで予定が分からん。