Queen Domination by SAT Solving

技術要約：SATソルバによるクイーン・ドミネーション

問題定義
クイーン・ドミネーション問題は、$n \times n$ のチェス盤上のすべてのマスを攻撃するために必要な最小のクイーンの数（$\gamma(Q_n)$ と表記）を求めるものである。この最小値の決定に加え、回転や反転といった盤面の対称性を考慮した上で、同型でない（non-isomorphic）すべての解を列挙することが大きな課題となっている。$\gamma(Q_n)$ の最適値は、UNIDOMのような特化型の探索ツールを用いて $n \le 25$ までは確立されているが、より大きな盤面における非同型解の列挙は計算量的に非常に困難である。この領域における重要な懸念事項は、計算結果の信頼性である。他の組合せ論的証明（例：ラムの問題）における不一致や、特化型ソルバにおけるバグの発見は、独立して検証可能な正当性の証明（correctness certificates）の必要性を浮き彫りにしている。

手法
著者らは、クイーン・ドミネーション問題に対処するために、証明生成型のブール充足可能性（SAT）フレームワークを提案する。独自の探索アルゴリズムを実装するのではなく、問題を連言標準形（CNF）の命題論理式へとエンコードする。本手法は、以下の主要な技術的革新に基づいている。

1. ライン変数によるエンコーディング:
   核心となる革新は、特定の幾何学的なライン（行、列、対角線、および逆対角線）に少なくとも一つのクイーンが含まれているかを表す補助的なブール変数の導入である。

   • クイーン変数 ($Q_i$): マス $i$ にクイーンが配置されているかを示す。
   • ライン変数 ($L_\ell$): ライン $\ell$ が「アクティブ」（クイックを含む）であるかを示す。
   • 制約: ラインがアクティブであれば、そのライン上にクイーンが存在することを保証する節（clause）を用いる。ドミネーション（支配）は、すべてのマスについて、交差する4つのラインのうち少なくとも1つがアクティブであることを要求することで表現される。カーディナリティ制約は、総クイーン数（$\sum Q_i \le \gamma$）および総アクティブライン数（$\sum L_\ell \le 4\gamma$）を制限する。

2. カーディナリティ・エンコーディングとリテラル順序:

   • カーディナリティ制約は、トータライザ（totalizer）ベースの手法を用いてエンコードされる。クイーンの制約には、Cube-and-Conquerフレームワークと互換性のある標準的なトータライザを使用し、ラインの制約にはパフォーマンス向上のためにモジュロ・トータライザを使用する。
   • ヒルベルト曲線順序: クイーンのカーディナリティ制約に対して、新しいリテラル順序戦略を適用する。ボードをヒルベルト曲線経由で走査することで、空間的に隣接するマスをカウンティング・ツリー内でグループ化する。これにより空間的な局所性が保持され、強力なユニット伝播（unit propagation）が実現される。実験の結果、この順序付けにより、$n=14$ のインスタンスをデフォルトの順序よりも約31.5倍高速に解くことができた。

3. 対称性の破り（Symmetry Breaking）:
   対称な解の冗長な探索を排除するため、元のクイーンの構成とその7つの非恒等な幾何学的変換との間に、辞書式順序制約（Warwick Harveyの手法に基づく）を課す。これにより、予備テストにおいて大幅な高速化（例：$n=15$ で6.64倍）が実現した。

4. Cube-and-Conquer:
   大規模なインスタンスに対しては、トータライザ・エンコーディングから派生した補助変数に基づいて分岐することで、探索空間を独立した部分問題（キューブ）に分割する。これにより、個々のクイーンの配置に依存することなく、並列計算による解法とスケーラビリティの向上を可能にする。

5. 証明生成と検証:
   本フレームワークは、ブロッキング節を反復的に追加することでモデルを列挙する cadical-exhaust を使用する。完全性を証明するために、「信頼された節（trusted clauses）」を含むDRAT証明を生成する。これらの証明は drat-trim-t を用いて独立して検証される。これにより、結果がソルバの内部的な探索ロジックの正当性に依存するのではなく、エンコーディングと証明チェッカーのみに依存することを保証する。

主な結果
本研究は、$n \le 19$ のすべてのケースについて、非同型な最小クイーン・ドミネーション解の列挙に成功した。結果には以下が含まれる：

• 文献の訂正: $n=16$ において、本論文は先行研究の報告との不一致を指摘している。特化型ソルバのUNIDOMは43個の非同型解を報告したが、SATフレームワークは正確には 371個 であることを証明した。著者らは、これを特定の構成下で有効な解を見落とすUNIDOMのバグに起因すると考えている。
• 未解決ケースの解決: 以前は未解決であった $n=19$ のケースが解決され、非同型な最小解が正確に 11個 であることが確立された。
• パフォーマンス: SATフレームワークは、非自明なインスタンスにおいて特化型ソルバであるUNIDOMを一貫して上回った。$n=19$ において、SATアプローチによる列挙にかかった時間は約171,575秒（CPU時間）であり、UNIDOMの714,733秒と比較して高速であった。ライン変数の導入は極めて重要であり、これを用いない予備バージョンでは、$n=19$ のインスタンスの解決および検証に22.8倍長く時間を要した。

意義と主張
本論文の主な貢献は、高性能かつ独立して検証可能なクイーン・ドミネーション列挙の解法を提供することである。特化した探索コードから、証明生成型のSATフレームワークへと移行することで、計算プロセスに求められる「信頼」の度合いを低減させている。結果の正当性は、特化したソルバの複雑でカスタムメイドなロジックではなく、SATエンコーディングと外部の証明チェッカーのみに依存することになる。

本研究は、補助変数の導入によって幾何学的構造を露出させること、グローバル制約を用いること、そして幾何学を考慮したリテラル順序付けを行うといった、注意深いエンコーディング設計によって、証明生成型SATソルビングが、高度に最適化されたドメイン特化型ソルバと同等、あるいはそれ以上に優れていることを示している。著者らは、さらなる検証と研究を促進するため、ソースコードと解データを公開している。