[2J5-OS-36a] OS-36

3:45 PM - 4:00 PM JST(6:45 AM - 7:00 AM UTC)

[2J5-OS-36a-02] (OS invited talk) SAT Encoding Design in the Winning Solution of ICFPC 2025

〇Yoichi Iwata¹ (1. AtCoder Inc.)

Keywords:

SAT solver,SAT encoding,graph inference

SAT ソルバはエンコーディングの違いによって性能が大きく変化することが知られているが，その要因は単純な変数数や制約数の削減に限られない．本講演では，国際プログラミングコンテスト ICFPC 2025 において SAT ソルバを用いて優勝を達成した解法を対象に，実際に採用したSAT エンコーディング設計と，その設計差が実行性能に与えた影響について報告する．ICFPC 2025 の問題は，未知のグラフを観測情報から特定するというものであり，ナイーブな定式化では SAT ソルバの探索が著しく非効率であった．本解法では，問題の解構造を分解し，階層的な決定を可能とする補助変数を導入することで，探索の効率化を図った．その結果，変数数自体は増加するにもかかわらず，SAT ソルバの探索挙動が大きく改善され，実行時間の大幅な短縮が確認された．