IPMに期待

 Cuopt,Highs共に、ダイレクトコルスキー分解を用いたIPM（内点法）を準備中の模様です。

Githubで実装を眺めることが出来ます。10月中のリリースと予想します。

超大規模問題、instance23/24の問題は、

■グラフがコンパイル出来ない

■SATソルバがコンパイル出来ない

■Lpソルバが遅すぎる

というものです。３番目の問題について、PDLPに期待しました。1e-4では、期待通りの性能を示すものの1e-5以上の精度となると遅すぎ、実用精度の1e-7では、全く遅すぎて使えないことが判明しました。

そこで、高精度領域でも速度が落ちないバリアソルバに期待がかかります。NVidia　CuDSS疎行列のコルスキー分解で革新的な速度向上があったようです。CuDSSについては、プレリリースされており、その気になれば、これを用いて自前実装も可能だとは思いますが、上記の通り、リリースを寝て待てばよいだけなので、待つことにしたいと思います。それまでに、上記他の課題をクリアしたいと思います。

MaxSATソルバのダイエット

 ■SATソルバが使えない問題

に対して、構造を見直しメモリダイエットを行いました。およそ1/4程度にはなりました。

結果、instance23については、AL1でコンパイル出来るようになりました。このとき、25GB位の消費です。

しかし、instance24については、AL1コンパイルが出来ませんでした。およそ57GB位で、ストップします。TIME制約関係の消費が大きいようで、恐らくは、SATソルバの最大節数を超えているのだと思われます。（デバッグ用の開発環境が32GBなのでデバッグが出来ません）

SATソルバが使えないと、やはり痛いです。LPソルバから整数化を行うのにLPソルバだけで整数化しようとすると途方もない時間がかかります。現実的な時間内に解を得るには、なんとかして使えるような検討を行う必要があります。

PDLPX

PDLPの改善版です。3倍程度、特に高精度領域において、改善が著しいようです。

[2507.14051] cuPDLPx: A Further Enhanced GPU-Based First-Order Solver for Linear Programming

■LPソルバが遅すぎる問題

現状では、全く遅すぎて、10倍以上の速度アップが必要ではないかと見ています。

上記でも足りませんが、とりあえず、

ＨＩＧＨＳまたは、Cuopt で、実装されるのを待ちたいと思います。

GPUの比較

PDLPで比較してみました。 

RTX4060TIをRTX3080 12GBに置き換えてみたのですが、期待していた性能向上は見られませんでした。ネックはメモリ転送レートと睨んで、あわよくば3倍と期待していましたが、1-3割程度の効果しかありませんでした。

• • 
    
  • 

    

    
    
    
    
    
  • 
    
  • 
    

instance23のLBが判明

これまでの世界記録は、 

Instance23 ： LB＝16990 UB＝17428

でした。今回、新たに　17284.3 ⇒LB＝17285

であることを発見しました。

大幅なLB更新は確定的で、これまでの経験上、UBもその直近傍(ex 17285)にあると思われます。

しかし、次の

■RCSSP　ソルバが遅すぎる

■LPソルバが遅すぎる

■SATソルバが使えない問題

という問題のため、それ以上前に進められていません。

LPソルバについては、

■GPU置き換え

■PDLPアルゴリズムの改善

■新たなIPMソルバの適用

の可能性を検討しました。

Pseude boolean competition 2025

日本から、3チームが出場したようです。

PB25 Pseudo-Boolean Competition 2025

名古屋大の酒井先生と山梨大の鍋島先生のチームが優勝されました。

擬ブールソルバ競技会（Pseudo-Boolean Competition 2025)よりDEC-LIN 部門 第1位を受賞しました。(情報システム学専攻 酒井 正彦 教授) | 名古屋大学情報学部／大学院情報学研究科

その他にもPrintempsや今井さんも参加されたようです。

Pseudo boolean  competition は、昔からあったように思いますが、しばらくお休みがあって、ここ最近復活したようです。最近の潮流は、MIPソルバの使用にあるように思います。

Maxsat competition については、今年はお休みです。一昨年と去年の解けた問題数の差異は、殆どなく誤差の範囲と言ってよいかもしれません。技術的進展がないと、研究者も敬遠するのかもしれません。

SAT Competition 2025

 The Results of SAT Competition 2025

今年の優勝者は、AE-Kissat-MABで、

DynamicSAT: Dynamic Configuration Tuning for SAT Solving

ダイナミックにチューニングするソルバのようです。明らかに優位性が見れます。

それから一カ月も経たないのに、それを凌駕するとの報告がありました。

Autonomous Code Evolution Meets NP-Completeness

NVidiaのSaturationというフレームワークを使って人がコーディングしたよりも性能が良いソルバを自動生成する、

とのことのようです。AlphaEvolve

Google: AlphaEvolve - Gemini を活用した次世代アルゴリズム設計について #GoogleCloud - Qiita

よりも、より進歩性のあるということを主張しています。

初期のSATソルバとは違い、最近のSATソルバは、細かな改善の積み重ねの結果としてあり、何のパラメータが支配的な性能向上につながるか？というのは、パラメータ数が多すぎてよく分からないことになっていると思います。　こうしたパラメータが多数ある分野でのチューニングは、人間は、LLMには敵わない、と私も見ています。言うなれば、人間勤務表ースケジュールナース勤務表のような関係性です。

最適化ソルバで、研究者自体が駆逐される可能性も出てきるでしょうか？　こちらは、未だ論文化されていない方法が多数あると思われます。（私が取り組んでいるのも、その一つです。）それらが全部オープンにされない限りは、LLMが支配することはないと思います。

逆に言えば、

■最先端技術が全てオープンになっているSAT技術分野でのLLMとの闘い

今後のSAT　Competitionは、LLMが生成したソルバが参戦してくるでしょうから、来年以降、過去の技術資産の組み合わせだけで、LLM生成ソルバに勝つのは、極めて難しいと思います。昨今の革新的進歩がないことを勘案すると、極めて不利な情勢です。しかし、一抹の期待を抱かずにはいられません。