着々と巨大なSudokuが解けるようになったのでどんどん行きましょう。 largeとかgiantとかを追加キーワードにして検索してとてもよさそうなサイトを見つけたけど、そのサイトはflashで書いてあって一切見れない。 なんという時代（技術）の断絶！
ただチャットページが生きていたのでなんとか144x144とか400x400の問題を見つけることができました。
ということで144x144 sudokuを対象にしてみます。 parseをちゃっちゃと書いて、実行してみるとルール生成中のプロセスサイズが主記憶の16GBを超え出したのでさらにルール数の削減が必要になりました。まあ、気づいていたけどこれまでやらなかった
全ての場合を網羅するルールを生成してから、初期状態を入れるのは無駄
という当たり前のことをいよいよ実践することになりました。
144x144の問題も400x400の問題もどちらも人間が解きやすいように初期状態で結構なセルが埋まっているのでそれらに関する無意味なルールの作成を止めれば、本当に次数が1下がるくらいの効果が期待できるのではなかろうか。 さらに二重にルールを作成していたところがあったので（上三角だけ計算するような感じで）半分だけ生成するようにすると生成されるCNFはおよそ200MB。 これは最初に生成されたものより1桁は小さくなるくらいの効果がありました。 これで、生成時にも16GB内で収まるようになった（ヘッダーを作るためにファイルに書き出すのは全てのルールを生成した後）し、Splr的にも節数は全然問題ありません。 実際、Splrは数秒で解きました。色々とデータが大きいので試したい方は以下をどうぞ。
git clone https://github.com/shnarazk/sudoku_sat.git
cd sudoku_sat
cargo run --bin sudoku144 --release < sudoku144.txt
ちなみにこの変更を施しても400x400は全然ダメ。ルールの生成中にプロセスサイズが40GBを超え、1時間経っても生成が終わらない。ちょっと無理ですね。ルール数は $O(n^4)$ だからなあ。