tl;dr
棋譜は f5f6e6f4g7c6g3e7d6f3e3d3b7d7c2g2g1c3b2b3b4f7g5c4c7c8e2 です。
経緯（2020）
オセロには相手の石を1つ以上裏返せる場所にしか石を置けないというルールがあります。
わたしはこのブログで2020年に、オセロの最大分岐数（石を置ける場所の数が最大になるような局面）を求めようとした記事をいくつか書いていました。
成果として、初期局面から合法的に到達可能かを考えなければ34箇所が最大であり、35箇所に石を置ける局面は存在しないことを証明しました。また実際に34箇所に置ける局面を構成できました。
オセロの最大分岐数は34以下 - ubiquitinブログ
初期局面から合法的に到達可能な局面に限定する場合に関しては、34箇所が上界となることがこの結果から言えます。
そこで、合法手生成と盤面更新をビット演算と簡単な四則演算で書き下し、初期局面から合法的に到達可能な最大分岐数とその局面をz3に求めさせるコードを書きました。
到達可能局面をSATソルバーに調べさせる - ubiquitinブログ
当時わたしはSMTソルバのz3 v4.6.0 を使っていましたが、そのPython APIでは、与えた制約と充足可能性において等価なCNF（連言標準形）の式を出力する（というか、内部表現を雑に全部書き出させる）ことができました。そこで、その書き出された式をDIMACS CNF形式に変換して、当時のSAT competition 2020でランキング上位だったCaDiCaLというSATソルバに与えてみました。しかし少なくとも数日では解が求まりませんでした。当時使っていたCPUがi7-4770で、2020年時点でも相当古かったせいかもしれませんが、とにかく当時はそこで一旦諦めました。
経緯（2023）
先日それを思い出して、2020年当時に作ったCNF形式のファイルを最新のSAT competition 2022でランキング上位だったkissatのsc2022-bulkyというrelease versionに投げてみたところ、33箇所がSATISFIABLEで（！）34箇所がUNSATISFIABLEだと証明できました。CPUはRyzen 5950Xで、30時間くらいかかりました。
Release SAT Competition 2022 Bulky Release · arminbiere/kissat · GitHub
しかし、その出力（すなわち、制約を満足するような真偽値の割り付け）から、オセロで33箇所に置ける局面への具体的な再構成手順が存在しませんでした。というのも、わたしは2020年時点では33箇所もUNSATなのではと予想していたので、z3の内部表現を標準出力に全部書き出させるという方法を取ったときも、その内部変数に対して真偽値を強制的に渡す方法は調べずにいました。実際、簡単な方法は見当たりませんでした。
そこで、当時z3で書いたコードをC++で書き直しました。CNF形式のファイルだけでなく、論理式上での変数番号とそのオセロソフトにおける意味との対応関係も別ファイルとして書き出すような実装をしました。kissat sc2022-bulkyに投げたところ、8時間くらいで計算できました。出力をPythonで適当に処理すると、結果として冒頭の棋譜が得られ、WZebraで画像を作ることができました。
余談: WZebraの機能で、棋譜の上で何ターン目に置かれたかの番号を石の上に書き出すことができる（Export game as PNG 等）のですが、この棋譜を書き出そうとしたところ石の色が勝手に変わるバグを踏みました。
